let M be MidSp; :: thesis: ( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
set GS = vectgroup M;
thus vectgroup M is add-associative :: thesis: ( vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
proof
let x, y, z be Element of (vectgroup M); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider xx = x, yy = y, zz = z as Element of setvect M ;
thus (x + y) + z = (addvect M) . ((xx + yy),zz) by Def14
.= (xx + yy) + zz by Def14
.= xx + (yy + zz) by Th50
.= (addvect M) . (xx,(yy + zz)) by Def14
.= x + (y + z) by Def14 ; :: thesis: verum
end;
thus vectgroup M is right_zeroed :: thesis: ( vectgroup M is right_complementable & vectgroup M is Abelian )
proof
let x be Element of (vectgroup M); :: according to RLVECT_1:def 4 :: thesis: x + (0. (vectgroup M)) = x
reconsider xx = x as Element of setvect M ;
thus x + (0. (vectgroup M)) = x :: thesis: verum
proof
reconsider xxx = xx as Vector of M by Th48;
xx + (zerovect M) = xxx + (ID M) by Def13
.= x by Th44 ;
hence x + (0. (vectgroup M)) = x by Def14; :: thesis: verum
end;
end;
thus vectgroup M is right_complementable :: thesis: vectgroup M is Abelian
proof
let x be Element of (vectgroup M); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider xx = x as Element of setvect M ;
reconsider w = (complvect M) . xx as Element of (vectgroup M) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: x + w = 0. (vectgroup M)
thus x + w = xx + ((complvect M) . xx) by Def14
.= 0. (vectgroup M) by Def15 ; :: thesis: verum
end;
thus vectgroup M is Abelian :: thesis: verum
proof
let x, y be Element of (vectgroup M); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider xx = x, yy = y as Element of setvect M ;
thus x + y = xx + yy by Def14
.= yy + xx by Th49
.= y + x by Def14 ; :: thesis: verum
end;