:: VECTSP_1 semantic presentation

defpred S₁[ Element of REAL , set ] means a₂ = - a₁;

definition

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

end;

:: deftheorem Def1 VECTSP_1:def 1 :

:: deftheorem Def2 VECTSP_1:def 2 :

:: deftheorem Def3 VECTSP_1:def 3 :

:: deftheorem Def4 VECTSP_1:def 4 :

:: deftheorem Def5 VECTSP_1:def 5 :

:: deftheorem Def6 defines G_Real VECTSP_1:def 6 :

registration

cluster G_Real -> non empty strict ;
coherence ;

end;

registration

cluster G_Real -> non empty strict Abelian add-associative right_zeroed right_complementable ;
coherence

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 b₁, b₂, b₃ being Element of G_Real holds
( b₁ + b₂ = b₂ + b₁ & (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃) & b₁ + (0. G_Real ) = b₁ & b₁ + (- b₁) = 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

proof end;

end;

definition

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

end;

theorem Th7: :: VECTSP_1:7

for b₁ being non empty LoopStr holds
( ( for b₂, b₃, b₄ being Element of b₁ holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. b₁) = b₂ & ex b₅ being Element of b₁ st b₂ + b₅ = 0. b₁ ) ) iff b₁ is AbGroup ) by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

definition

attr a₁ is strict;
struct multLoopStr -> HGrStr ;
aggr multLoopStr(# carrier, mult, unity #) -> multLoopStr ;
sel unity c₁ -> Element of the carrier of a₁;

end;

registration

cluster non empty strict multLoopStr ;
existence

proof end;

end;

definition

let c₁ be multLoopStr ;
canceled;
canceled;
func 1_ c₁ -> Element of a₁ equals :: VECTSP_1:def 9
the unity of a₁;
coherence ;

end;

:: deftheorem Def7 VECTSP_1:def 7 :

:: deftheorem Def8 VECTSP_1:def 8 :

:: deftheorem Def9 defines 1_ VECTSP_1:def 9 :

definition

attr a₁ 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

proof end;

end;

definition

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

end;

registration

cluster non empty strict doubleLoopStr ;
existence

proof end;

end;

definition

let c₁ be non empty doubleLoopStr ;
canceled;
attr a₁ is right-distributive means :Def11: :: VECTSP_1:def 11
for b₁, b₂, b₃ being Element of a₁ holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃);
attr a₁ is left-distributive means :Def12: :: VECTSP_1:def 12
for b₁, b₂, b₃ being Element of a₁ holds (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁);

end;

:: deftheorem Def10 VECTSP_1:def 10 :

:: deftheorem Def11 defines right-distributive VECTSP_1:def 11 :

:: deftheorem Def12 defines left-distributive VECTSP_1:def 12 :

definition

let c₁ be non empty multLoopStr ;
attr a₁ is right_unital means :Def13: :: VECTSP_1:def 13
for b₁ being Element of a₁ holds b₁ * (1. a₁) = b₁;

end;

:: deftheorem Def13 defines right_unital VECTSP_1:def 13 :

definition

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

end;

:: deftheorem Def14 VECTSP_1:def 14 :

:: deftheorem Def15 defines F_Real VECTSP_1:def 15 :

definition

let c₁ be non empty doubleLoopStr ;
canceled;
canceled;
attr a₁ is distributive means :Def18: :: VECTSP_1:def 18
for b₁, b₂, b₃ being Element of a₁ holds
( b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) );

end;

:: deftheorem Def16 VECTSP_1:def 16 :

:: deftheorem Def17 VECTSP_1:def 17 :

:: deftheorem Def18 defines distributive VECTSP_1:def 18 :

definition

let c₁ be non empty multLoopStr ;
attr a₁ is left_unital means :Def19: :: VECTSP_1:def 19
for b₁ being Element of a₁ holds (1. a₁) * b₁ = b₁;

end;

:: deftheorem Def19 defines left_unital VECTSP_1:def 19 :

definition

let c₁ be non empty multLoopStr_0 ;
attr a₁ is Field-like means :Def20: :: VECTSP_1:def 20
for b₁ being Element of a₁ st b₁ <> 0. a₁ holds
ex b₂ being Element of a₁ st b₁ * b₂ = 1. a₁;

end;

:: deftheorem Def20 defines Field-like VECTSP_1:def 20 :

definition

let c₁ be non empty multLoopStr_0 ;
attr a₁ is degenerated means :Def21: :: VECTSP_1:def 21
0. a₁ = 1. a₁;

end;

