set S = LC_Z_Module V;

A1: now :: thesis: for v, u being Vector of (LC_Z_Module V)
for K, L being Linear_Combination of V st v = K & u = L holds
v + u = K + L

let v, u be Vector of (LC_Z_Module V); :: thesis: for K, L being Linear_Combination of V st v = K & u = L holds
v + u = K + L
let K, L be Linear_Combination of V; :: thesis: ( v = K & u = L implies v + u = K + L )
A2: ( @ (@ K) = K & @ (@ L) = L ) ;
assume ( v = K & u = L ) ; :: thesis: v + u = K + L
hence v + u = K + L by A2, Def32; :: thesis: verum

end;

thus LC_Z_Module V is Abelian :: thesis: ( LC_Z_Module V is add-associative & LC_Z_Module V is right_zeroed & LC_Z_Module V is right_complementable & LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof

let u, v be Element of (LC_Z_Module V); :: according to RLVECT_1:def 2 :: thesis: u + v = v + u
reconsider K = u, L = v as Linear_Combination of V by Def29;
thus u + v = K + L by A1
.= L + K
.= v + u by A1 ; :: thesis: verum

end;

thus LC_Z_Module V is add-associative :: thesis: ( LC_Z_Module V is right_zeroed & LC_Z_Module V is right_complementable & LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof

let u, v, w be Element of (LC_Z_Module V); :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
reconsider L = u, K = v, M = w as Linear_Combination of V by Def29;
A3: v + w = K + M by A1;
u + v = L + K by A1;
hence (u + v) + w = (L + K) + M by A1
.= L + (K + M) by Th28
.= u + (v + w) by A1, A3 ;
:: thesis: verum

end;

thus LC_Z_Module V is right_zeroed :: thesis: ( LC_Z_Module V is right_complementable & LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof

let v be Element of (LC_Z_Module V); :: according to RLVECT_1:def 4 :: thesis: v + (0. (LC_Z_Module V)) = v
reconsider K = v as Linear_Combination of V by Def29;
thus v + (0. (LC_Z_Module V)) = K + (ZeroLC V) by A1
.= v ; :: thesis: verum

end;

thus LC_Z_Module V is right_complementable :: thesis: ( LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof

let v be Element of (LC_Z_Module V); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider K = v as Linear_Combination of V by Def29;
- K in the carrier of (LC_Z_Module V) by Def29;
then - K in LC_Z_Module V ;
then - K = vector ((LC_Z_Module V),(- K)) by RLVECT_2:def 1;
then v + (vector ((LC_Z_Module V),(- K))) = K - K by A1
.= 0. (LC_Z_Module V) by Th42 ;
hence ex w being Vector of (LC_Z_Module V) st v + w = 0. (LC_Z_Module V) ; :: according to ALGSTR_0:def 11 :: thesis: verum

end;

A4: now :: thesis: for v being Vector of (LC_Z_Module V)
for L being Linear_Combination of V
for a being Element of R st v = L holds
a * v = a * L

let v be Vector of (LC_Z_Module V); :: thesis: for L being Linear_Combination of V
for a being Element of R st v = L holds
a * v = a * L
let L be Linear_Combination of V; :: thesis: for a being Element of R st v = L holds
a * v = a * L
let a be Element of R; :: thesis: ( v = L implies a * v = a * L )
A5: @ (@ L) = L ;
assume v = L ; :: thesis: a * v = a * L
hence a * v = a * L by A5, Def33; :: thesis: verum

end;

thus LC_Z_Module V is vector-distributive :: thesis: ( LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof

let a be Element of R; :: according to VECTSP_1:def 13 :: thesis: for b₁, b₂ being Element of the carrier of (LC_Z_Module V) holds a * (b₁ + b₂) = (a * b₁) + (a * b₂)
let v, w be Vector of (LC_Z_Module V); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider K = v, M = w as Linear_Combination of V by Def29;
A6: ( a * v = a * K & a * w = a * M ) by A4;
v + w = K + M by A1;
then a * (v + w) = a * (K + M) by A4
.= (a * K) + (a * M) by Th33
.= (a * v) + (a * w) by A1, A6 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

thus LC_Z_Module V is scalar-distributive :: thesis: ( LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )

proof

let a, b be Element of R; :: according to VECTSP_1:def 14 :: thesis: for b₁ being Element of the carrier of (LC_Z_Module V) holds (a + b) * b₁ = (a * b₁) + (b * b₁)
let v be Vector of (LC_Z_Module V); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider K = v as Linear_Combination of V by Def29;
A7: ( a * v = a * K & b * v = b * K ) by A4;
(a + b) * v = (a + b) * K by A4
.= (a * K) + (b * K) by Th32
.= (a * v) + (b * v) by A1, A7 ;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

thus LC_Z_Module V is scalar-associative :: thesis: LC_Z_Module V is scalar-unital

proof

let a, b be Element of R; :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of (LC_Z_Module V) holds (a * b) * b₁ = a * (b * b₁)
let v be Vector of (LC_Z_Module V); :: thesis: (a * b) * v = a * (b * v)
reconsider K = v as Linear_Combination of V by Def29;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th34
.= a * (b * v) by A4, A8 ;
hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

let v be Vector of (LC_Z_Module V); :: according to VECTSP_1:def 16 :: thesis: (1. R) * v = v
reconsider K = v as Linear_Combination of V by Def29;
thus (1. R) * v = (1. R) * K by A4
.= v ; :: thesis: verum