:: VECTSP_1 semantic presentation

defpred S₁[ Element of REAL , set ] means $2 = - $1;

definition

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

end;

:: deftheorem VECTSP_1:def 1 :

:: deftheorem VECTSP_1:def 2 :

:: deftheorem VECTSP_1:def 3 :

:: deftheorem VECTSP_1:def 4 :

:: deftheorem VECTSP_1:def 5 :

:: deftheorem 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 :: VECTSP_1:1

canceled;

theorem :: VECTSP_1:2

canceled;

theorem :: VECTSP_1:3

canceled;

theorem :: VECTSP_1:4

canceled;

theorem :: VECTSP_1:5

canceled;

theorem :: VECTSP_1:6

for x, y, z being Element of G_Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Real ) = x & x + (- x) = 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 :: VECTSP_1:7

for GS being non empty LoopStr holds
( ( for x, y, z being Element of GS holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. GS) = x & ex x' being Element of GS st x + x' = 0. GS ) ) iff GS is AbGroup ) by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

definition

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

end;

registration

cluster non empty strict multLoopStr ;
existence

proof end;

end;

definition

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

end;

:: deftheorem VECTSP_1:def 7 :

:: deftheorem VECTSP_1:def 8 :

:: deftheorem defines 1_ VECTSP_1:def 9 :

definition

attr c₁ 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 c₁ 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 IT be non empty doubleLoopStr ;
canceled;
attr IT is right-distributive means :Def11: :: VECTSP_1:def 11
for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c);
attr IT is left-distributive means :Def12: :: VECTSP_1:def 12
for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a);

end;

:: deftheorem VECTSP_1:def 10 :

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

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

definition

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

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 VECTSP_1:def 14 :

:: deftheorem defines F_Real VECTSP_1:def 15 :

definition

let IT be non empty doubleLoopStr ;
canceled;
canceled;
attr IT is distributive means :Def18: :: VECTSP_1:def 18
for x, y, z being Element of IT holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) );

end;

:: deftheorem VECTSP_1:def 16 :

:: deftheorem VECTSP_1:def 17 :

:: deftheorem Def18 defines distributive VECTSP_1:def 18 :

definition

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

end;

:: deftheorem Def19 defines left_unital VECTSP_1:def 19 :

definition

let IT be non empty multLoopStr_0 ;
attr IT is Field-like means :Def20: :: VECTSP_1:def 20
for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st x * y = 1. IT;

end;

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

definition

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

end;

:: deftheorem Def21 defines degenerated VECTSP_1:def 21 :

registration

cluster F_Real -> non empty strict ;
coherence

proof end;

end;

set FR = F_Real ;

Lm1: now

let h, a be Element of F_Real ; :: thesis:
assume A1: a = 1 ; :: thesis:
reconsider g = h as Element of REAL ;
thus h * a = multreal . h,a
.= g * 1 by A1, BINOP_2:def 11
.= h ; :: thesis:
thus a * h = multreal . a,h
.= 1 * g by A1, BINOP_2:def 11
.= h ; :: thesis:

end;

registration

cluster F_Real -> non empty unital strict ;
coherence

proof end;

end;

Lm2: 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;

Lm3: for L being non empty doubleLoopStr st L is distributive holds
( L is right-distributive & L is left-distributive )

proof end;

registration

cluster non empty distributive -> non empty right-distributive left-distributive doubleLoopStr ;
coherence by Lm3;
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 :: VECTSP_1:8

canceled;

theorem :: VECTSP_1:9

canceled;

theorem :: VECTSP_1:10

canceled;

theorem :: VECTSP_1:11

canceled;

theorem :: VECTSP_1:12

canceled;

theorem :: VECTSP_1:13

canceled;

theorem :: VECTSP_1:14

canceled;

theorem :: VECTSP_1:15

canceled;

theorem :: VECTSP_1:16

canceled;

theorem :: VECTSP_1:17

canceled;

theorem :: VECTSP_1:18

canceled;

theorem :: VECTSP_1:19

canceled;

theorem :: VECTSP_1:20

1. F_Real = 1 by Lm2;

theorem :: VECTSP_1:21

for x, y, z being Element of F_Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F_Real ) = x & x + (- x) = 0. F_Real & x * y = y * x & (x * y) * z = x * (y * z) & (1. F_Real ) * x = x & ( x <> 0. F_Real implies ex y being Element of F_Real st x * y = 1. F_Real ) & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Def18, Def19, Def20, GROUP_1:def 4, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 10;

