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 )

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

thus
vectgroup M is right_zeroed
:: thesis: ( vectgroup M is right_complementable & vectgroup M is Abelian )
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;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

proof

thus
vectgroup M is right_complementable
:: thesis: vectgroup M is Abelian
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

end;reconsider xx = x as Element of setvect M ;

thus x + (0. (vectgroup M)) = x :: thesis: verum

proof

thus
vectgroup M is Abelian
:: thesis: verum
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;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