let V be Z_Module; :: thesis: for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds
( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real; :: thesis: ( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
set L = GenLat (V,sc);
A1: for x, y being Vector of (GenLat (V,sc))
for x9, y9 being Vector of V st x = x9 & y = y9 holds
( x + y = x9 + y9 & ( for a being Element of INT.Ring holds a * x = a * x9 ) ) ;
thus for v, w being Vector of (GenLat (V,sc)) holds v + w = w + v :: according to RLVECT_1:def 2 :: thesis: ( GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
proof
let v, w be Vector of (GenLat (V,sc)); :: thesis: v + w = w + v
reconsider v9 = v, w9 = w as Vector of V ;
thus v + w = w9 + v9 by A1
.= w + v ; :: thesis: verum
end;
thus for u, v, w being Vector of (GenLat (V,sc)) holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def 3 :: thesis: ( GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
proof
let u, v, w be Vector of (GenLat (V,sc)); :: thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as Vector of V ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum
end;
thus for v being Vector of (GenLat (V,sc)) holds v + (0. (GenLat (V,sc))) = v :: according to RLVECT_1:def 4 :: thesis: ( GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
proof
let v be Vector of (GenLat (V,sc)); :: thesis: v + (0. (GenLat (V,sc))) = v
reconsider v9 = v as Vector of V ;
thus v + (0. (GenLat (V,sc))) = v9 + (0. V)
.= v ; :: thesis: verum
end;
thus GenLat (V,sc) is right_complementable :: thesis: ( GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
proof
let v be Vector of (GenLat (V,sc)); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v9 = v as Vector of V ;
consider w9 being Vector of V such that
A2: v9 + w9 = 0. V by ALGSTR_0:def 11;
reconsider w = w9 as Vector of (GenLat (V,sc)) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (GenLat (V,sc))
thus v + w = 0. (GenLat (V,sc)) by A2; :: thesis: verum
end;
thus for a, b being Element of INT.Ring
for v being Vector of (GenLat (V,sc)) holds (a + b) * v = (a * v) + (b * v) :: according to VECTSP_1:def 14 :: thesis: ( GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
proof
let a, b be Element of INT.Ring; :: thesis: for v being Vector of (GenLat (V,sc)) holds (a + b) * v = (a * v) + (b * v)
let v be Vector of (GenLat (V,sc)); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as Vector of V ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by VECTSP_1:def 15
.= (a * v) + (b * v) ; :: thesis: verum
end;
thus for a being Element of INT.Ring
for v, w being Vector of (GenLat (V,sc)) holds a * (v + w) = (a * v) + (a * w) :: according to VECTSP_1:def 13 :: thesis: ( GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
proof
let a be Element of INT.Ring; :: thesis: for v, w being Vector of (GenLat (V,sc)) holds a * (v + w) = (a * v) + (a * w)
let v, w be Vector of (GenLat (V,sc)); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as Vector of V ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by VECTSP_1:def 14
.= (a * v) + (a * w) ; :: thesis: verum
end;
thus for a, b being Element of INT.Ring
for v being Vector of (GenLat (V,sc)) holds (a * b) * v = a * (b * v) :: according to VECTSP_1:def 15 :: thesis: GenLat (V,sc) is scalar-unital
proof
let a, b be Element of INT.Ring; :: thesis: for v being Vector of (GenLat (V,sc)) holds (a * b) * v = a * (b * v)
let v be Vector of (GenLat (V,sc)); :: thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as Vector of V ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by VECTSP_1:def 16
.= a * (b * v) ; :: thesis: verum
end;
thus for v being Vector of (GenLat (V,sc)) holds (1. INT.Ring) * v = v :: according to VECTSP_1:def 16 :: thesis: verum
proof
let v be Vector of (GenLat (V,sc)); :: thesis: (1. INT.Ring) * v = v
reconsider v9 = v as Vector of V ;
thus (1. INT.Ring) * v = (1. INT.Ring) * v9
.= v by VECTSP_1:def 17 ; :: thesis: verum
end;