theorem :: VECTSP_1:22

for FS being non empty doubleLoopStr holds
( ( for x, y, z being Element of FS holds
( ( x <> 0. FS implies ex y being Element of FS st x * y = 1. FS ) & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ) iff FS is non empty distributive Field-like doubleLoopStr ) by Def18, Def20;

theorem :: VECTSP_1:23

canceled;

theorem :: VECTSP_1:24

canceled;

theorem :: VECTSP_1:25

canceled;

theorem :: VECTSP_1:26

canceled;

theorem :: VECTSP_1:27

canceled;

theorem :: VECTSP_1:28

canceled;

theorem :: VECTSP_1:29

canceled;

theorem :: VECTSP_1:30

canceled;

theorem :: VECTSP_1:31

canceled;

theorem :: VECTSP_1:32

canceled;

theorem Th33: :: VECTSP_1:33

for F being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for x, y, z being Element of F st x <> 0. F & x * y = x * z holds
y = z

proof end;

definition

let F be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let x be Element of F;
assume A1: x <> 0. F ;
func x " -> Element of F means :Def22: :: VECTSP_1:def 22
x * it = 1. F;
existence by A1, Def20;
uniqueness by A1, Th33;

end;

:: deftheorem Def22 defines " VECTSP_1:def 22 :

definition

let F be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let x, y be Element of F;
func x / y -> Element of F equals :: VECTSP_1:def 23
x * (y " );
coherence ;

end;

:: deftheorem defines / VECTSP_1:def 23 :

theorem :: VECTSP_1:34

canceled;

theorem :: VECTSP_1:35

canceled;

theorem Th36: :: VECTSP_1:36

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

proof end;

theorem :: VECTSP_1:37

canceled;

theorem :: VECTSP_1:38

canceled;

theorem Th39: :: VECTSP_1:39

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

proof end;

theorem Th40: :: VECTSP_1:40

for F being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for x, y being Element of F holds x * (- y) = - (x * y)

proof end;

theorem Th41: :: VECTSP_1:41

for F being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for x, y being Element of F holds (- x) * y = - (x * y)

proof end;

theorem Th42: :: VECTSP_1:42

for F being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for x, y being Element of F holds (- x) * (- y) = x * y

proof end;

theorem :: VECTSP_1:43

for F being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)

proof end;

theorem Th44: :: VECTSP_1:44

for F being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for x, y being Element of F holds
( x * y = 0. F iff ( x = 0. F or y = 0. F ) )

proof end;

theorem :: VECTSP_1:45

for K being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)

proof end;

definition

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

end;

registration

let F be 1-sorted ;
cluster non empty strict VectSpStr of F;
existence

proof end;

end;

registration

let F be 1-sorted ;
let A be non empty set ;
let a be BinOp of A;
let Z be Element of A;
let l be Function of [:the carrier of F,A:],A;
cluster VectSpStr(# A,a,Z,l #) -> non empty ;
coherence

proof end;

end;

definition

let F be 1-sorted ;
mode Scalar of F is Element of F;

end;

definition

let F be 1-sorted ;
let VS be VectSpStr of F;
mode Scalar of VS is Scalar of F;
mode Vector of VS is Element of VS;

end;

definition

let F be non empty 1-sorted ;
let V be non empty VectSpStr of F;
let x be Element of F;
let v be Element of V;
func x * v -> Element of V equals :: VECTSP_1:def 24
the lmult of V . x,v;
coherence ;

end;

:: deftheorem defines * VECTSP_1:def 24 :

definition

let F be non empty LoopStr ;
func comp F -> UnOp of the carrier of F means :: VECTSP_1:def 25
for x being Element of F holds it . x = - x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines comp VECTSP_1:def 25 :

Lm4: now

let F be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ; :: thesis:
let MLT be Function of [:the carrier of F,the carrier of F:],the carrier of F; :: thesis:
set GF = VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #);
for x, y, z being Element of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #)) = x & ex x' being Element of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) st x + x' = 0. VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) )

proof

let x, y, z be Element of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #); :: thesis:
reconsider x' = x, y' = y, z' = z as Element of F ;
thus x + y = the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,y by RLVECT_1:5
.= y' + x' by RLVECT_1:5
.= the add of F . y',x' by RLVECT_1:5
.= y + x by RLVECT_1:5 ; :: thesis:
thus (x + y) + z = the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . (x + y),z by RLVECT_1:5
.= the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . (the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,y),z by RLVECT_1:5
.= the add of F . (x' + y'),z' by RLVECT_1:5
.= (x' + y') + z' by RLVECT_1:5
.= x' + (y' + z') by RLVECT_1:def 6
.= the add of F . x',(y' + z') by RLVECT_1:5
.= the add of F . x',(the add of F . y',z') by RLVECT_1:5
.= the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,(y + z) by RLVECT_1:5
.= x + (y + z) by RLVECT_1:5 ; :: thesis:
thus x + (0. VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #)) = the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,(0. VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #)) by RLVECT_1:5
.= the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,the Zero of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #)
.= x' + (0. F) by RLVECT_1:5
.= x by RLVECT_1:10 ; :: thesis:
consider t being Element of F such that
A1: x' + t = 0. F by RLVECT_1:def 8;
reconsider t' = t as Element of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) ;
take t' ; :: thesis:
thus x + t' = the add of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,t' by RLVECT_1:5
.= x' + t by RLVECT_1:5
.= 0. VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) by A1 ; :: thesis:

end;

hence VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) is AbGroup by RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8; :: thesis:

