let F be non almost_trivial Field; for x being non trivial Element of F
for u being object st not u in [#] F holds
( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )
let x be non trivial Element of F; for u being object st not u in [#] F holds
( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )
let u be object ; ( not u in [#] F implies ( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving ) )
assume A1:
not u in [#] F
; ( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )
then A2:
for a being Element of F holds a <> u
;
set f = isoR (x,u);
u in {u}
by TARSKI:def 1;
then reconsider o = u as Element of carr (x,u) by XBOOLE_0:def 3;
now for a, b being Element of F holds ((isoR (x,u)) . a) + ((isoR (x,u)) . b) = (isoR (x,u)) . (a + b)let a,
b be
Element of
F;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)A3:
(
a <> u &
b <> u )
by A2;
per cases
( a = x or a <> x )
;
suppose A4:
a = x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)then A5:
(isoR (x,u)) . a = u
by Def9;
per cases
( b = x or b <> x )
;
suppose A6:
b = x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)then A7:
(isoR (x,u)) . b = u
by Def9;
per cases
( the addF of F . (x,x) <> x or the addF of F . (x,x) = x )
;
suppose A8:
the
addF of
F . (
x,
x)
<> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
u,
u)
by A5, A7, Def8
.=
addR (
o,
o)
by Def5
.=
a + b
by A4, A6, A8, Def4
.=
(isoR (x,u)) . (a + b)
by A4, A6, A8, Def9
;
verum end; suppose A9:
the
addF of
F . (
x,
x)
= x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
u,
u)
by A5, A7, Def8
.=
addR (
o,
o)
by Def5
.=
u
by A9, Def4
.=
(isoR (x,u)) . (a + b)
by A4, A6, A9, Def9
;
verum end; end; suppose A10:
b <> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)then
not
b in {x}
by TARSKI:def 1;
then
b in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider b1 =
b as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A11:
(isoR (x,u)) . b = b
by A10, Def9;
per cases
( the addF of F . (x,b) <> x or the addF of F . (x,b) = x )
;
suppose A12:
the
addF of
F . (
x,
b)
<> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
u,
b)
by A5, A11, Def8
.=
addR (
o,
b1)
by Def5
.=
a + b
by A2, A4, A12, Def4
.=
(isoR (x,u)) . (a + b)
by A4, A12, Def9
;
verum end; suppose A13:
the
addF of
F . (
x,
b)
= x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
u,
b)
by A5, A11, Def8
.=
addR (
o,
b1)
by Def5
.=
u
by A3, A13, Def4
.=
(isoR (x,u)) . (a + b)
by A4, A13, Def9
;
verum end; end; end; suppose A14:
a <> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)then
not
a in {x}
by TARSKI:def 1;
then
a in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider a1 =
a as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A15:
(isoR (x,u)) . a = a
by A14, Def9;
per cases
( b = x or b <> x )
;
suppose A16:
b = x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)then A17:
(isoR (x,u)) . b = u
by Def9;
per cases
( the addF of F . (a,x) <> x or the addF of F . (a,x) = x )
;
suppose A18:
the
addF of
F . (
a,
x)
<> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
a,
u)
by A15, A17, Def8
.=
addR (
a1,
o)
by Def5
.=
a + b
by A16, A2, A18, Def4
.=
(isoR (x,u)) . (a + b)
by A16, A18, Def9
;
verum end; suppose A19:
the
addF of
F . (
a,
x)
= x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
a,
u)
by A15, A17, Def8
.=
addR (
a1,
o)
by Def5
.=
u
by A3, A19, Def4
.=
(isoR (x,u)) . (a + b)
by A16, A19, Def9
;
verum end; end; suppose A20:
b <> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)then
not
b in {x}
by TARSKI:def 1;
then
b in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider b1 =
b as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A21:
(isoR (x,u)) . b = b
by A20, Def9;
per cases
( the addF of F . (a,b) <> x or the addF of F . (a,b) = x )
;
suppose A22:
the
addF of
F . (
a,
b)
<> x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
a,
b)
by A15, A21, Def8
.=
addR (
a1,
b1)
by Def5
.=
a + b
by A3, A22, Def4
.=
(isoR (x,u)) . (a + b)
by A22, Def9
;
verum end; suppose A23:
the
addF of
F . (
a,
b)
= x
;
((isoR (x,u)) . b1) + ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 + b2)thus ((isoR (x,u)) . a) + ((isoR (x,u)) . b) =
(addR (x,u)) . (
a,
b)
by A15, A21, Def8
.=
addR (
a1,
b1)
by Def5
.=
u
by A3, A23, Def4
.=
(isoR (x,u)) . (a + b)
by A23, Def9
;
verum end; end; end; end;
hence
isoR (x,u) is additive
; ( isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )
now for a, b being Element of F holds ((isoR (x,u)) . a) * ((isoR (x,u)) . b) = (isoR (x,u)) . (a * b)let a,
b be
Element of
F;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)A24:
(
a <> u &
b <> u )
by A1;
per cases
( a = x or a <> x )
;
suppose A25:
a = x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)then A26:
(isoR (x,u)) . a = u
by Def9;
per cases
( b = x or b <> x )
;
suppose A27:
b = x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)then A28:
(isoR (x,u)) . b = u
by Def9;
per cases
( the multF of F . (x,x) <> x or the multF of F . (x,x) = x )
;
suppose A29:
the
multF of
F . (
x,
x)
<> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
u,
u)
by A26, A28, Def8
.=
multR (
o,
o)
by Def7
.=
a * b
by A25, A27, A29, Def6
.=
(isoR (x,u)) . (a * b)
by A25, A27, A29, Def9
;
verum end; suppose A30:
the
multF of
F . (
x,
x)
= x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
u,
u)
by A26, A28, Def8
.=
multR (
o,
o)
by Def7
.=
u
by A30, Def6
.=
(isoR (x,u)) . (a * b)
by A25, A27, A30, Def9
;
verum end; end; suppose A31:
b <> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)then
not
b in {x}
by TARSKI:def 1;
then
b in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider b1 =
b as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A32:
(isoR (x,u)) . b = b
by A31, Def9;
per cases
( the multF of F . (x,b) <> x or the multF of F . (x,b) = x )
;
suppose A33:
the
multF of
F . (
x,
b)
<> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
u,
b)
by A26, A32, Def8
.=
multR (
o,
b1)
by Def7
.=
a * b
by A2, A25, A33, Def6
.=
(isoR (x,u)) . (a * b)
by A25, A33, Def9
;
verum end; suppose A34:
the
multF of
F . (
x,
b)
= x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
u,
b)
by A26, A32, Def8
.=
multR (
o,
b1)
by Def7
.=
u
by A24, A34, Def6
.=
(isoR (x,u)) . (a * b)
by A25, A34, Def9
;
verum end; end; end; suppose A35:
a <> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)then
not
a in {x}
by TARSKI:def 1;
then
a in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider a1 =
a as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A36:
(isoR (x,u)) . a = a
by A35, Def9;
per cases
( b = x or b <> x )
;
suppose A37:
b = x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)then A38:
(isoR (x,u)) . b = u
by Def9;
per cases
( the multF of F . (a,x) <> x or the multF of F . (a,x) = x )
;
suppose A39:
the
multF of
F . (
a,
x)
<> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
a,
u)
by A36, A38, Def8
.=
multR (
a1,
o)
by Def7
.=
a * b
by A2, A37, A39, Def6
.=
(isoR (x,u)) . (a * b)
by A37, A39, Def9
;
verum end; suppose A40:
the
multF of
F . (
a,
x)
= x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
a,
u)
by A36, A38, Def8
.=
multR (
a1,
o)
by Def7
.=
u
by A24, A40, Def6
.=
(isoR (x,u)) . (a * b)
by A37, A40, Def9
;
verum end; end; suppose A41:
b <> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)then
not
b in {x}
by TARSKI:def 1;
then
b in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider b1 =
b as
Element of
carr (
x,
u)
by XBOOLE_0:def 3;
A42:
(isoR (x,u)) . b = b
by A41, Def9;
per cases
( the multF of F . (a,b) <> x or the multF of F . (a,b) = x )
;
suppose A43:
the
multF of
F . (
a,
b)
<> x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
a,
b)
by A36, A42, Def8
.=
multR (
a1,
b1)
by Def7
.=
a * b
by A24, A43, Def6
.=
(isoR (x,u)) . (a * b)
by A43, Def9
;
verum end; suppose A44:
the
multF of
F . (
a,
b)
= x
;
((isoR (x,u)) . b1) * ((isoR (x,u)) . b2) = (isoR (x,u)) . (b1 * b2)thus ((isoR (x,u)) . a) * ((isoR (x,u)) . b) =
(multR (x,u)) . (
a,
b)
by A36, A42, Def8
.=
multR (
a1,
b1)
by Def7
.=
u
by A24, A44, Def6
.=
(isoR (x,u)) . (a * b)
by A44, Def9
;
verum end; end; end; end;
hence
isoR (x,u) is multiplicative
by GROUP_6:def 6; isoR (x,u) is unity-preserving
reconsider S = ExField (x,u) as Ring by A1, Th7, Th10, Th8, Th9, Th11;
1. F <> x
by Def2;
then (isoR (x,u)) . (1_ F) =
1. F
by Def9
.=
1_ S
by Def8
;
hence
isoR (x,u) is unity-preserving
; verum