let I be non degenerated commutative domRing-like Ring; :: thesis: canHom I is RingHomomorphism
A1: 0. I <> 1. I ;
for x, y being Element of I holds
( (canHom I) . (x + y) = ((canHom I) . x) + ((canHom I) . y) & (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
proof
reconsider res3 = [(1. I),(1. I)] as Element of Q. I by A1, Def1;
let x, y be Element of I; :: thesis: ( (canHom I) . (x + y) = ((canHom I) . x) + ((canHom I) . y) & (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
reconsider t1 = quotient (x,(1. I)), t2 = quotient (y,(1. I)) as Element of Q. I ;
A2: t1 `2 = [x,(1. I)] `2 by A1, Def20
.= 1. I ;
( t1 `2 <> 0. I & t2 `2 <> 0. I ) by Th2;
then A3: (t1 `2) * (t2 `2) <> 0. I by VECTSP_2:def 1;
then reconsider sum = [(((t1 `1) * (t2 `2)) + ((t2 `1) * (t1 `2))),((t1 `2) * (t2 `2))] as Element of Q. I by Def1;
A4: t2 `1 = [y,(1. I)] `1 by A1, Def20
.= y ;
reconsider prod = [((t1 `1) * (t2 `1)),((t1 `2) * (t2 `2))] as Element of Q. I by A3, Def1;
A5: ( QClass. t1 = (canHom I) . x & QClass. t2 = (canHom I) . y ) by Def21;
A6: (quotadd I) . ((QClass. t1),(QClass. t2)) = qadd ((QClass. t1),(QClass. t2)) by Def12
.= QClass. (padd (t1,t2)) by Th9
.= QClass. sum ;
A7: t1 `1 = [x,(1. I)] `1 by A1, Def20
.= x ;
A8: t2 `2 = [y,(1. I)] `2 by A1, Def20
.= 1. I ;
then A9: sum = [((t1 `1) + ((t2 `1) * (1. I))),((1. I) * (1. I))] by A2
.= [((t1 `1) + (t2 `1)),((1. I) * (1. I))]
.= [(x + y),(1. I)] by A4, A7 ;
thus (canHom I) . (x + y) = QClass. (quotient ((x + y),(1. I))) by Def21
.= ((canHom I) . x) + ((canHom I) . y) by A1, A5, A6, A9, Def20 ; :: thesis: ( (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
A10: (quotmult I) . ((QClass. t1),(QClass. t2)) = qmult ((QClass. t1),(QClass. t2)) by Def13
.= QClass. (pmult (t1,t2)) by Th10
.= QClass. prod ;
A11: prod = [(x * y),(1. I)] by A8, A2, A4, A7;
thus (canHom I) . (x * y) = QClass. (quotient ((x * y),(1. I))) by Def21
.= ((canHom I) . x) * ((canHom I) . y) by A1, A5, A10, A11, Def20 ; :: thesis: (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I)
A12: for u being object st u in QClass. res3 holds
u in q1. I
proof
let u be object ; :: thesis: ( u in QClass. res3 implies u in q1. I )
assume A13: u in QClass. res3 ; :: thesis: u in q1. I
then reconsider u = u as Element of Q. I ;
u `1 = (u `1) * (1. I)
.= (u `1) * (res3 `2)
.= (u `2) * (res3 `1) by A13, Def4
.= (u `2) * (1. I)
.= u `2 ;
hence u in q1. I by Def9; :: thesis: verum
end;
for u being object st u in q1. I holds
u in QClass. res3
proof
let u be object ; :: thesis: ( u in q1. I implies u in QClass. res3 )
assume A14: u in q1. I ; :: thesis: u in QClass. res3
then reconsider u = u as Element of Q. I ;
(u `1) * (res3 `2) = (u `1) * (1. I)
.= u `1
.= u `2 by A14, Def9
.= (u `2) * (1. I)
.= (u `2) * (res3 `1) ;
hence u in QClass. res3 by Def4; :: thesis: verum
end;
then A15: q1. I = QClass. res3 by A12, TARSKI:2;
thus (canHom I) . (1_ I) = QClass. (quotient ((1. I),(1. I))) by Def21
.= 1_ (the_Field_of_Quotients I) by A1, A15, Def20 ; :: thesis: verum
end;
then ( canHom I is additive & canHom I is multiplicative & canHom I is unity-preserving ) by GROUP_1:def 13, GROUP_6:def 6;
hence canHom I is RingHomomorphism ; :: thesis: verum