let E be RealLinearSpace; :: thesis: for v being Element of E
for A, B being non empty binary-image of E holds
( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )
let v be Element of E; :: thesis: for A, B being non empty binary-image of E holds
( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )
let A, B be non empty binary-image of E; :: thesis: ( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )
for x being object holds
( x in (v + A) (-) B iff x in A (-) (v + B) )
proof
let x be object ; :: thesis: ( x in (v + A) (-) B iff x in A (-) (v + B) )
hereby :: thesis: ( x in A (-) (v + B) implies x in (v + A) (-) B )
assume x in (v + A) (-) B ; :: thesis: x in A (-) (v + B)
then consider w being Element of E such that
A1: ( x = w & ( for b being Element of E st b in B holds
w - b in v + A ) ) ;
now :: thesis: for vb being Element of E st vb in v + B holds
w - vb in A
let vb be Element of E; :: thesis: ( vb in v + B implies w - vb in A )
assume vb in v + B ; :: thesis: w - vb in A
then consider b being Element of E such that
A2: ( vb = v + b & b in B ) ;
w - b in v + A by A2, A1;
then consider a being Element of E such that
A3: ( w - b = v + a & a in A ) ;
w - vb = (w - b) - v by A2, RLVECT_1:27
.= a by A3, RLVECT_4:1 ;
hence w - vb in A by A3; :: thesis: verum
end;
hence x in A (-) (v + B) by A1; :: thesis: verum
end;
assume x in A (-) (v + B) ; :: thesis: x in (v + A) (-) B
then consider w being Element of E such that
A4: ( x = w & ( for vb being Element of E st vb in v + B holds
w - vb in A ) ) ;
now :: thesis: for b being Element of E st b in B holds
w - b in v + A
let b be Element of E; :: thesis: ( b in B implies w - b in v + A )
assume b in B ; :: thesis: w - b in v + A
then v + b in v + B ;
then w - (v + b) in A by A4;
then A5: v + (w - (v + b)) in v + A ;
v + (w - (v + b)) = (v + w) - (v + b) by RLVECT_1:28
.= w + (v - (v + b)) by RLVECT_1:28
.= w + ((v - v) - b) by RLVECT_1:27
.= w + ((0. E) - b) by RLVECT_1:15 ;
hence w - b in v + A by A5; :: thesis: verum
end;
hence x in (v + A) (-) B by A4; :: thesis: verum
end;
hence (v + A) (-) B = A (-) (v + B) by TARSKI:2; :: thesis: (v + A) (-) B = v + (A (-) B)
for x being object holds
( x in (v + A) (-) B iff x in v + (A (-) B) )
proof
let x be object ; :: thesis: ( x in (v + A) (-) B iff x in v + (A (-) B) )
hereby :: thesis: ( x in v + (A (-) B) implies x in (v + A) (-) B )
assume x in (v + A) (-) B ; :: thesis: x in v + (A (-) B)
then consider w being Element of E such that
A6: ( x = w & ( for b being Element of E st b in B holds
w - b in v + A ) ) ;
now :: thesis: for b being Element of E st b in B holds
(w - v) - b in A
let b be Element of E; :: thesis: ( b in B implies (w - v) - b in A )
assume b in B ; :: thesis: (w - v) - b in A
then A7: w - b in v + A by A6;
consider a being Element of E such that
A8: ( w - b = v + a & a in A ) by A7;
(w - v) - b = w - (v + b) by RLVECT_1:27
.= (v + a) - v by A8, RLVECT_1:27
.= a by RLVECT_4:1 ;
hence (w - v) - b in A by A8; :: thesis: verum
end;
then A9: w - v in A (-) B ;
v + (w - v) = w by RLVECT_4:1;
hence x in v + (A (-) B) by A6, A9; :: thesis: verum
end;
assume x in v + (A (-) B) ; :: thesis: x in (v + A) (-) B
then consider ab being Element of E such that
A10: ( x = v + ab & ab in A (-) B ) ;
reconsider w = x as Element of E by A10;
consider d being Element of E such that
A11: ( ab = d & ( for b being Element of E st b in B holds
d - b in A ) ) by A10;
now :: thesis: for b being Element of E st b in B holds
(v + ab) - b in v + A
let b be Element of E; :: thesis: ( b in B implies (v + ab) - b in v + A )
assume b in B ; :: thesis: (v + ab) - b in v + A
then A12: ab - b in A by A11;
(v + ab) - b = v + (ab - b) by RLVECT_1:28;
hence (v + ab) - b in v + A by A12; :: thesis: verum
end;
hence x in (v + A) (-) B by A10; :: thesis: verum
end;
hence (v + A) (-) B = v + (A (-) B) by TARSKI:2; :: thesis: verum