end;

Lm5: now

let F be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ; :: thesis:
let MLT be Function of [:the carrier of F,the carrier of F:],the carrier of F; :: thesis:
assume A1: MLT = the mult of F ; :: thesis:
set LS = VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #);
let x, y be Element of F; :: thesis:
let v, w be Element of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #); :: thesis:
reconsider v' = v, w' = w as Element of F ;
thus x * (v + w) = the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,(v + w)
.= MLT . x,(the add of F . v',w') by RLVECT_1:5
.= MLT . x,(v' + w') by RLVECT_1:5
.= x * (v' + w') by A1
.= (x * v') + (x * w') by Def18
.= the add of F . (x * v'),(x * w') by RLVECT_1:5
.= the add of F . (MLT . x,v'),(x * w') by A1
.= the add of F . (the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,v),(the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,w) by A1
.= the add of F . (x * v),(x * w)
.= (x * v) + (x * w) by RLVECT_1:5 ; :: thesis:
thus (x + y) * v = the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . (x + y),v
.= (x + y) * v' by A1
.= (x * v') + (y * v') by Def18
.= the add of F . (x * v'),(y * v') by RLVECT_1:5
.= the add of F . (MLT . x,v'),(y * v') by A1
.= the add of F . (the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,v),(the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . y,v) by A1
.= the add of F . (x * v),(y * v)
.= (x * v) + (y * v) by RLVECT_1:5 ; :: thesis:
thus (x * y) * v = the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . (x * y),v
.= (x * y) * v' by A1
.= x * (y * v') by GROUP_1:def 4
.= MLT . x,(y * v') by A1
.= the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,(the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . y,v) by A1
.= the lmult of VectSpStr(# the carrier of F,the add of F,the Zero of F,MLT #) . x,(y * v)
.= x * (y * v) ; :: thesis:
thus (1. F) * v = MLT . (1. F),v'
.= (1. F) * v' by A1
.= v by Def19 ; :: thesis:

end;

definition

let F be non empty doubleLoopStr ;
let IT be non empty VectSpStr of F;
attr IT is VectSp-like means :Def26: :: VECTSP_1:def 26
for x, y being Element of F
for v, w being Element of IT holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v );

end;

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

registration

let F 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 F;
existence

proof end;

end;

definition

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

end;

theorem :: VECTSP_1:46

canceled;

theorem :: VECTSP_1:47

canceled;

theorem :: VECTSP_1:48

canceled;

theorem :: VECTSP_1:49

canceled;

theorem :: VECTSP_1:50

canceled;

theorem :: VECTSP_1:51

canceled;

theorem :: VECTSP_1:52

canceled;

theorem :: VECTSP_1:53

canceled;

theorem :: VECTSP_1:54

canceled;

theorem :: VECTSP_1:55

canceled;

theorem :: VECTSP_1:56

canceled;

theorem :: VECTSP_1:57

canceled;

theorem :: VECTSP_1:58

canceled;

theorem Th59: :: VECTSP_1:59

for F being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for x being Element of F
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F
for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )

proof end;

theorem :: VECTSP_1:60

for F being Field
for x being Element of F
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F
for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

proof end;

theorem :: VECTSP_1:61

canceled;

theorem :: VECTSP_1:62

canceled;

theorem :: VECTSP_1:63

for V being non empty add-associative right_zeroed right_complementable LoopStr
for v, w being Element of V holds
( v + w = 0. V iff - v = w )

proof end;

Lm6: for V being non empty add-associative right_zeroed right_complementable LoopStr
for v, w being Element of V holds - (w + (- v)) = v - w

proof end;

Lm7: for V being non empty add-associative right_zeroed right_complementable LoopStr
for v, w being Element of V holds - ((- v) - w) = w + v

proof end;

theorem :: VECTSP_1:64

for V being non empty add-associative right_zeroed right_complementable LoopStr
for u, v, w being Element of V holds
( - (v + w) = (- w) - v & - (w + (- v)) = v - w & - (v - w) = w + (- v) & - ((- v) - w) = w + v & u - (w + v) = (u - v) - w ) by Lm6, Lm7, RLVECT_1:41, RLVECT_1:44, RLVECT_1:47;

theorem :: VECTSP_1:65

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

theorem Th66: :: VECTSP_1:66

for F being non empty add-associative right_zeroed right_complementable LoopStr
for x, y being Element of F holds
( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )

proof end;

theorem :: VECTSP_1:67

for F being Field
for x being Element of F
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F
for v being Element of V st x <> 0. F holds
(x " ) * (x * v) = v

proof end;

theorem Th68: :: VECTSP_1:68

for F being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F
for x being Element of F
for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )

proof end;

registration

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

proof end;

end;

theorem Th69: :: VECTSP_1:69

for F being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F
for x being Element of F
for v being Element of V holds x * (- v) = - (x * v)

proof end;

theorem :: VECTSP_1:70

proof end;

theorem :: VECTSP_1:71

canceled;

theorem :: VECTSP_1:72

canceled;

theorem :: VECTSP_1:73

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

proof end;

theorem :: VECTSP_1:74

for F being Field
for x being Element of F st x <> 0. F holds
( x " <> 0. F & - (x " ) <> 0. F )

