let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; 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; for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let v be Element of V; ( M = N + {v} iff M - {v} = N )
A1:
( M - {v} = N implies M = N + {v} )
proof
assume A2:
M - {v} = N
;
M = N + {v}
for
x being
object st
x in N + {v} holds
x in M
proof
let x be
object ;
( x in N + {v} implies x in M )
assume A3:
x in N + {v}
;
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 A3, RUSUB_4:def 9;
then consider u1,
v1 being
Element of
V such that A4:
x = u1 + v1
and A5:
u1 in N
and A6:
v1 in {v}
;
A7:
x - v1 =
u1 + (v1 - v1)
by A4, RLVECT_1:def 3
.=
u1 + (0. V)
by RLVECT_1:15
.=
u1
;
v1 = v
by A6, TARSKI:def 1;
then consider u2,
v2 being
Element of
V such that A8:
x - v = u2 - v2
and A9:
u2 in M
and A10:
v2 in {v}
by A2, A5, A7;
v2 = v
by A10, TARSKI:def 1;
then (x - v) + v =
u2 - (v - v)
by A8, RLVECT_1:29
.=
u2 - (0. V)
by RLVECT_1:15
.=
u2
;
then u2 =
x - (v - v)
by RLVECT_1:29
.=
x - (0. V)
by RLVECT_1:15
;
hence
x in M
by A9;
verum
end;
then A11:
N + {v} c= M
;
for
x being
object st
x in M holds
x in N + {v}
then
M c= N + {v}
;
hence
M = N + {v}
by A11;
verum
end;
( M = N + {v} implies M - {v} = N )
proof
assume A16:
M = N + {v}
;
M - {v} = N
for
x being
object st
x in M - {v} holds
x in N
proof
let x be
object ;
( x in M - {v} implies x in N )
assume A17:
x in M - {v}
;
x in N
then reconsider x =
x as
Element of
V ;
consider u1,
v1 being
Element of
V such that A18:
x = u1 - v1
and A19:
u1 in M
and A20:
v1 in {v}
by A17;
A21:
x + v1 =
u1 - (v1 - v1)
by A18, RLVECT_1:29
.=
u1 - (0. V)
by RLVECT_1:15
.=
u1
;
v1 = v
by A20, TARSKI:def 1;
then
x + v in { (u2 + v2) where u2, v2 is Element of V : ( u2 in N & v2 in {v} ) }
by A16, A19, A21, RUSUB_4:def 9;
then consider u2,
v2 being
Element of
V such that A22:
(
x + v = u2 + v2 &
u2 in N )
and A23:
v2 in {v}
;
v2 = v
by A23, TARSKI:def 1;
hence
x in N
by A22, RLVECT_1:8;
verum
end;
then A24:
M - {v} c= N
;
for
x being
object st
x in N holds
x in M - {v}
then
N c= M - {v}
;
hence
M - {v} = N
by A24;
verum
end;
hence
( M = N + {v} iff M - {v} = N )
by A1; verum