let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for M, N being Subset of V
for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let M, N be Subset of V; :: thesis: for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let v be Element of V; :: thesis: ( M = N + {v} iff M - {v} = N )
A1:
( M = N + {v} implies M - {v} = N )
proof
assume A2:
M = N + {v}
;
:: thesis: M - {v} = N
for
x being
set st
x in M - {v} holds
x in N
proof
let x be
set ;
:: thesis: ( x in M - {v} implies x in N )
assume A3:
x in M - {v}
;
:: thesis: x in N
then reconsider x =
x as
Element of
V ;
consider u1,
v1 being
Element of
V such that A4:
(
x = u1 - v1 &
u1 in M &
v1 in {v} )
by A3;
A5:
v1 = v
by A4, TARSKI:def 1;
x + v1 =
u1 - (v1 - v1)
by A4, RLVECT_1:43
.=
u1 - (0. V)
by RLVECT_1:28
.=
u1
by RLVECT_1:26
;
then
x + v in { (u2 + v2) where u2, v2 is Element of V : ( u2 in N & v2 in {v} ) }
by A2, A4, A5, RUSUB_4:def 10;
then consider u2,
v2 being
Element of
V such that A6:
(
x + v = u2 + v2 &
u2 in N &
v2 in {v} )
;
v2 = v
by A6, TARSKI:def 1;
hence
x in N
by A6, RLVECT_1:21;
:: thesis: verum
end;
then A7:
M - {v} c= N
by TARSKI:def 3;
for
x being
set st
x in N holds
x in M - {v}
then
N c= M - {v}
by TARSKI:def 3;
hence
M - {v} = N
by A7, XBOOLE_0:def 10;
:: thesis: verum
end;
( M - {v} = N implies M = N + {v} )
proof
assume A11:
M - {v} = N
;
:: thesis: M = N + {v}
for
x being
set st
x in N + {v} holds
x in M
proof
let x be
set ;
:: thesis: ( x in N + {v} implies x in M )
assume A12:
x in N + {v}
;
:: thesis: x in M
then reconsider x =
x as
Element of
V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in N & v1 in {v} ) }
by A12, RUSUB_4:def 10;
then consider u1,
v1 being
Element of
V such that A13:
(
x = u1 + v1 &
u1 in N &
v1 in {v} )
;
A14:
v1 = v
by A13, TARSKI:def 1;
x - v1 =
u1 + (v1 - v1)
by A13, RLVECT_1:def 6
.=
u1 + (0. V)
by RLVECT_1:28
.=
u1
by RLVECT_1:10
;
then consider u2,
v2 being
Element of
V such that A15:
(
x - v = u2 - v2 &
u2 in M &
v2 in {v} )
by A11, A13, A14;
v2 = v
by A15, TARSKI:def 1;
then (x - v) + v =
u2 - (v - v)
by A15, RLVECT_1:43
.=
u2 - (0. V)
by RLVECT_1:28
.=
u2
by RLVECT_1:26
;
then u2 =
x - (v - v)
by RLVECT_1:43
.=
x - (0. V)
by RLVECT_1:28
;
hence
x in M
by A15, RLVECT_1:26;
:: thesis: verum
end;
then A16:
N + {v} c= M
by TARSKI:def 3;
for
x being
set st
x in M holds
x in N + {v}
then
M c= N + {v}
by TARSKI:def 3;
hence
M = N + {v}
by A16, XBOOLE_0:def 10;
:: thesis: verum
end;
hence
( M = N + {v} iff M - {v} = N )
by A1; :: thesis: verum