:: deftheorem Def21 defines degenerated VECTSP_1:def 21 :

registration

cluster F_Real -> non empty strict ;
coherence

proof end;

end;

set c₁ = F_Real ;

E8: now

let c₂, c₃ be Element of F_Real ;
assume E9: c₃ = 1 ;
reconsider c₄ = c₂ as Element of REAL ;
thus c₂ * c₃ = multreal . c₂,c₃
.= c₄ * 1 by E9, BINOP_2:def 11
.= c₂ ;
thus c₃ * c₂ = multreal . c₃,c₂
.= 1 * c₄ by E9, BINOP_2:def 11
.= c₂ ;

end;

registration

cluster F_Real -> non empty unital strict ;
coherence

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

proof end;

end;

Lemma10: for b₁ being non empty doubleLoopStr st b₁ is distributive holds
( b₁ is right-distributive & b₁ is left-distributive )

proof end;

registration

cluster non empty distributive -> non empty right-distributive left-distributive doubleLoopStr ;
coherence by Lemma10;
cluster non empty right-distributive left-distributive -> non empty distributive doubleLoopStr ;
coherence

proof end;

end;

registration

cluster non empty unital -> non empty right_unital left_unital multLoopStr ;
coherence

proof end;

cluster non empty right_unital left_unital -> non empty unital multLoopStr ;
coherence

proof end;

end;

registration

cluster non empty associative commutative HGrStr ;
existence

proof end;

end;

registration

cluster non empty unital associative commutative right_unital left_unital multLoopStr ;
existence

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

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 b₁, b₂, b₃ being Element of F_Real holds
( b₁ + b₂ = b₂ + b₁ & (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃) & b₁ + (0. F_Real ) = b₁ & b₁ + (- b₁) = 0. F_Real & b₁ * b₂ = b₂ * b₁ & (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) & (1. F_Real ) * b₁ = b₁ & ( b₁ <> 0. F_Real implies ex b₄ being Element of F_Real st b₁ * b₄ = 1. F_Real ) & b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) ) 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 b₁ being non empty doubleLoopStr holds
( ( for b₂, b₃, b₄ being Element of b₁ holds
( ( b₂ <> 0. b₁ implies ex b₅ being Element of b₁ st b₂ * b₅ = 1. b₁ ) & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) ) ) iff b₁ 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 b₁ being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄

proof end;

definition

let c₂ be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let c₃ be Element of c₂;
assume E12: c₃ <> 0. c₂ ;
func c₂ " -> Element of a₁ means :Def22: :: VECTSP_1:def 22
a₂ * a₃ = 1. a₁;
existence by E12, Def20;
uniqueness by E12, Th33;

end;

:: deftheorem Def22 defines " VECTSP_1:def 22 :

definition

let c₂ be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let c₃, c₄ be Element of c₂;
func c₂ / c₃ -> Element of a₁ equals :: VECTSP_1:def 23
a₂ * (a₃ " );
coherence ;

end;

:: deftheorem Def23 defines / VECTSP_1:def 23 :

theorem Th34: :: VECTSP_1:34

canceled;

theorem Th35: :: VECTSP_1:35

canceled;

theorem Th36: :: VECTSP_1:36

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁

proof end;

theorem Th37: :: VECTSP_1:37

canceled;

theorem Th38: :: VECTSP_1:38

canceled;

theorem Th39: :: VECTSP_1:39

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁

proof end;

theorem Th40: :: VECTSP_1:40

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃ being Element of b₁ holds b₂ * (- b₃) = - (b₂ * b₃)

proof end;

theorem Th41: :: VECTSP_1:41

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃ being Element of b₁ holds (- b₂) * b₃ = - (b₂ * b₃)

proof end;

theorem Th42: :: VECTSP_1:42

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Element of b₁ holds (- b₂) * (- b₃) = b₂ * b₃

proof end;

theorem Th43: :: VECTSP_1:43

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ * (b₃ - b₄) = (b₂ * b₃) - (b₂ * b₄)

proof end;

theorem Th44: :: VECTSP_1:44

for b₁ being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for b₂, b₃ being Element of b₁ holds
( b₂ * b₃ = 0. b₁ iff ( b₂ = 0. b₁ or b₃ = 0. b₁ ) )

proof end;

theorem Th45: :: VECTSP_1:45

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ - b₃) * b₄ = (b₂ * b₄) - (b₃ * b₄)

proof end;

definition

