set S = LC_Z_Module V;

reconsider K = v as Linear_Combination of V by Def29;

thus (1. R) * v = (1. R) * K by A4

.= v ; :: thesis: verum

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

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 )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;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

proof

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 )
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;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

proof

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 )
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;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

proof

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 )
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;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

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

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

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 )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;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

proof

thus
LC_Z_Module V is scalar-distributive
:: thesis: ( LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )
let a be Element of R; :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of (LC_Z_Module V) holds a * (b_{1} + b_{2}) = (a * b_{1}) + (a * b_{2})

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

proof

thus
LC_Z_Module V is scalar-associative
:: thesis: LC_Z_Module V is scalar-unital
let a, b be Element of R; :: according to VECTSP_1:def 14 :: thesis: for b_{1} being Element of the carrier of (LC_Z_Module V) holds (a + b) * b_{1} = (a * b_{1}) + (b * b_{1})

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

proof

let v be Vector of (LC_Z_Module V); :: according to VECTSP_1:def 16 :: thesis: (1. R) * v = v
let a, b be Element of R; :: according to VECTSP_1:def 15 :: thesis: for b_{1} being Element of the carrier of (LC_Z_Module V) holds (a * b) * b_{1} = a * (b * b_{1})

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

reconsider K = v as Linear_Combination of V by Def29;

thus (1. R) * v = (1. R) * K by A4

.= v ; :: thesis: verum