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