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
multF of
F . (
a1,
x) =
aR * x
.=
x * aR
by GROUP_1:def 12
.=
the
multF of
F . (
x,
a1)
;
per cases
( the multF of F . (a,x) <> x or the multF of F . (a,x) = x )
;
suppose A7:
the
multF of
F . (
a,
x)
<> x
;
b1 * b2 = b2 * b1thus a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
the
multF of
F . (
a,
x)
by A7, A4, A2, Def6
.=
multR (
b1,
a1)
by A6, A7, A4, A2, Def6
.=
(multR (x,o)) . (
b1,
a1)
by Def7
.=
b * a
by Def8
;
verum end; suppose A8:
the
multF of
F . (
a,
x)
= x
;
b1 * b2 = b2 * b1thus a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
o
by A8, A4, A2, Def6
.=
multR (
b1,
a1)
by A6, A8, A4, A2, Def6
.=
(multR (x,o)) . (
b1,
a1)
by Def7
.=
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
multF of
F . (
x,
b1) =
x * bR
.=
bR * x
by GROUP_1:def 12
.=
the
multF of
F . (
b1,
x)
;
per cases
( the multF of F . (x,b) <> x or the multF of F . (x,b) = x )
;
suppose A13:
the
multF of
F . (
x,
b)
<> x
;
b1 * b2 = b2 * b1thus a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
the
multF of
F . (
x,
b)
by A13, A11, A9, Def6
.=
multR (
b1,
a1)
by A12, A13, A11, A9, Def6
.=
(multR (x,o)) . (
b1,
a1)
by Def7
.=
b * a
by Def8
;
verum end; suppose A14:
the
multF of
F . (
x,
b)
= x
;
b1 * b2 = b2 * b1thus a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
o
by A14, A11, A9, Def6
.=
multR (
b1,
a1)
by A12, A14, A11, A9, Def6
.=
(multR (x,o)) . (
b1,
a1)
by Def7
.=
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
multF of
F . (
a,
b) =
aR * bR
.=
bR * aR
by GROUP_1:def 12
.=
the
multF of
F . (
b,
a)
;
per cases
( the multF of F . (a,b) <> x or the multF of F . (a,b) = x )
;
suppose A18:
the
multF of
F . (
a,
b)
<> x
;
b1 * b2 = b2 * b1thus a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
the
multF of
F . (
a,
b)
by A18, A15, A9, Def6
.=
multR (
b1,
a1)
by A17, A18, A15, A9, Def6
.=
(multR (x,o)) . (
b1,
a1)
by Def7
.=
b * a
by Def8
;
verum end; suppose A19:
the
multF of
F . (
a,
b)
= x
;
b1 * b2 = b2 * b1thus a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
o
by A19, A15, A9, Def6
.=
multR (
b1,
a1)
by A17, A19, A15, A9, Def6
.=
(multR (x,o)) . (
b1,
a1)
by Def7
.=
b * a
by Def8
;
verum end; end; end; end;
hence
ExField (x,o) is commutative
; verum