let F be non almost_trivial Field; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: 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; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)
A3: ( a <> u & b <> u ) by A2;

per cases ( a = x or a <> x ) ;

suppose A4: a = x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

then A5: (isoR (x,u)) . a = u by Def9;

per cases ( b = x or b <> x ) ;

suppose A6: b = x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

suppose A9: the addF of F . (x,x) = x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

end;

end;

suppose A10: b <> x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

suppose A13: the addF of F . (x,b) = x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A14: a <> x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

suppose A19: the addF of F . (a,x) = x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

end;

end;

suppose A20: b <> x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

suppose A23: the addF of F . (a,b) = x ; :: thesis: ((isoR (x,u)) . b₁) + ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ + b₂)

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 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence isoR (x,u) is additive ; :: thesis: ( isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )

now :: thesis: 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; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)
A24: ( a <> u & b <> u ) by A1;

per cases ( a = x or a <> x ) ;

suppose A25: a = x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

then A26: (isoR (x,u)) . a = u by Def9;

per cases ( b = x or b <> x ) ;

suppose A27: b = x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

suppose A30: the multF of F . (x,x) = x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

end;

end;

suppose A31: b <> x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

suppose A34: the multF of F . (x,b) = x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A35: a <> x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

suppose A40: the multF of F . (a,x) = x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

end;

end;

suppose A41: b <> x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

suppose A44: the multF of F . (a,b) = x ; :: thesis: ((isoR (x,u)) . b₁) * ((isoR (x,u)) . b₂) = (isoR (x,u)) . (b₁ * b₂)

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 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence isoR (x,u) is multiplicative by GROUP_6:def 6; :: thesis: 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 ; :: thesis: verum