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 well-unital
let x be non trivial Element of F; for o being object st not o in [#] F holds
ExField (x,o) is well-unital
let u be object ; ( not u in [#] F implies ExField (x,u) is well-unital )
assume
not u in [#] F
; ExField (x,u) is well-unital
then A1:
for a being Element of F holds a <> u
;
set C = carr (x,u);
set E = ExField (x,u);
A2:
[#] (ExField (x,u)) = carr (x,u)
by Def8;
now for a being Element of (ExField (x,u)) holds
( a * (1. (ExField (x,u))) = a & (1. (ExField (x,u))) * a = a )let a be
Element of
(ExField (x,u));
( b1 * (1. (ExField (x,u))) = b1 & (1. (ExField (x,u))) * b1 = b1 )A3:
1. (ExField (x,u)) = 1. F
by Def8;
1. F <> x
by Def2;
then
not
1. F in {x}
by TARSKI:def 1;
then
1. F in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider o =
1. F as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A4:
o <> u
by A1;
per cases
( a = u or a <> u )
;
suppose A5:
a = u
;
( b1 * (1. (ExField (x,u))) = b1 & (1. (ExField (x,u))) * b1 = b1 )then
a in {u}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A6: the
multF of
F . (
x,
(1. F)) =
x * (1. F)
.=
x
;
thus a * (1. (ExField (x,u))) =
(multR (x,u)) . (
a1,
o)
by A3, Def8
.=
multR (
a1,
o)
by Def7
.=
a
by A6, A4, A5, Def6
;
(1. (ExField (x,u))) * a = aA7: the
multF of
F . (
(1. F),
x) =
(1. F) * x
.=
x
;
thus (1. (ExField (x,u))) * a =
(multR (x,u)) . (
o,
a1)
by A3, Def8
.=
multR (
o,
a1)
by Def7
.=
a
by A7, A4, A5, Def6
;
verum end; suppose A8:
a <> u
;
( b1 * (1. (ExField (x,u))) = b1 & (1. (ExField (x,u))) * b1 = b1 )then
not
a in {u}
by TARSKI:def 1;
then A9:
a in ([#] F) \ {x}
by A2, XBOOLE_0:def 3;
reconsider a1 =
a as
Element of
carr (
x,
u)
by Def8;
reconsider aR =
a as
Element of
[#] F by A9;
A10: the
multF of
F . (
a,
o) =
aR * (1. F)
.=
aR
;
A11:
not
aR in {x}
by A9, XBOOLE_0:def 5;
then A12:
the
multF of
F . (
a,
o)
<> x
by A10, TARSKI:def 1;
thus a * (1. (ExField (x,u))) =
(multR (x,u)) . (
a1,
o)
by A3, Def8
.=
multR (
a1,
o)
by Def7
.=
aR * (1. F)
by A12, A4, A8, Def6
.=
a
;
(1. (ExField (x,u))) * a = a the
multF of
F . (
o,
a) =
(1. F) * aR
.=
aR
;
then A13:
the
multF of
F . (
o,
a)
<> x
by A11, TARSKI:def 1;
thus (1. (ExField (x,u))) * a =
(multR (x,u)) . (
o,
a1)
by A3, Def8
.=
multR (
o,
a1)
by Def7
.=
(1. F) * aR
by A13, A4, A8, Def6
.=
a
;
verum end; end;
hence
ExField (x,u) is well-unital
; verum