:: BILINEAR semantic presentation
:: deftheorem Def1 BILINEAR:def 1 :
canceled;
:: deftheorem Def2 defines NulForm BILINEAR:def 2 :
definition
let c
1 be non
empty LoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4, c
5 be
Form of c
2,c
3;
func c
4 + c
5 -> Form of a
2,a
3 means :
Def3:
:: BILINEAR:def 3
for b
1 being
Vector of a
2for b
2 being
Vector of a
3 holds a
6 . b
1,b
2 = (a4 . b1,b2) + (a5 . b1,b2);
existence
ex b1 being Form of c2,c3 st
for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . b2,b3 = (c4 . b2,b3) + (c5 . b2,b3)
proof
set c
6 = the
carrier of c
2;
set c
7 = the
carrier of c
3;
set c
8 = the
carrier of c
1;
deffunc H
1(
Element of the
carrier of c
2,
Element of the
carrier of c
3)
-> Element of the
carrier of c
1 =
(c4 . a1,a2) + (c5 . a1,a2);
consider c
9 being
Function of
[:the carrier of c2,the carrier of c3:],the
carrier of c
1 such that E1:
for b
1 being
Element of the
carrier of c
2for b
2 being
Element of the
carrier of c
3 holds c
9 . b
1,b
2 = H
1(b
1,b
2)
from BINOP_1:sch 4();
reconsider c
10 = c
9 as
Form of c
2,c
3 ;
take
c
10
;
thus
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
10 . b
1,b
2 = (c4 . b1,b2) + (c5 . b1,b2)
by E1;
end;
uniqueness
for b1, b2 being Form of c2,c3 holds
( ( for b3 being Vector of c2
for b4 being Vector of c3 holds b1 . b3,b4 = (c4 . b3,b4) + (c5 . b3,b4) ) & ( for b3 being Vector of c2
for b4 being Vector of c3 holds b2 . b3,b4 = (c4 . b3,b4) + (c5 . b3,b4) ) implies b1 = b2 )
proof
let c
6, c
7 be
Form of c
2,c
3;
assume that E1:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
6 . b
1,b
2 = (c4 . b1,b2) + (c5 . b1,b2)
and E2:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
7 . b
1,b
2 = (c4 . b1,b2) + (c5 . b1,b2)
;
now
let c
8 be
Vector of c
2;
let c
9 be
Vector of c
3;
thus c
6 . c
8,c
9 =
(c4 . c8,c9) + (c5 . c8,c9)
by E1
.=
c
7 . c
8,c
9
by E2
;
end;
hence
c
6 = c
7
by BINOP_1:2;
end;
end;
:: deftheorem Def3 defines + BILINEAR:def 3 :
definition
let c
1 be non
empty HGrStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4 be
Form of c
2,c
3;
let c
5 be
Element of c
1;
func c
5 * c
4 -> Form of a
2,a
3 means :
Def4:
:: BILINEAR:def 4
for b
1 being
Vector of a
2for b
2 being
Vector of a
3 holds a
6 . b
1,b
2 = a
5 * (a4 . b1,b2);
existence
ex b1 being Form of c2,c3 st
for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . b2,b3 = c5 * (c4 . b2,b3)
uniqueness
for b1, b2 being Form of c2,c3 holds
( ( for b3 being Vector of c2
for b4 being Vector of c3 holds b1 . b3,b4 = c5 * (c4 . b3,b4) ) & ( for b3 being Vector of c2
for b4 being Vector of c3 holds b2 . b3,b4 = c5 * (c4 . b3,b4) ) implies b1 = b2 )
proof
let c
6, c
7 be
Form of c
2,c
3;
assume that E2:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
6 . b
1,b
2 = c
5 * (c4 . b1,b2)
and E3:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
7 . b
1,b
2 = c
5 * (c4 . b1,b2)
;
now
let c
8 be
Vector of c
2;
let c
9 be
Vector of c
3;
thus c
6 . c
8,c
9 =
c
5 * (c4 . c8,c9)
by E2
.=
c
7 . c
8,c
9
by E3
;
end;
hence
c
6 = c
7
by BINOP_1:2;
end;
end;
:: deftheorem Def4 defines * BILINEAR:def 4 :
definition
let c
1 be non
empty LoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4 be
Form of c
2,c
3;
func - c
4 -> Form of a
2,a
3 means :
Def5:
:: BILINEAR:def 5
for b
1 being
Vector of a
2for b
2 being
Vector of a
3 holds a
5 . b
1,b
2 = - (a4 . b1,b2);
existence
ex b1 being Form of c2,c3 st
for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . b2,b3 = - (c4 . b2,b3)
uniqueness
for b1, b2 being Form of c2,c3 holds
( ( for b3 being Vector of c2
for b4 being Vector of c3 holds b1 . b3,b4 = - (c4 . b3,b4) ) & ( for b3 being Vector of c2
for b4 being Vector of c3 holds b2 . b3,b4 = - (c4 . b3,b4) ) implies b1 = b2 )
proof
let c
5, c
6 be
Form of c
2,c
3;
assume that E3:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
5 . b
1,b
2 = - (c4 . b1,b2)
and E4:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
6 . b
1,b
2 = - (c4 . b1,b2)
;
now
let c
7 be
Vector of c
2;
let c
8 be
Vector of c
3;
thus c
5 . c
7,c
8 =
- (c4 . c7,c8)
by E3
.=
c
6 . c
7,c
8
by E4
;
end;
hence
c
5 = c
6
by BINOP_1:2;
end;
end;
:: deftheorem Def5 defines - BILINEAR:def 5 :
:: deftheorem Def6 defines - BILINEAR:def 6 :
:: deftheorem Def7 defines - BILINEAR:def 7 :
definition
let c
1 be non
empty LoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4, c
5 be
Form of c
2,c
3;
redefine func - as c
4 - c
5 -> Form of a
2,a
3 means :
Def8:
:: BILINEAR:def 8
for b
1 being
Vector of a
2for b
2 being
Vector of a
3 holds a
6 . b
1,b
2 = (a4 . b1,b2) - (a5 . b1,b2);
coherence
c4 - c5 is Form of c2,c3
;
compatibility
for b1 being Form of c2,c3 holds
( b1 = c4 - c5 iff for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . b2,b3 = (c4 . b2,b3) - (c5 . b2,b3) )
proof
let c
6 be
Form of c
2,c
3;
thus
( c
6 = c
4 - c
5 implies for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
6 . b
1,b
2 = (c4 . b1,b2) - (c5 . b1,b2) )
assume E4:
for b
1 being
Vector of c
2for b
2 being
Vector of c
3 holds c
6 . b
1,b
2 = (c4 . b1,b2) - (c5 . b1,b2)
;
hence
c
6 = c
4 - c
5
by BINOP_1:2;
end;
end;
:: deftheorem Def8 defines - BILINEAR:def 8 :
theorem Th1: :: BILINEAR:1
theorem Th2: :: BILINEAR:2
theorem Th3: :: BILINEAR:3
proof
let c
1 be non
empty add-associative LoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4, c
5, c
6 be
Form of c
2,c
3;
now
let c
7 be
Vector of c
2;
let c
8 be
Vector of c
3;
thus ((c4 + c5) + c6) . c
7,c
8 =
((c4 + c5) . c7,c8) + (c6 . c7,c8)
by Def3
.=
((c4 . c7,c8) + (c5 . c7,c8)) + (c6 . c7,c8)
by Def3
.=
(c4 . c7,c8) + ((c5 . c7,c8) + (c6 . c7,c8))
by RLVECT_1:def 6
.=
(c4 . c7,c8) + ((c5 + c6) . c7,c8)
by Def3
.=
(c4 + (c5 + c6)) . c
7,c
8
by Def3
;
end;
hence
(c4 + c5) + c
6 = c
4 + (c5 + c6)
by BINOP_1:2;
end;
theorem Th4: :: BILINEAR:4
theorem Th5: :: BILINEAR:5
proof
let c
1 be non
empty right-distributive doubleLoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4 be
Element of c
1;
let c
5, c
6 be
Form of c
2,c
3;
now
let c
7 be
Vector of c
2;
let c
8 be
Vector of c
3;
thus (c4 * (c5 + c6)) . c
7,c
8 =
c
4 * ((c5 + c6) . c7,c8)
by Def4
.=
c
4 * ((c5 . c7,c8) + (c6 . c7,c8))
by Def3
.=
(c4 * (c5 . c7,c8)) + (c4 * (c6 . c7,c8))
by VECTSP_1:def 11
.=
((c4 * c5) . c7,c8) + (c4 * (c6 . c7,c8))
by Def4
.=
((c4 * c5) . c7,c8) + ((c4 * c6) . c7,c8)
by Def4
.=
((c4 * c5) + (c4 * c6)) . c
7,c
8
by Def3
;
end;
hence
c
4 * (c5 + c6) = (c4 * c5) + (c4 * c6)
by BINOP_1:2;
end;
theorem Th6: :: BILINEAR:6
theorem Th7: :: BILINEAR:7
theorem Th8: :: BILINEAR:8
E7:
now
let c
1 be non
empty 1-sorted ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4 be
Form of c
2,c
3;
let c
5 be
Element of the
carrier of c
2;
let c
6 be
Element of c
3;
E8:
dom c
4 = [:the carrier of c2,the carrier of c3:]
by FUNCT_2:def 1;
then consider c
7 being
Function such that E9:
(
(curry c4) . c
5 = c
7 &
dom c
7 = the
carrier of c
3 &
rng c
7 c= rng c
4 )
and
for b
1 being
set holds
( b
1 in the
carrier of c
3 implies c
7 . b
1 = c
4 . c
5,b
1 )
by FUNCT_5:36;
rng c
7 c= the
carrier of c
1
by E9, XBOOLE_1:1;
then reconsider c
8 = c
7 as
Function of the
carrier of c
3,the
carrier of c
1 by E9, FUNCT_2:4;
c
8 = (curry c4) . c
5
by E9;
hence
(curry c4) . c
5 is
Functional of c
3
;
consider c
9 being
Function such that E10:
(
(curry' c4) . c
6 = c
9 &
dom c
9 = the
carrier of c
2 &
rng c
9 c= rng c
4 )
and
for b
1 being
set holds
( b
1 in the
carrier of c
2 implies c
9 . b
1 = c
4 . b
1,c
6 )
by E8, FUNCT_5:39;
rng c
9 c= the
carrier of c
1
by E10, XBOOLE_1:1;
then reconsider c
10 = c
9 as
Function of the
carrier of c
2,the
carrier of c
1 by E10, FUNCT_2:4;
c
10 = (curry' c4) . c
6
by E10;
hence
(curry' c4) . c
6 is
Functional of c
2
;
end;
:: deftheorem Def9 defines FunctionalFAF BILINEAR:def 9 :
:: deftheorem Def10 defines FunctionalSAF BILINEAR:def 10 :
theorem Th9: :: BILINEAR:9
proof
let c
1 be non
empty 1-sorted ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4 be
Form of c
2,c
3;
let c
5 be
Vector of c
2;
set c
6 =
FunctionalFAF c
4,c
5;
E9:
(
dom c
4 = [:the carrier of c2,the carrier of c3:] &
rng c
4 c= the
carrier of c
1 )
by FUNCT_2:def 1;
consider c
7 being
Function such that E10:
(
(curry c4) . c
5 = c
7 &
dom c
7 = the
carrier of c
3 &
rng c
7 c= rng c
4 )
and E11:
for b
1 being
set holds
( b
1 in the
carrier of c
3 implies c
7 . b
1 = c
4 . c
5,b
1 )
by E9, FUNCT_5:36;
thus
(
dom (FunctionalFAF c4,c5) = the
carrier of c
3 &
rng (FunctionalFAF c4,c5) c= the
carrier of c
1 )
by E10;
let c
8 be
Vector of c
3;
thus
(FunctionalFAF c4,c5) . c
8 = c
4 . c
5,c
8
by E10, E11;
end;
theorem Th10: :: BILINEAR:10
proof
let c
1 be non
empty 1-sorted ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4 be
Form of c
2,c
3;
let c
5 be
Vector of c
3;
set c
6 =
FunctionalSAF c
4,c
5;
E10:
(
dom c
4 = [:the carrier of c2,the carrier of c3:] &
rng c
4 c= the
carrier of c
1 )
by FUNCT_2:def 1;
consider c
7 being
Function such that E11:
(
(curry' c4) . c
5 = c
7 &
dom c
7 = the
carrier of c
2 &
rng c
7 c= rng c
4 )
and E12:
for b
1 being
set holds
( b
1 in the
carrier of c
2 implies c
7 . b
1 = c
4 . b
1,c
5 )
by E10, FUNCT_5:39;
thus
(
dom (FunctionalSAF c4,c5) = the
carrier of c
2 &
rng (FunctionalSAF c4,c5) c= the
carrier of c
1 )
by E11;
let c
8 be
Vector of c
2;
thus
(FunctionalSAF c4,c5) . c
8 = c
4 . c
8,c
5
by E11, E12;
end;
theorem Th11: :: BILINEAR:11
theorem Th12: :: BILINEAR:12
theorem Th13: :: BILINEAR:13
proof
let c
1 be non
empty LoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4, c
5 be
Form of c
2,c
3;
let c
6 be
Vector of c
3;
now
let c
7 be
Vector of c
2;
thus (FunctionalSAF (c4 + c5),c6) . c
7 =
(c4 + c5) . c
7,c
6
by Th10
.=
(c4 . c7,c6) + (c5 . c7,c6)
by Def3
.=
((FunctionalSAF c4,c6) . c7) + (c5 . c7,c6)
by Th10
.=
((FunctionalSAF c4,c6) . c7) + ((FunctionalSAF c5,c6) . c7)
by Th10
.=
((FunctionalSAF c4,c6) + (FunctionalSAF c5,c6)) . c
7
by HAHNBAN1:def 6
;
end;
hence
FunctionalSAF (c4 + c5),c
6 = (FunctionalSAF c4,c6) + (FunctionalSAF c5,c6)
by FUNCT_2:113;
end;
theorem Th14: :: BILINEAR:14
proof
let c
1 be non
empty LoopStr ;
let c
2, c
3 be non
empty VectSpStr of c
1;
let c
4, c
5 be
Form of c
2,c
3;
let c
6 be
Vector of c
2;
now
let c
7 be
Vector of c
3;
thus (FunctionalFAF (c4 + c5),c6) . c
7 =
(c4 + c5) . c
6,c
7
by Th9
.=
(c4 . c6,c7) + (c5 . c6,c7)
by Def3
.=
((FunctionalFAF c4,c6) . c7) + (c5 . c6,c7)
by Th9
.=
((FunctionalFAF c4,c6) . c7) + ((FunctionalFAF c5,c6) . c7)
by Th9
.=
((FunctionalFAF c4,c6) + (FunctionalFAF c5,c6)) . c
7
by HAHNBAN1:def 6
;
end;
hence
FunctionalFAF (c4 + c5),c
6 = (FunctionalFAF c4,c6) + (FunctionalFAF c5,c6)
by FUNCT_2:113;
end;
theorem Th15: :: BILINEAR:15