let F be non almost_trivial Field; for x being non trivial Element of F
for o being object st not o in [#] F holds
( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )
let x be non trivial Element of F; for o being object st not o in [#] F holds
( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )
let o be object ; ( not o in [#] F implies ( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable ) )
assume a1:
not o in [#] F
; ( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )
then A1:
for a being Element of F holds a <> o
;
set C = carr (x,o);
set ADDR = the addF of F;
consider xi being Element of F such that
A2:
x + xi = 0. F
by ALGSTR_0:def 11;
A3:
[#] (ExField (x,o)) = carr (x,o)
by Def8;
o in {o}
by TARSKI:def 1;
then reconsider u1 = o as Element of carr (x,o) by XBOOLE_0:def 3;
reconsider u = u1 as Element of (ExField (x,o)) by Def8;
now for a being Element of (ExField (x,o)) holds a + (0. (ExField (x,o))) = alet a be
Element of
(ExField (x,o));
b1 + (0. (ExField (x,o))) = b1A4:
0. (ExField (x,o)) = 0. F
by Def8;
0. F <> x
by Def2;
then
not
0. F in {x}
by TARSKI:def 1;
then
0. F in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider u =
0. F as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
A5:
o <> u
by a1;
per cases
( a = o or a <> o )
;
suppose A6:
a = o
;
b1 + (0. (ExField (x,o))) = b1then
a in {o}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
A7: the
addF of
F . (
x,
(0. F)) =
x + (0. F)
.=
x
;
thus a + (0. (ExField (x,o))) =
(addR (x,o)) . (
a1,
u)
by A4, Def8
.=
addR (
a1,
u)
by Def5
.=
a
by A5, A6, A7, Def4
;
verum end; suppose A8:
a <> o
;
b1 + (0. (ExField (x,o))) = b1then
not
a in {o}
by TARSKI:def 1;
then A9:
a in ([#] F) \ {x}
by A3, XBOOLE_0:def 3;
reconsider a1 =
a as
Element of
carr (
x,
o)
by Def8;
reconsider aR =
a as
Element of
[#] F by A9;
A10: the
addF of
F . (
a,
u) =
aR + (0. F)
.=
aR
;
not
aR in {x}
by A9, XBOOLE_0:def 5;
then A11:
the
addF of
F . (
a,
u)
<> x
by A10, TARSKI:def 1;
thus a + (0. (ExField (x,o))) =
(addR (x,o)) . (
a1,
u)
by A4, Def8
.=
addR (
a1,
u)
by Def5
.=
aR + (0. F)
by A8, A5, A11, Def4
.=
a
;
verum end; end;
hence
ExField (x,o) is right_zeroed
by RLVECT_1:def 4; ExField (x,o) is right_complementable
now for a being Element of (ExField (x,o)) holds a is right_complementable let a be
Element of
(ExField (x,o));
b1 is right_complementable per cases
( a = o or a <> o )
;
suppose A12:
a = o
;
b1 is right_complementable then
a in {o}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( xi = x or xi <> x )
;
suppose A13:
xi = x
;
b1 is right_complementable then A14:
the
addF of
F . (
x,
x)
<> x
by A2, Def2;
a + u =
(addR (x,o)) . (
a1,
u1)
by Def8
.=
addR (
a1,
u1)
by Def5
.=
the
addF of
F . (
x,
xi)
by A12, A13, A14, Def4
.=
0. (ExField (x,o))
by A2, Def8
;
hence
a is
right_complementable
by ALGSTR_0:def 11;
verum end; suppose
xi <> x
;
b1 is right_complementable then
not
xi in {x}
by TARSKI:def 1;
then
xi in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider x1i =
xi as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
reconsider b =
x1i as
Element of
(ExField (x,o)) by Def8;
A15:
the
addF of
F . (
x,
b)
<> x
by A2, Def2;
a + b =
(addR (x,o)) . (
a1,
x1i)
by Def8
.=
addR (
a1,
x1i)
by Def5
.=
the
addF of
F . (
x,
xi)
by A1, A12, A15, Def4
.=
0. (ExField (x,o))
by A2, Def8
;
hence
a is
right_complementable
by ALGSTR_0:def 11;
verum end; end; suppose A16:
a <> o
;
b1 is right_complementable then
not
a in {o}
by TARSKI:def 1;
then A17:
a in ([#] F) \ {x}
by A3, XBOOLE_0:def 3;
reconsider a1 =
a as
Element of
carr (
x,
o)
by Def8;
reconsider aR =
a as
Element of
[#] F by A17;
consider aRi being
Element of
F such that A18:
aR + aRi = 0. F
by ALGSTR_0:def 11;
per cases
( aRi = x or aRi <> x )
;
suppose A19:
aRi = x
;
b1 is right_complementable then A20:
the
addF of
F . (
a,
x)
<> x
by A18, Def2;
a + u =
(addR (x,o)) . (
a1,
u1)
by Def8
.=
addR (
a1,
u1)
by Def5
.=
the
addF of
F . (
aR,
aRi)
by A16, A19, A20, Def4
.=
0. (ExField (x,o))
by A18, Def8
;
hence
a is
right_complementable
by ALGSTR_0:def 11;
verum end; suppose
aRi <> x
;
b1 is right_complementable then
not
aRi in {x}
by TARSKI:def 1;
then
aRi in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider a1i =
aRi as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
reconsider b =
a1i as
Element of
(ExField (x,o)) by Def8;
A21:
the
addF of
F . (
a,
b)
<> x
by A18, Def2;
A22:
(
aR <> o &
aRi <> o )
by a1;
a + b =
(addR (x,o)) . (
a1,
aRi)
by Def8
.=
addR (
a1,
a1i)
by Def5
.=
the
addF of
F . (
aR,
aRi)
by A21, A22, Def4
.=
0. (ExField (x,o))
by A18, Def8
;
hence
a is
right_complementable
by ALGSTR_0:def 11;
verum end; end; end;
hence
ExField (x,o) is right_complementable
by ALGSTR_0:def 16; verum