let E be RealLinearSpace; :: thesis: for A, B being non empty binary-image of E holds
( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
let A, B be non empty binary-image of E; :: thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
per cases ( A = the carrier of E or A <> the carrier of E ) ;
suppose A1: A = the carrier of E ; :: thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
reconsider X = {} as Subset of E by XBOOLE_1:2;
thus ( the carrier of E \ A) (+) B = X (+) B by A1, XBOOLE_1:37
.= {} by Th1
.= the carrier of E \ the carrier of E by XBOOLE_1:37
.= the carrier of E \ (A (-) B) by A1, Th4 ; :: thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)
thus ( the carrier of E \ A) (-) B = X (-) B by A1, XBOOLE_1:37
.= {} by Th2
.= the carrier of E \ the carrier of E by XBOOLE_1:37
.= the carrier of E \ (A (+) B) by A1, Th3 ; :: thesis: verum
end;
suppose A2: A <> the carrier of E ; :: thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
A3: not the carrier of E \ A is empty by XBOOLE_1:37, A2;
A4: for x being object holds
( x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } iff ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } ) )
proof
let x be object ; :: thesis: ( x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } iff ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } ) )
hereby :: thesis: ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } implies x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } )
assume x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } ; :: thesis: ( x in the carrier of E & not x in { w where w is Element of E : w + ((- 1) * B) c= A } )
then consider v being Element of E such that
A5: ( x = v & (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} ) ;
thus x in the carrier of E by A5; :: thesis: not x in { w where w is Element of E : w + ((- 1) * B) c= A }
thus not x in { w where w is Element of E : w + ((- 1) * B) c= A } :: thesis: verum
proof
assume x in { w where w is Element of E : w + ((- 1) * B) c= A } ; :: thesis: contradiction
then consider w being Element of E such that
A6: ( w = x & w + ((- 1) * B) c= A ) ;
v + ((- 1) * B) misses the carrier of E \ A by A5, A6, XBOOLE_1:85;
hence contradiction by A5; :: thesis: verum
end;
end;
assume A7: ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } ) ; :: thesis: x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} }
then reconsider w = x as Element of E ;
now :: thesis: not (w + ((- 1) * B)) /\ ( the carrier of E \ A) = {}
assume (w + ((- 1) * B)) /\ ( the carrier of E \ A) = {} ; :: thesis: contradiction
then {} = ((w + ((- 1) * B)) /\ the carrier of E) \ A by XBOOLE_1:49
.= (w + ((- 1) * B)) \ A by XBOOLE_1:28 ;
then w + ((- 1) * B) c= A by XBOOLE_1:37;
hence contradiction by A7; :: thesis: verum
end;
hence x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } ; :: thesis: verum
end;
A8: for x being object holds
( x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } iff ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ) )
proof
let x be object ; :: thesis: ( x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } iff ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ) )
hereby :: thesis: ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } implies x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } )
assume x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } ; :: thesis: ( x in the carrier of E & not x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } )
then consider v being Element of E such that
A9: ( x = v & v + ((- 1) * B) c= the carrier of E \ A ) ;
thus x in the carrier of E by A9; :: thesis: not x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} }
thus not x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } :: thesis: verum
proof
assume x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } ; :: thesis: contradiction
then consider w being Element of E such that
A10: ( w = x & (w + ((- 1) * B)) /\ A <> {} ) ;
w + ((- 1) * B) misses the carrier of E \ ( the carrier of E \ A) by A9, A10, XBOOLE_1:85;
then w + ((- 1) * B) misses the carrier of E /\ A by XBOOLE_1:48;
then w + ((- 1) * B) misses A by XBOOLE_1:28;
hence contradiction by A10; :: thesis: verum
end;
end;
assume A11: ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ) ; :: thesis: x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A }
then reconsider w = x as Element of E ;
reconsider w = x as Element of E by A11;
(w + ((- 1) * B)) \ ( the carrier of E \ A) = ((w + ((- 1) * B)) \ the carrier of E) \/ ((w + ((- 1) * B)) /\ A) by XBOOLE_1:52
.= {} \/ ((w + ((- 1) * B)) /\ A) by XBOOLE_1:37
.= {} by A11 ;
then w + ((- 1) * B) c= the carrier of E \ A by XBOOLE_1:37;
hence x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } ; :: thesis: verum
end;
thus ( the carrier of E \ A) (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } by Th7, A3
.= the carrier of E \ { v where v is Element of E : v + ((- 1) * B) c= A } by A4, XBOOLE_0:def 5
.= the carrier of E \ (A (-) B) by Th8 ; :: thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)
thus ( the carrier of E \ A) (-) B = { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } by Th8, A3
.= the carrier of E \ { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } by A8, XBOOLE_0:def 5
.= the carrier of E \ (A (+) B) by Th7 ; :: thesis: verum
end;
end;