:: VECTSP_1 semantic presentation

defpred S1[ Element of REAL , set ] means a2 = - a1;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
func G_Real -> strict LoopStr equals :: VECTSP_1:def 6
LoopStr(# REAL ,addreal ,0 #);
coherence
LoopStr(# REAL ,addreal ,0 #) is strict LoopStr
;
end;

:: deftheorem Def1 VECTSP_1:def 1 :
canceled;

:: deftheorem Def2 VECTSP_1:def 2 :
canceled;

:: deftheorem Def3 VECTSP_1:def 3 :
canceled;

:: deftheorem Def4 VECTSP_1:def 4 :
canceled;

:: deftheorem Def5 VECTSP_1:def 5 :
canceled;

:: deftheorem Def6 defines G_Real VECTSP_1:def 6 :
G_Real = LoopStr(# REAL ,addreal ,0 #);

registration
cluster G_Real -> non empty strict ;
coherence
not G_Real is empty
;
end;

registration
cluster G_Real -> non empty strict Abelian add-associative right_zeroed right_complementable ;
coherence
( G_Real is Abelian & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )
proof end;
end;

theorem Th1: :: VECTSP_1:1
canceled;

theorem Th2: :: VECTSP_1:2
canceled;

theorem Th3: :: VECTSP_1:3
canceled;

theorem Th4: :: VECTSP_1:4
canceled;

theorem Th5: :: VECTSP_1:5
canceled;

theorem Th6: :: VECTSP_1:6
for b1, b2, b3 being Element of G_Real holds
( b1 + b2 = b2 + b1 & (b1 + b2) + b3 = b1 + (b2 + b3) & b1 + (0. G_Real ) = b1 & b1 + (- b1) = 0. G_Real ) by RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 10;

registration
cluster non empty strict Abelian add-associative right_zeroed right_complementable LoopStr ;
existence
ex b1 being non empty LoopStr st
( b1 is strict & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian )
proof end;
end;

definition
mode AbGroup is non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
end;

theorem Th7: :: VECTSP_1:7
for b1 being non empty LoopStr holds
( ( for b2, b3, b4 being Element of b1 holds
( b2 + b3 = b3 + b2 & (b2 + b3) + b4 = b2 + (b3 + b4) & b2 + (0. b1) = b2 & ex b5 being Element of b1 st b2 + b5 = 0. b1 ) ) iff b1 is AbGroup ) by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

definition
attr a1 is strict;
struct multLoopStr -> HGrStr ;
aggr multLoopStr(# carrier, mult, unity #) -> multLoopStr ;
sel unity c1 -> Element of the carrier of a1;
end;

registration
cluster non empty strict multLoopStr ;
existence
ex b1 being multLoopStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let c1 be multLoopStr ;
canceled;
canceled;
func 1_ c1 -> Element of a1 equals :: VECTSP_1:def 9
the unity of a1;
coherence
the unity of c1 is Element of c1
;
end;

:: deftheorem Def7 VECTSP_1:def 7 :
canceled;

:: deftheorem Def8 VECTSP_1:def 8 :
canceled;

:: deftheorem Def9 defines 1_ VECTSP_1:def 9 :
for b1 being multLoopStr holds 1_ b1 = the unity of b1;

definition
attr a1 is strict;
struct multLoopStr_0 -> multLoopStr , ZeroStr ;
aggr multLoopStr_0(# carrier, mult, unity, Zero #) -> multLoopStr_0 ;
end;

registration
cluster non empty strict multLoopStr_0 ;
existence
ex b1 being multLoopStr_0 st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
attr a1 is strict;
struct doubleLoopStr -> LoopStr , multLoopStr_0 ;
aggr doubleLoopStr(# carrier, add, mult, unity, Zero #) -> doubleLoopStr ;
end;

registration
cluster non empty strict doubleLoopStr ;
existence
ex b1 being doubleLoopStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let c1 be non empty doubleLoopStr ;
canceled;
attr a1 is right-distributive means :Def11: :: VECTSP_1:def 11
for b1, b2, b3 being Element of a1 holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3);
attr a1 is left-distributive means :Def12: :: VECTSP_1:def 12
for b1, b2, b3 being Element of a1 holds (b2 + b3) * b1 = (b2 * b1) + (b3 * b1);
end;

:: deftheorem Def10 VECTSP_1:def 10 :
canceled;

:: deftheorem Def11 defines right-distributive VECTSP_1:def 11 :
for b1 being non empty doubleLoopStr holds
( b1 is right-distributive iff for b2, b3, b4 being Element of b1 holds b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) );

:: deftheorem Def12 defines left-distributive VECTSP_1:def 12 :
for b1 being non empty doubleLoopStr holds
( b1 is left-distributive iff for b2, b3, b4 being Element of b1 holds (b3 + b4) * b2 = (b3 * b2) + (b4 * b2) );

definition
let c1 be non empty multLoopStr ;
attr a1 is right_unital means :Def13: :: VECTSP_1:def 13
for b1 being Element of a1 holds b1 * (1. a1) = b1;
end;

:: deftheorem Def13 defines right_unital VECTSP_1:def 13 :
for b1 being non empty multLoopStr holds
( b1 is right_unital iff for b2 being Element of b1 holds b2 * (1. b1) = b2 );

definition
canceled;
func F_Real -> strict doubleLoopStr equals :: VECTSP_1:def 15
doubleLoopStr(# REAL ,addreal ,multreal ,1,0 #);
correctness
coherence
doubleLoopStr(# REAL ,addreal ,multreal ,1,0 #) is strict doubleLoopStr
;
;
end;

:: deftheorem Def14 VECTSP_1:def 14 :
canceled;

:: deftheorem Def15 defines F_Real VECTSP_1:def 15 :
F_Real = doubleLoopStr(# REAL ,addreal ,multreal ,1,0 #);

definition
let c1 be non empty doubleLoopStr ;
canceled;
canceled;
attr a1 is distributive means :Def18: :: VECTSP_1:def 18
for b1, b2, b3 being Element of a1 holds
( b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) & (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) );
end;

:: deftheorem Def16 VECTSP_1:def 16 :
canceled;

:: deftheorem Def17 VECTSP_1:def 17 :
canceled;

:: deftheorem Def18 defines distributive VECTSP_1:def 18 :
for b1 being non empty doubleLoopStr holds
( b1 is distributive iff for b2, b3, b4 being Element of b1 holds
( b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) & (b3 + b4) * b2 = (b3 * b2) + (b4 * b2) ) );

definition
let c1 be non empty multLoopStr ;
attr a1 is left_unital means :Def19: :: VECTSP_1:def 19
for b1 being Element of a1 holds (1. a1) * b1 = b1;
end;

:: deftheorem Def19 defines left_unital VECTSP_1:def 19 :
for b1 being non empty multLoopStr holds
( b1 is left_unital iff for b2 being Element of b1 holds (1. b1) * b2 = b2 );

definition
let c1 be non empty multLoopStr_0 ;
attr a1 is Field-like means :Def20: :: VECTSP_1:def 20
for b1 being Element of a1 st b1 <> 0. a1 holds
ex b2 being Element of a1 st b1 * b2 = 1. a1;
end;

:: deftheorem Def20 defines Field-like VECTSP_1:def 20 :
for b1 being non empty multLoopStr_0 holds
( b1 is Field-like iff for b2 being Element of b1 st b2 <> 0. b1 holds
ex b3 being Element of b1 st b2 * b3 = 1. b1 );

definition
let c1 be non empty multLoopStr_0 ;
attr a1 is degenerated means :Def21: :: VECTSP_1:def 21
0. a1 = 1. a1;
end;

:: deftheorem Def21 defines degenerated VECTSP_1:def 21 :
for b1 being non empty multLoopStr_0 holds
( b1 is degenerated iff 0. b1 = 1. b1 );

registration
cluster F_Real -> non empty strict ;
coherence
not F_Real is empty
proof end;
end;

set c1 = F_Real ;

E8: now
let c2, c3 be Element of F_Real ;
assume E9: c3 = 1 ;
reconsider c4 = c2 as Element of REAL ;
thus c2 * c3 = multreal . c2,c3
.= c4 * 1 by E9, BINOP_2:def 11
.= c2 ;
thus c3 * c2 = multreal . c3,c2
.= 1 * c4 by E9, BINOP_2:def 11
.= c2 ;
end;

registration
cluster F_Real -> non empty unital strict ;
coherence
F_Real is unital
proof end;
end;

Lemma9: 1. F_Real = 1
proof end;

registration
cluster F_Real -> non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict right_unital distributive left_unital Field-like non degenerated ;
coherence
( F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is Field-like & not F_Real is degenerated )
proof end;
end;

Lemma10: for b1 being non empty doubleLoopStr st b1 is distributive holds
( b1 is right-distributive & b1 is left-distributive )
proof end;

registration
cluster non empty distributive -> non empty right-distributive left-distributive doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is distributive holds
( b1 is left-distributive & b1 is right-distributive )
by Lemma10;
cluster non empty right-distributive left-distributive -> non empty distributive doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is left-distributive & b1 is right-distributive holds
b1 is distributive
proof end;
end;

registration
cluster non empty unital -> non empty right_unital left_unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is unital holds
( b1 is left_unital & b1 is right_unital )
proof end;
cluster non empty right_unital left_unital -> non empty unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is left_unital & b1 is right_unital holds
b1 is unital
proof end;
end;

registration
cluster non empty associative commutative HGrStr ;
existence
ex b1 being non empty HGrStr st
( b1 is commutative & b1 is associative )
proof end;
end;

registration
cluster non empty unital associative commutative right_unital left_unital multLoopStr ;
existence
ex b1 being non empty multLoopStr st
( b1 is commutative & b1 is associative & b1 is unital )
proof end;
end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict right-distributive left-distributive right_unital distributive left_unital Field-like non degenerated doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is left_unital & b1 is right_unital & b1 is distributive & b1 is Field-like & not b1 is degenerated & b1 is strict )
proof end;
end;

definition
mode Field is non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr ;
end;

theorem Th8: :: VECTSP_1:8
canceled;

theorem Th9: :: VECTSP_1:9
canceled;

theorem Th10: :: VECTSP_1:10
canceled;

theorem Th11: :: VECTSP_1:11
canceled;

theorem Th12: :: VECTSP_1:12
canceled;

theorem Th13: :: VECTSP_1:13
canceled;

theorem Th14: :: VECTSP_1:14
canceled;

theorem Th15: :: VECTSP_1:15
canceled;

theorem Th16: :: VECTSP_1:16
canceled;

theorem Th17: :: VECTSP_1:17
canceled;

theorem Th18: :: VECTSP_1:18
canceled;

theorem Th19: :: VECTSP_1:19
canceled;

theorem Th20: :: VECTSP_1:20
1. F_Real = 1 by Lemma9;

theorem Th21: :: VECTSP_1:21
for b1, b2, b3 being Element of F_Real holds
( b1 + b2 = b2 + b1 & (b1 + b2) + b3 = b1 + (b2 + b3) & b1 + (0. F_Real ) = b1 & b1 + (- b1) = 0. F_Real & b1 * b2 = b2 * b1 & (b1 * b2) * b3 = b1 * (b2 * b3) & (1. F_Real ) * b1 = b1 & ( b1 <> 0. F_Real implies ex b4 being Element of F_Real st b1 * b4 = 1. F_Real ) & b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) & (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) ) by Def18, Def19, Def20, GROUP_1:def 4, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 10;

theorem Th22: :: VECTSP_1:22
for b1 being non empty doubleLoopStr holds
( ( for b2, b3, b4 being Element of b1 holds
( ( b2 <> 0. b1 implies ex b5 being Element of b1 st b2 * b5 = 1. b1 ) & b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) & (b3 + b4) * b2 = (b3 * b2) + (b4 * b2) ) ) iff b1 is non empty distributive Field-like doubleLoopStr ) by Def18, Def20;

theorem Th23: :: VECTSP_1:23
canceled;

theorem Th24: :: VECTSP_1:24
canceled;

theorem Th25: :: VECTSP_1:25
canceled;

theorem Th26: :: VECTSP_1:26
canceled;

theorem Th27: :: VECTSP_1:27
canceled;

theorem Th28: :: VECTSP_1:28
canceled;

theorem Th29: :: VECTSP_1:29
canceled;

theorem Th30: :: VECTSP_1:30
canceled;

theorem Th31: :: VECTSP_1:31
canceled;

theorem Th32: :: VECTSP_1:32
canceled;

theorem Th33: :: VECTSP_1:33
for b1 being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for b2, b3, b4 being Element of b1 st b2 <> 0. b1 & b2 * b3 = b2 * b4 holds
b3 = b4
proof end;

definition
let c2 be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let c3 be Element of c2;
assume E12: c3 <> 0. c2 ;
func c2 " -> Element of a1 means :Def22: :: VECTSP_1:def 22
a2 * a3 = 1. a1;
existence
ex b1 being Element of c2 st c3 * b1 = 1. c2
by E12, Def20;
uniqueness
for b1, b2 being Element of c2 st c3 * b1 = 1. c2 & c3 * b2 = 1. c2 holds
b1 = b2
by E12, Th33;
end;

:: deftheorem Def22 defines " VECTSP_1:def 22 :
for b1 being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for b2 being Element of b1 st b2 <> 0. b1 holds
for b3 being Element of b1 holds
( b3 = b2 " iff b2 * b3 = 1. b1 );

definition
let c2 be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let c3, c4 be Element of c2;
func c2 / c3 -> Element of a1 equals :: VECTSP_1:def 23
a2 * (a3 " );
coherence
c3 * (c4 " ) is Element of c2
;
end;

:: deftheorem Def23 defines / VECTSP_1:def 23 :
for b1 being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for b2, b3 being Element of b1 holds b2 / b3 = b2 * (b3 " );

theorem Th34: :: VECTSP_1:34
canceled;

theorem Th35: :: VECTSP_1:35
canceled;

theorem Th36: :: VECTSP_1:36
for b1 being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b2 being Element of b1 holds b2 * (0. b1) = 0. b1
proof end;

theorem Th37: :: VECTSP_1:37
canceled;

theorem Th38: :: VECTSP_1:38
canceled;

theorem Th39: :: VECTSP_1:39
for b1 being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b2 being Element of b1 holds (0. b1) * b2 = 0. b1
proof end;

theorem Th40: :: VECTSP_1:40
for b1 being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b2, b3 being Element of b1 holds b2 * (- b3) = - (b2 * b3)
proof end;

theorem Th41: :: VECTSP_1:41
for b1 being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b2, b3 being Element of b1 holds (- b2) * b3 = - (b2 * b3)
proof end;

theorem Th42: :: VECTSP_1:42
for b1 being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b2, b3 being Element of b1 holds (- b2) * (- b3) = b2 * b3
proof end;

theorem Th43: :: VECTSP_1:43
for b1 being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b2, b3, b4 being Element of b1 holds b2 * (b3 - b4) = (b2 * b3) - (b2 * b4)
proof end;

theorem Th44: :: VECTSP_1:44
for b1 being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for b2, b3 being Element of b1 holds
( b2 * b3 = 0. b1 iff ( b2 = 0. b1 or b3 = 0. b1 ) )
proof end;

theorem Th45: :: VECTSP_1:45
for b1 being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b2, b3, b4 being Element of b1 holds (b2 - b3) * b4 = (b2 * b4) - (b3 * b4)
proof end;

definition
let c2 be 1-sorted ;
attr a2 is strict;
struct VectSpStr of c1 -> LoopStr ;
aggr VectSpStr(# carrier, add, Zero, lmult #) -> VectSpStr of a1;
sel lmult c2 -> Function of [:the carrier of a1,the carrier of a2:],the carrier of a2;
end;

registration
let c2 be 1-sorted ;
cluster non empty strict VectSpStr of a1;
existence
ex b1 being VectSpStr of c2 st
( not b1 is empty & b1 is strict )
proof end;
end;

registration
let c2 be 1-sorted ;
let c3 be non empty set ;
let c4 be BinOp of c3;
let c5 be Element of c3;
let c6 be Function of [:the carrier of c2,c3:],c3;
cluster VectSpStr(# a2,a3,a4,a5 #) -> non empty ;
coherence
not VectSpStr(# c3,c4,c5,c6 #) is empty
proof end;
end;

definition
let c2 be 1-sorted ;
mode Scalar of a1 is Element of a1;
end;

definition
let c2 be 1-sorted ;
let c3 be VectSpStr of c2;
mode Scalar of a2 is Scalar of a1;
mode Vector of a2 is Element of a2;
end;

definition
let c2 be non empty 1-sorted ;
let c3 be non empty VectSpStr of c2;
let c4 be Element of c2;
let c5 be Element of c3;
func c3 * c4 -> Element of a2 equals :: VECTSP_1:def 24
the lmult of a2 . a3,a4;
coherence
the lmult of c3 . c4,c5 is Element of c3
;
end;

:: deftheorem Def24 defines * VECTSP_1:def 24 :
for b1 being non empty 1-sorted
for b2 being non empty VectSpStr of b1
for b3 being Element of b1
for b4 being Element of b2 holds b3 * b4 = the lmult of b2 . b3,b4;

definition
let c2 be non empty LoopStr ;
func comp c1 -> UnOp of the carrier of a1 means :: VECTSP_1:def 25
for b1 being Element of a1 holds a2 . b1 = - b1;
existence
ex b1 being UnOp of the carrier of c2 st
for b2 being Element of c2 holds b1 . b2 = - b2
proof end;
uniqueness
for b1, b2 being UnOp of the carrier of c2 st ( for b3 being Element of c2 holds b1 . b3 = - b3 ) & ( for b3 being Element of c2 holds b2 . b3 = - b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines comp VECTSP_1:def 25 :
for b1 being non empty LoopStr
for b2 being UnOp of the carrier of b1 holds
( b2 = comp b1 iff for b3 being Element of b1 holds b2 . b3 = - b3 );

E19: now
let c2 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c3 be Function of [:the carrier of c2,the carrier of c2:],the carrier of c2;
set c4 = VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #);
for b1, b2, b3 being Element of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) holds
( b1 + b2 = b2 + b1 & (b1 + b2) + b3 = b1 + (b2 + b3) & b1 + (0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #)) = b1 & ex b4 being Element of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) st b1 + b4 = 0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) )
proof
let c5, c6, c7 be Element of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #);
reconsider c8 = c5, c9 = c6, c10 = c7 as Element of c2 ;
thus c5 + c6 = the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c6 by RLVECT_1:5
.= c9 + c8 by RLVECT_1:5
.= the add of c2 . c9,c8 by RLVECT_1:5
.= c6 + c5 by RLVECT_1:5 ;
thus (c5 + c6) + c7 = the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . (c5 + c6),c7 by RLVECT_1:5
.= the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . (the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c6),c7 by RLVECT_1:5
.= the add of c2 . (c8 + c9),c10 by RLVECT_1:5
.= (c8 + c9) + c10 by RLVECT_1:5
.= c8 + (c9 + c10) by RLVECT_1:def 6
.= the add of c2 . c8,(c9 + c10) by RLVECT_1:5
.= the add of c2 . c8,(the add of c2 . c9,c10) by RLVECT_1:5
.= the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,(c6 + c7) by RLVECT_1:5
.= c5 + (c6 + c7) by RLVECT_1:5 ;
thus c5 + (0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #)) = the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,(0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #)) by RLVECT_1:5
.= the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,the Zero of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #)
.= c8 + (0. c2) by RLVECT_1:5
.= c5 by RLVECT_1:10 ;
consider c11 being Element of c2 such that
E20: c8 + c11 = 0. c2 by RLVECT_1:def 8;
reconsider c12 = c11 as Element of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) ;
take c12 ;
thus c5 + c12 = the add of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c12 by RLVECT_1:5
.= c8 + c11 by RLVECT_1:5
.= 0. VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) by E20 ;
end;
hence VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) is AbGroup by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;
end;

E20: now
let c2 be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c3 be Function of [:the carrier of c2,the carrier of c2:],the carrier of c2;
assume E21: c3 = the mult of c2 ;
set c4 = VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #);
let c5, c6 be Element of c2;
let c7, c8 be Element of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #);
reconsider c9 = c7, c10 = c8 as Element of c2 ;
thus c5 * (c7 + c8) = the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,(c7 + c8)
.= c3 . c5,(the add of c2 . c9,c10) by RLVECT_1:5
.= c3 . c5,(c9 + c10) by RLVECT_1:5
.= c5 * (c9 + c10) by E21
.= (c5 * c9) + (c5 * c10) by Def18
.= the add of c2 . (c5 * c9),(c5 * c10) by RLVECT_1:5
.= the add of c2 . (c3 . c5,c9),(c5 * c10) by E21
.= the add of c2 . (the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c7),(the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c8) by E21
.= the add of c2 . (c5 * c7),(c5 * c8)
.= (c5 * c7) + (c5 * c8) by RLVECT_1:5 ;
thus (c5 + c6) * c7 = the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . (c5 + c6),c7
.= (c5 + c6) * c9 by E21
.= (c5 * c9) + (c6 * c9) by Def18
.= the add of c2 . (c5 * c9),(c6 * c9) by RLVECT_1:5
.= the add of c2 . (c3 . c5,c9),(c6 * c9) by E21
.= the add of c2 . (the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,c7),(the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c6,c7) by E21
.= the add of c2 . (c5 * c7),(c6 * c7)
.= (c5 * c7) + (c6 * c7) by RLVECT_1:5 ;
thus (c5 * c6) * c7 = the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . (c5 * c6),c7
.= (c5 * c6) * c9 by E21
.= c5 * (c6 * c9) by GROUP_1:def 4
.= c3 . c5,(c6 * c9) by E21
.= the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,(the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c6,c7) by E21
.= the lmult of VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,c3 #) . c5,(c6 * c7)
.= c5 * (c6 * c7) ;
thus (1. c2) * c7 = c3 . (1. c2),c9
.= (1. c2) * c9 by E21
.= c7 by Def19 ;
end;

definition
let c2 be non empty doubleLoopStr ;
let c3 be non empty VectSpStr of c2;
attr a2 is VectSp-like means :Def26: :: VECTSP_1:def 26
for b1, b2 being Element of a1
for b3, b4 being Element of a2 holds
( b1 * (b3 + b4) = (b1 * b3) + (b1 * b4) & (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) & (b1 * b2) * b3 = b1 * (b2 * b3) & (1. a1) * b3 = b3 );
end;

:: deftheorem Def26 defines VectSp-like VECTSP_1:def 26 :
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1 holds
( b2 is VectSp-like iff for b3, b4 being Element of b1
for b5, b6 being Element of b2 holds
( b3 * (b5 + b6) = (b3 * b5) + (b3 * b6) & (b3 + b4) * b5 = (b3 * b5) + (b4 * b5) & (b3 * b4) * b5 = b3 * (b4 * b5) & (1. b1) * b5 = b5 ) );

registration
let c2 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of a1;
existence
ex b1 being non empty VectSpStr of c2 st
( b1 is VectSp-like & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is strict )
proof end;
end;

definition
let c2 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
mode VectSp of a1 is non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of a1;
end;

theorem Th46: :: VECTSP_1:46
canceled;

theorem Th47: :: VECTSP_1:47
canceled;

theorem Th48: :: VECTSP_1:48
canceled;

theorem Th49: :: VECTSP_1:49
canceled;

theorem Th50: :: VECTSP_1:50
canceled;

theorem Th51: :: VECTSP_1:51
canceled;

theorem Th52: :: VECTSP_1:52
canceled;

theorem Th53: :: VECTSP_1:53
canceled;

theorem Th54: :: VECTSP_1:54
canceled;

theorem Th55: :: VECTSP_1:55
canceled;

theorem Th56: :: VECTSP_1:56
canceled;

theorem Th57: :: VECTSP_1:57
canceled;

theorem Th58: :: VECTSP_1:58
canceled;

theorem Th59: :: VECTSP_1:59
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being Element of b1
for b3 being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b4 being Element of b3 holds
( (0. b1) * b4 = 0. b3 & (- (1. b1)) * b4 = - b4 & b2 * (0. b3) = 0. b3 )
proof end;

theorem Th60: :: VECTSP_1:60
for b1 being Field
for b2 being Element of b1
for b3 being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b4 being Element of b3 holds
( b2 * b4 = 0. b3 iff ( b2 = 0. b1 or b4 = 0. b3 ) )
proof end;

theorem Th61: :: VECTSP_1:61
canceled;

theorem Th62: :: VECTSP_1:62
canceled;

theorem Th63: :: VECTSP_1:63
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds
( b2 + b3 = 0. b1 iff - b2 = b3 )
proof end;

Lemma23: for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - (b3 + (- b2)) = b2 - b3
proof end;

Lemma24: for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - ((- b2) - b3) = b3 + b2
proof end;

theorem Th64: :: VECTSP_1:64
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Element of b1 holds
( - (b3 + b4) = (- b4) - b3 & - (b4 + (- b3)) = b3 - b4 & - (b3 - b4) = b4 + (- b3) & - ((- b3) - b4) = b4 + b3 & b2 - (b4 + b3) = (b2 - b3) - b4 ) by Lemma23, Lemma24, RLVECT_1:41, RLVECT_1:44, RLVECT_1:47;

theorem Th65: :: VECTSP_1:65
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2 being Element of b1 holds
( (0. b1) - b2 = - b2 & b2 - (0. b1) = b2 ) by RLVECT_1:26, RLVECT_1:27;

theorem Th66: :: VECTSP_1:66
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds
( ( b2 + (- b3) = 0. b1 implies b2 = b3 ) & ( b2 = b3 implies b2 + (- b3) = 0. b1 ) & ( b2 - b3 = 0. b1 implies b2 = b3 ) & ( b2 = b3 implies b2 - b3 = 0. b1 ) )
proof end;

theorem Th67: :: VECTSP_1:67
for b1 being Field
for b2 being Element of b1
for b3 being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b4 being Element of b3 st b2 <> 0. b1 holds
(b2 " ) * (b2 * b4) = b4
proof end;

theorem Th68: :: VECTSP_1:68
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4, b5 being Element of b2 holds
( - (b3 * b4) = (- b3) * b4 & b5 - (b3 * b4) = b5 + ((- b3) * b4) )
proof end;

registration
cluster non empty commutative left_unital -> non empty right_unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is commutative & b1 is left_unital holds
b1 is right_unital
proof end;
end;

theorem Th69: :: VECTSP_1:69
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4 being Element of b2 holds b3 * (- b4) = - (b3 * b4)
proof end;

theorem Th70: :: VECTSP_1:70
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4, b5 being Element of b2 holds b3 * (b4 - b5) = (b3 * b4) - (b3 * b5)
proof end;

theorem Th71: :: VECTSP_1:71
canceled;

theorem Th72: :: VECTSP_1:72
canceled;

theorem Th73: :: VECTSP_1:73
for b1 being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for b2 being Element of b1 st b2 <> 0. b1 holds
(b2 " ) " = b2
proof end;

theorem Th74: :: VECTSP_1:74
for b1 being Field
for b2 being Element of b1 st b2 <> 0. b1 holds
( b2 " <> 0. b1 & - (b2 " ) <> 0. b1 )
proof end;

theorem Th75: :: VECTSP_1:75
canceled;

theorem Th76: :: VECTSP_1:76
canceled;

theorem Th77: :: VECTSP_1:77
canceled;

theorem Th78: :: VECTSP_1:78
(1. F_Real ) + (1. F_Real ) <> 0. F_Real
proof end;

definition
let c2 be non empty LoopStr ;
canceled;
attr a1 is Fanoian means :Def28: :: VECTSP_1:def 28
for b1 being Element of a1 st b1 + b1 = 0. a1 holds
b1 = 0. a1;
end;

:: deftheorem Def27 VECTSP_1:def 27 :
canceled;

:: deftheorem Def28 defines Fanoian VECTSP_1:def 28 :
for b1 being non empty LoopStr holds
( b1 is Fanoian iff for b2 being Element of b1 st b2 + b2 = 0. b1 holds
b2 = 0. b1 );

registration
cluster non empty Fanoian LoopStr ;
existence
ex b1 being non empty LoopStr st b1 is Fanoian
proof end;
end;

definition
let c2 be non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr ;
redefine attr a1 is Fanoian means :Def29: :: VECTSP_1:def 29
(1. a1) + (1. a1) <> 0. a1;
compatibility
( c2 is Fanoian iff (1. c2) + (1. c2) <> 0. c2 )
proof end;
end;

:: deftheorem Def29 defines Fanoian VECTSP_1:def 29 :
for b1 being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr holds
( b1 is Fanoian iff (1. b1) + (1. b1) <> 0. b1 );

registration
cluster unital strict right_unital Fanoian doubleLoopStr ;
existence
ex b1 being Field st
( b1 is strict & b1 is Fanoian )
proof end;
end;

theorem Th79: :: VECTSP_1:79
canceled;

theorem Th80: :: VECTSP_1:80
canceled;

theorem Th81: :: VECTSP_1:81
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - (b2 - b3) = b3 - b2 by RLVECT_1:47;

theorem Th82: :: VECTSP_1:82
canceled;

theorem Th83: :: VECTSP_1:83
canceled;

theorem Th84: :: VECTSP_1:84
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 st b2 - b3 = 0. b1 holds
b2 = b3 by Th66;

theorem Th85: :: VECTSP_1:85
canceled;

theorem Th86: :: VECTSP_1:86
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2 being Element of b1 st - b2 = 0. b1 holds
b2 = 0. b1
proof end;

theorem Th87: :: VECTSP_1:87
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 st b2 - b3 = 0. b1 holds
b3 - b2 = 0. b1
proof end;

theorem Th88: :: VECTSP_1:88
for b1 being Field
for b2, b3, b4 being Element of b1 holds
( ( b2 <> 0. b1 & (b2 * b4) - b3 = 0. b1 implies b4 = b3 * (b2 " ) ) & ( b2 <> 0. b1 & b3 - (b4 * b2) = 0. b1 implies b4 = b3 * (b2 " ) ) )
proof end;

theorem Th89: :: VECTSP_1:89
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds b2 + b3 = - ((- b3) + (- b2))
proof end;

theorem Th90: :: VECTSP_1:90
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Element of b1 holds (b3 + b2) - (b4 + b2) = b3 - b4
proof end;

theorem Th91: :: VECTSP_1:91
canceled;

theorem Th92: :: VECTSP_1:92
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - ((- b2) + b3) = (- b3) + b2
proof end;

theorem Th93: :: VECTSP_1:93
for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Element of b1 holds (b2 - b3) - b4 = (b2 - b4) - b3
proof end;

theorem Th94: :: VECTSP_1:94
for b1 being AbGroup holds HGrStr(# the carrier of b1,the add of b1 #) is commutative Group
proof end;