let c₂ be 1-sorted ;
attr a₂ is strict;
struct VectSpStr of c₁ -> LoopStr ;
aggr VectSpStr(# carrier, add, Zero, lmult #) -> VectSpStr of a₁;
sel lmult c₂ -> Function of [:the carrier of a₁,the carrier of a₂:],the carrier of a₂;

end;

registration

let c₂ be 1-sorted ;
cluster non empty strict VectSpStr of a₁;
existence

proof end;

end;

registration

let c₂ be 1-sorted ;
let c₃ be non empty set ;
let c₄ be BinOp of c₃;
let c₅ be Element of c₃;
let c₆ be Function of [:the carrier of c₂,c₃:],c₃;
cluster VectSpStr(# a₂,a₃,a₄,a₅ #) -> non empty ;
coherence

proof end;

end;

definition

let c₂ be 1-sorted ;
mode Scalar of a₁ is Element of a₁;

end;

definition

let c₂ be 1-sorted ;
let c₃ be VectSpStr of c₂;
mode Scalar of a₂ is Scalar of a₁;
mode Vector of a₂ is Element of a₂;

end;

definition

let c₂ be non empty 1-sorted ;
let c₃ be non empty VectSpStr of c₂;
let c₄ be Element of c₂;
let c₅ be Element of c₃;
func c₃ * c₄ -> Element of a₂ equals :: VECTSP_1:def 24
the lmult of a₂ . a₃,a₄;
coherence ;

end;

:: deftheorem Def24 defines * VECTSP_1:def 24 :

definition

let c₂ be non empty LoopStr ;
func comp c₁ -> UnOp of the carrier of a₁ means :: VECTSP_1:def 25
for b₁ being Element of a₁ holds a₂ . b₁ = - b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def25 defines comp VECTSP_1:def 25 :

E19: now

let c₂ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₃ be Function of [:the carrier of c₂,the carrier of c₂:],the carrier of c₂;
set c₄ = VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #);
for b₁, b₂, b₃ being Element of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) holds
( b₁ + b₂ = b₂ + b₁ & (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃) & b₁ + (0. VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #)) = b₁ & ex b₄ being Element of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) st b₁ + b₄ = 0. VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) )

proof

let c₅, c₆, c₇ be Element of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #);
reconsider c₈ = c₅, c₉ = c₆, c₁₀ = c₇ as Element of c₂ ;
thus c₅ + c₆ = the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,c₆ by RLVECT_1:5
.= c₉ + c₈ by RLVECT_1:5
.= the add of c₂ . c₉,c₈ by RLVECT_1:5
.= c₆ + c₅ by RLVECT_1:5 ;
thus (c₅ + c₆) + c₇ = the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . (c₅ + c₆),c₇ by RLVECT_1:5
.= the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . (the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,c₆),c₇ by RLVECT_1:5
.= the add of c₂ . (c₈ + c₉),c₁₀ by RLVECT_1:5
.= (c₈ + c₉) + c₁₀ by RLVECT_1:5
.= c₈ + (c₉ + c₁₀) by RLVECT_1:def 6
.= the add of c₂ . c₈,(c₉ + c₁₀) by RLVECT_1:5
.= the add of c₂ . c₈,(the add of c₂ . c₉,c₁₀) by RLVECT_1:5
.= the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,(c₆ + c₇) by RLVECT_1:5
.= c₅ + (c₆ + c₇) by RLVECT_1:5 ;
thus c₅ + (0. VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #)) = the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,(0. VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #)) by RLVECT_1:5
.= the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,the Zero of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #)
.= c₈ + (0. c₂) by RLVECT_1:5
.= c₅ by RLVECT_1:10 ;
consider c₁₁ being Element of c₂ such that
E20: c₈ + c₁₁ = 0. c₂ by RLVECT_1:def 8;
reconsider c₁₂ = c₁₁ as Element of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) ;
take c₁₂ ;
thus c₅ + c₁₂ = the add of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,c₁₂ by RLVECT_1:5
.= c₈ + c₁₁ by RLVECT_1:5
.= 0. VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) by E20 ;

end;

hence VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) is AbGroup by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

end;

E20: now

let c₂ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₃ be Function of [:the carrier of c₂,the carrier of c₂:],the carrier of c₂;
assume E21: c₃ = the mult of c₂ ;
set c₄ = VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #);
let c₅, c₆ be Element of c₂;
let c₇, c₈ be Element of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #);
reconsider c₉ = c₇, c₁₀ = c₈ as Element of c₂ ;
thus c₅ * (c₇ + c₈) = the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,(c₇ + c₈)
.= c₃ . c₅,(the add of c₂ . c₉,c₁₀) by RLVECT_1:5
.= c₃ . c₅,(c₉ + c₁₀) by RLVECT_1:5
.= c₅ * (c₉ + c₁₀) by E21
.= (c₅ * c₉) + (c₅ * c₁₀) by Def18
.= the add of c₂ . (c₅ * c₉),(c₅ * c₁₀) by RLVECT_1:5
.= the add of c₂ . (c₃ . c₅,c₉),(c₅ * c₁₀) by E21
.= the add of c₂ . (the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,c₇),(the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,c₈) by E21
.= the add of c₂ . (c₅ * c₇),(c₅ * c₈)
.= (c₅ * c₇) + (c₅ * c₈) by RLVECT_1:5 ;
thus (c₅ + c₆) * c₇ = the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . (c₅ + c₆),c₇
.= (c₅ + c₆) * c₉ by E21
.= (c₅ * c₉) + (c₆ * c₉) by Def18
.= the add of c₂ . (c₅ * c₉),(c₆ * c₉) by RLVECT_1:5
.= the add of c₂ . (c₃ . c₅,c₉),(c₆ * c₉) by E21
.= the add of c₂ . (the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,c₇),(the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₆,c₇) by E21
.= the add of c₂ . (c₅ * c₇),(c₆ * c₇)
.= (c₅ * c₇) + (c₆ * c₇) by RLVECT_1:5 ;
thus (c₅ * c₆) * c₇ = the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . (c₅ * c₆),c₇
.= (c₅ * c₆) * c₉ by E21
.= c₅ * (c₆ * c₉) by GROUP_1:def 4
.= c₃ . c₅,(c₆ * c₉) by E21
.= the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,(the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₆,c₇) by E21
.= the lmult of VectSpStr(# the carrier of c₂,the add of c₂,the Zero of c₂,c₃ #) . c₅,(c₆ * c₇)
.= c₅ * (c₆ * c₇) ;
thus (1. c₂) * c₇ = c₃ . (1. c₂),c₉
.= (1. c₂) * c₉ by E21
.= c₇ by Def19 ;

end;

definition

let c₂ be non empty doubleLoopStr ;
let c₃ be non empty VectSpStr of c₂;
attr a₂ is VectSp-like means :Def26: :: VECTSP_1:def 26
for b₁, b₂ being Element of a₁
for b₃, b₄ being Element of a₂ holds
( b₁ * (b₃ + b₄) = (b₁ * b₃) + (b₁ * b₄) & (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) & (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) & (1. a₁) * b₃ = b₃ );

end;

:: deftheorem Def26 defines VectSp-like VECTSP_1:def 26 :

registration

let c₂ 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 a₁;
existence

proof end;

end;

definition

let c₂ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
mode VectSp of a₁ is non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of a₁;

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 b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄ being Element of b₃ holds
( (0. b₁) * b₄ = 0. b₃ & (- (1. b₁)) * b₄ = - b₄ & b₂ * (0. b₃) = 0. b₃ )

proof end;

theorem Th60: :: VECTSP_1:60

for b₁ being Field
for b₂ being Element of b₁
for b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄ being Element of b₃ holds
( b₂ * b₄ = 0. b₃ iff ( b₂ = 0. b₁ or b₄ = 0. b₃ ) )

proof end;

theorem Th61: :: VECTSP_1:61

canceled;

theorem Th62: :: VECTSP_1:62

canceled;

theorem Th63: :: VECTSP_1:63

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds
( b₂ + b₃ = 0. b₁ iff - b₂ = b₃ )

proof end;

Lemma23: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (b₃ + (- b₂)) = b₂ - b₃

proof end;

Lemma24: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - ((- b₂) - b₃) = b₃ + b₂

proof end;

theorem Th64: :: VECTSP_1:64

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds
( - (b₃ + b₄) = (- b₄) - b₃ & - (b₄ + (- b₃)) = b₃ - b₄ & - (b₃ - b₄) = b₄ + (- b₃) & - ((- b₃) - b₄) = b₄ + b₃ & b₂ - (b₄ + b₃) = (b₂ - b₃) - b₄ ) by Lemma23, Lemma24, RLVECT_1:41, RLVECT_1:44, RLVECT_1:47;

theorem Th65: :: VECTSP_1:65

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds
( (0. b₁) - b₂ = - b₂ & b₂ - (0. b₁) = b₂ ) by RLVECT_1:26, RLVECT_1:27;

theorem Th66: :: VECTSP_1:66

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds
( ( b₂ + (- b₃) = 0. b₁ implies b₂ = b₃ ) & ( b₂ = b₃ implies b₂ + (- b₃) = 0. b₁ ) & ( b₂ - b₃ = 0. b₁ implies b₂ = b₃ ) & ( b₂ = b₃ implies b₂ - b₃ = 0. b₁ ) )

proof end;

theorem Th67: :: VECTSP_1:67

for b₁ being Field
for b₂ being Element of b₁
for b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄ being Element of b₃ st b₂ <> 0. b₁ holds
(b₂ " ) * (b₂ * b₄) = b₄

proof end;

theorem Th68: :: VECTSP_1:68

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₁
for b₄, b₅ being Element of b₂ holds
( - (b₃ * b₄) = (- b₃) * b₄ & b₅ - (b₃ * b₄) = b₅ + ((- b₃) * b₄) )

proof end;

registration

cluster non empty commutative left_unital -> non empty right_unital multLoopStr ;
coherence

proof end;

end;

theorem Th69: :: VECTSP_1:69

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₁
for b₄ being Element of b₂ holds b₃ * (- b₄) = - (b₃ * b₄)

proof end;

theorem Th70: :: VECTSP_1:70

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₁
for b₄, b₅ being Element of b₂ holds b₃ * (b₄ - b₅) = (b₃ * b₄) - (b₃ * b₅)

proof end;

theorem Th71: :: VECTSP_1:71

canceled;

theorem Th72: :: VECTSP_1:72

canceled;

theorem Th73: :: VECTSP_1:73

for b₁ being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
(b₂ " ) " = b₂

proof end;

theorem Th74: :: VECTSP_1:74

for b₁ being Field
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
( b₂ " <> 0. b₁ & - (b₂ " ) <> 0. b₁ )

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 c₂ be non empty LoopStr ;
canceled;
attr a₁ is Fanoian means :Def28: :: VECTSP_1:def 28
for b₁ being Element of a₁ st b₁ + b₁ = 0. a₁ holds
b₁ = 0. a₁;

end;

:: deftheorem Def27 VECTSP_1:def 27 :

:: deftheorem Def28 defines Fanoian VECTSP_1:def 28 :

registration

cluster non empty Fanoian LoopStr ;
existence

proof end;

end;

definition

let c₂ be non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr ;
redefine attr a₁ is Fanoian means :Def29: :: VECTSP_1:def 29
(1. a₁) + (1. a₁) <> 0. a₁;
compatibility

proof end;

end;

:: deftheorem Def29 defines Fanoian VECTSP_1:def 29 :

registration

cluster unital strict right_unital Fanoian doubleLoopStr ;
existence

proof end;

end;

theorem Th79: :: VECTSP_1:79

canceled;

theorem Th80: :: VECTSP_1:80

canceled;

theorem Th81: :: VECTSP_1:81

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (b₂ - b₃) = b₃ - b₂ by RLVECT_1:47;

theorem Th82: :: VECTSP_1:82

canceled;

theorem Th83: :: VECTSP_1:83

canceled;

theorem Th84: :: VECTSP_1:84

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ - b₃ = 0. b₁ holds
b₂ = b₃ by Th66;

theorem Th85: :: VECTSP_1:85

canceled;

theorem Th86: :: VECTSP_1:86

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ st - b₂ = 0. b₁ holds
b₂ = 0. b₁

proof end;

theorem Th87: :: VECTSP_1:87

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ - b₃ = 0. b₁ holds
b₃ - b₂ = 0. b₁

proof end;

theorem Th88: :: VECTSP_1:88

for b₁ being Field
for b₂, b₃, b₄ being Element of b₁ holds
( ( b₂ <> 0. b₁ & (b₂ * b₄) - b₃ = 0. b₁ implies b₄ = b₃ * (b₂ " ) ) & ( b₂ <> 0. b₁ & b₃ - (b₄ * b₂) = 0. b₁ implies b₄ = b₃ * (b₂ " ) ) )

proof end;

theorem Th89: :: VECTSP_1:89

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds b₂ + b₃ = - ((- b₃) + (- b₂))

proof end;

theorem Th90: :: VECTSP_1:90

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds (b₃ + b₂) - (b₄ + b₂) = b₃ - b₄

proof end;

theorem Th91: :: VECTSP_1:91

canceled;

theorem Th92: :: VECTSP_1:92

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - ((- b₂) + b₃) = (- b₃) + b₂

proof end;

theorem Th93: :: VECTSP_1:93

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ - b₃) - b₄ = (b₂ - b₄) - b₃

proof end;

theorem Th94: :: VECTSP_1:94

for b₁ being AbGroup holds HGrStr(# the carrier of b₁,the add of b₁ #) is commutative Group

proof end;