let M be MidSp; :: thesis: ( ( for a being set holds
( a is Element of (vectgroup M) iff a is Vector of M ) ) & 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
set G = vectgroup M;
thus for a being set holds
( a is Element of (vectgroup M) iff a is Vector of M ) :: thesis: ( 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
proof
let a be set ; :: thesis: ( a is Element of (vectgroup M) iff a is Vector of M )
( a is Element of (vectgroup M) iff a is Element of setvect M ) by MIDSP_1:53;
hence ( a is Element of (vectgroup M) iff a is Vector of M ) by MIDSP_1:48; :: thesis: verum
end;
thus 0. (vectgroup M) = zerovect M by MIDSP_1:55
.= ID M by MIDSP_1:def 16 ; :: thesis: for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y
thus for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y :: thesis: verum
proof
let a, b be Element of (vectgroup M); :: thesis: for x, y being Vector of M st a = x & b = y holds
a + b = x + y
let x, y be Vector of M; :: thesis: ( a = x & b = y implies a + b = x + y )
assume A1: ( a = x & b = y ) ; :: thesis: a + b = x + y
reconsider xx = x, yy = y as Element of setvect M by MIDSP_1:48;
thus a + b = the addF of (vectgroup M) . (a,b) by RLVECT_1:2
.= (addvect M) . (xx,yy) by A1, MIDSP_1:54
.= xx + yy by MIDSP_1:def 14
.= x + y by MIDSP_1:def 13 ; :: thesis: verum
end;