proof end;

theorem :: VECTSP_1:75

canceled;

theorem :: VECTSP_1:76

canceled;

theorem :: VECTSP_1:77

canceled;

theorem Th78: :: VECTSP_1:78

(1. F_Real ) + (1. F_Real ) <> 0. F_Real

proof end;

definition

let IT be non empty LoopStr ;
canceled;
attr IT is Fanoian means :Def28: :: VECTSP_1:def 28
for a being Element of IT st a + a = 0. IT holds
a = 0. IT;

end;

:: deftheorem VECTSP_1:def 27 :

:: deftheorem Def28 defines Fanoian VECTSP_1:def 28 :

registration

cluster non empty Fanoian LoopStr ;
existence

proof end;

end;

definition

let F be non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr ;
redefine attr F is Fanoian means :Def29: :: VECTSP_1:def 29
(1. F) + (1. F) <> 0. F;
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 :: VECTSP_1:79

canceled;

theorem :: VECTSP_1:80

canceled;

theorem Th81: :: VECTSP_1:81

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

theorem :: VECTSP_1:82

canceled;

theorem :: VECTSP_1:83

canceled;

theorem :: VECTSP_1:84

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

theorem :: VECTSP_1:85

canceled;

theorem Th86: :: VECTSP_1:86

for F being non empty add-associative right_zeroed right_complementable LoopStr
for a being Element of F st - a = 0. F holds
a = 0. F

proof end;

theorem :: VECTSP_1:87

for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b being Element of F st a - b = 0. F holds
b - a = 0. F

proof end;

theorem :: VECTSP_1:88

for F being Field
for a, b, c being Element of F holds
( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a " ) ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a " ) ) )

proof end;

theorem :: VECTSP_1:89

for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b being Element of F holds a + b = - ((- b) + (- a))

proof end;

theorem :: VECTSP_1:90

for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b, c being Element of F holds (b + a) - (c + a) = b - c

proof end;

theorem :: VECTSP_1:91

canceled;

theorem :: VECTSP_1:92

for G being non empty add-associative right_zeroed right_complementable LoopStr
for v, w being Element of G holds - ((- v) + w) = (- w) + v

proof end;

theorem :: VECTSP_1:93

for G being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for u, v, w being Element of G holds (u - v) - w = (u - w) - v

proof end;

theorem :: VECTSP_1:94

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

proof end;