set R = F;
A1:
[#] (ExField (x,o)) = carr (x,o)
by Def8;
now for a, b being Element of (ExField (x,o)) holds a + b = b + alet a,
b be
Element of
(ExField (x,o));
b1 + b2 = b2 + b1per cases
( b = o or b <> o )
;
suppose A2:
b = o
;
b1 + b2 = b2 + b1then
b in {o}
by TARSKI:def 1;
then reconsider b1 =
b as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( a = o or a <> o )
;
suppose A4:
a <> o
;
b1 + b2 = b2 + b1then
not
a in {o}
by TARSKI:def 1;
then A5:
a in ([#] F) \ {x}
by A1, XBOOLE_0:def 3;
reconsider a1 =
a as
Element of
carr (
x,
o)
by Def8;
reconsider aR =
a as
Element of
F by A5;
A6: the
addF of
F . (
a1,
x) =
aR + x
.=
x + aR
.=
the
addF of
F . (
x,
a1)
;
per cases
( the addF of F . (a,x) <> x or the addF of F . (a,x) = x )
;
suppose A7:
the
addF of
F . (
a,
x)
<> x
;
b1 + b2 = b2 + b1thus a + b =
(addR (x,o)) . (
a1,
b1)
by Def8
.=
addR (
a1,
b1)
by Def5
.=
the
addF of
F . (
a,
x)
by A7, A4, A2, Def4
.=
addR (
b1,
a1)
by A2, A4, A6, A7, Def4
.=
(addR (x,o)) . (
b1,
a1)
by Def5
.=
b + a
by Def8
;
verum end; suppose A8:
the
addF of
F . (
a,
x)
= x
;
b1 + b2 = b2 + b1thus a + b =
(addR (x,o)) . (
a1,
b1)
by Def8
.=
addR (
a1,
b1)
by Def5
.=
o
by A8, A4, A2, Def4
.=
addR (
b1,
a1)
by A6, A8, A4, A2, Def4
.=
(addR (x,o)) . (
b1,
a1)
by Def5
.=
b + a
by Def8
;
verum end; end; end; suppose A9:
b <> o
;
b1 + b2 = b2 + b1then
not
b in {o}
by TARSKI:def 1;
then A10:
b in ([#] F) \ {x}
by A1, XBOOLE_0:def 3;
reconsider b1 =
b as
Element of
carr (
x,
o)
by Def8;
per cases
( a = o or a <> o )
;
suppose A11:
a = o
;
b1 + b2 = b2 + b1then
a in {o}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
reconsider bR =
b as
Element of
F by A10;
A12: the
addF of
F . (
x,
b1) =
x + bR
.=
bR + x
.=
the
addF of
F . (
b1,
x)
;
per cases
( the addF of F . (x,b) <> x or the addF of F . (x,b) = x )
;
suppose A13:
the
addF of
F . (
x,
b)
<> x
;
b1 + b2 = b2 + b1thus a + b =
(addR (x,o)) . (
a1,
b1)
by Def8
.=
addR (
a1,
b1)
by Def5
.=
the
addF of
F . (
x,
b)
by A13, A11, A9, Def4
.=
addR (
b1,
a1)
by A9, A11, A12, A13, Def4
.=
(addR (x,o)) . (
b1,
a1)
by Def5
.=
b + a
by Def8
;
verum end; suppose A14:
the
addF of
F . (
x,
b)
= x
;
b1 + b2 = b2 + b1thus a + b =
(addR (x,o)) . (
a1,
b1)
by Def8
.=
addR (
a1,
b1)
by Def5
.=
o
by A9, A11, A14, Def4
.=
addR (
b1,
a1)
by A9, A11, A12, A14, Def4
.=
(addR (x,o)) . (
b1,
a1)
by Def5
.=
b + a
by Def8
;
verum end; end; suppose A15:
a <> o
;
b1 + b2 = b2 + b1then
not
a in {o}
by TARSKI:def 1;
then A16:
a in ([#] F) \ {x}
by A1, XBOOLE_0:def 3;
reconsider a1 =
a as
Element of
carr (
x,
o)
by Def8;
reconsider aR =
a,
bR =
b as
Element of
[#] F by A10, A16;
A17: the
addF of
F . (
a,
b) =
aR + bR
.=
bR + aR
.=
the
addF of
F . (
b,
a)
;
per cases
( the addF of F . (a,b) <> x or the addF of F . (a,b) = x )
;
suppose A18:
the
addF of
F . (
a,
b)
<> x
;
b1 + b2 = b2 + b1thus a + b =
(addR (x,o)) . (
a1,
b1)
by Def8
.=
addR (
a1,
b1)
by Def5
.=
the
addF of
F . (
a,
b)
by A9, A15, A18, Def4
.=
addR (
b1,
a1)
by A9, A15, A17, A18, Def4
.=
(addR (x,o)) . (
b1,
a1)
by Def5
.=
b + a
by Def8
;
verum end; suppose A19:
the
addF of
F . (
a,
b)
= x
;
b1 + b2 = b2 + b1thus a + b =
(addR (x,o)) . (
a1,
b1)
by Def8
.=
addR (
a1,
b1)
by Def5
.=
o
by A9, A15, A19, Def4
.=
addR (
b1,
a1)
by A9, A15, A17, A19, Def4
.=
(addR (x,o)) . (
b1,
a1)
by Def5
.=
b + a
by Def8
;
verum end; end; end; end;
hence
ExField (x,o) is Abelian
by RLVECT_1:def 2; verum