Metamath Proof Explorer

Theorem fldhmf1

Description: A field homomorphism is injective. This follows immediately from the definition of the ring homomorphism that sends the multiplicative identity to the multiplicative identity. (Contributed by metakunt, 7-Jan-2025)

Ref Expression
Hypotheses fldhmf1.1 
|- ( ph -> K e. Field )
fldhmf1.2 
|- ( ph -> L e. Field )
fldhmf1.3 
|- ( ph -> F e. ( K RingHom L ) )
fldhmf1.4 
|- A = ( Base ` K )
fldhmf1.5 
|- B = ( Base ` L )
Assertion fldhmf1 
|- ( ph -> F : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 fldhmf1.1 
 |-  ( ph -> K e. Field )
2 fldhmf1.2 
 |-  ( ph -> L e. Field )
3 fldhmf1.3 
 |-  ( ph -> F e. ( K RingHom L ) )
4 fldhmf1.4 
 |-  A = ( Base ` K )
5 fldhmf1.5 
 |-  B = ( Base ` L )
6 4 5 rhmf 
 |-  ( F e. ( K RingHom L ) -> F : A --> B )
7 3 6 syl 
 |-  ( ph -> F : A --> B )
8 3 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> F e. ( K RingHom L ) )
9 rhmghm 
 |-  ( F e. ( K RingHom L ) -> F e. ( K GrpHom L ) )
10 8 9 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> F e. ( K GrpHom L ) )
11 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> a e. A )
12 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
13 1 12 sylib 
 |-  ( ph -> ( K e. DivRing /\ K e. CRing ) )
14 13 simpld 
 |-  ( ph -> K e. DivRing )
15 14 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> K e. DivRing )
16 drnggrp 
 |-  ( K e. DivRing -> K e. Grp )
17 15 16 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> K e. Grp )
18 simpllr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> b e. A )
19 eqid 
 |-  ( invg ` K ) = ( invg ` K )
20 4 19 grpinvcl 
 |-  ( ( K e. Grp /\ b e. A ) -> ( ( invg ` K ) ` b ) e. A )
21 17 18 20 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invg ` K ) ` b ) e. A )
22 eqid 
 |-  ( +g ` K ) = ( +g ` K )
23 eqid 
 |-  ( +g ` L ) = ( +g ` L )
24 4 22 23 ghmlin 
 |-  ( ( F e. ( K GrpHom L ) /\ a e. A /\ ( ( invg ` K ) ` b ) e. A ) -> ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) = ( ( F ` a ) ( +g ` L ) ( F ` ( ( invg ` K ) ` b ) ) ) )
25 10 11 21 24 syl3anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) = ( ( F ` a ) ( +g ` L ) ( F ` ( ( invg ` K ) ` b ) ) ) )
26 eqid 
 |-  ( invg ` L ) = ( invg ` L )
27 4 19 26 ghminv 
 |-  ( ( F e. ( K GrpHom L ) /\ b e. A ) -> ( F ` ( ( invg ` K ) ` b ) ) = ( ( invg ` L ) ` ( F ` b ) ) )
28 10 18 27 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( ( invg ` K ) ` b ) ) = ( ( invg ` L ) ` ( F ` b ) ) )
29 28 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` a ) ( +g ` L ) ( F ` ( ( invg ` K ) ` b ) ) ) = ( ( F ` a ) ( +g ` L ) ( ( invg ` L ) ` ( F ` b ) ) ) )
30 simpr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` a ) = ( F ` b ) )
31 30 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` a ) ( +g ` L ) ( ( invg ` L ) ` ( F ` b ) ) ) = ( ( F ` b ) ( +g ` L ) ( ( invg ` L ) ` ( F ` b ) ) ) )
32 2 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> L e. Field )
33 isfld 
 |-  ( L e. Field <-> ( L e. DivRing /\ L e. CRing ) )
34 32 33 sylib 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> ( L e. DivRing /\ L e. CRing ) )
35 34 simpld 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> L e. DivRing )
36 35 adantr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> L e. DivRing )
37 drngring 
 |-  ( L e. DivRing -> L e. Ring )
38 36 37 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> L e. Ring )
39 38 ringgrpd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> L e. Grp )
40 8 6 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> F : A --> B )
41 40 18 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` b ) e. B )
42 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
43 5 23 42 26 grprinv 
 |-  ( ( L e. Grp /\ ( F ` b ) e. B ) -> ( ( F ` b ) ( +g ` L ) ( ( invg ` L ) ` ( F ` b ) ) ) = ( 0g ` L ) )
44 39 41 43 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` b ) ( +g ` L ) ( ( invg ` L ) ` ( F ` b ) ) ) = ( 0g ` L ) )
45 31 44 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` a ) ( +g ` L ) ( ( invg ` L ) ` ( F ` b ) ) ) = ( 0g ` L ) )
46 29 45 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` a ) ( +g ` L ) ( F ` ( ( invg ` K ) ` b ) ) ) = ( 0g ` L ) )
47 25 46 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) = ( 0g ` L ) )
48 47 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( ( 0g ` L ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) )
49 4 22 grpcl 
 |-  ( ( K e. Grp /\ a e. A /\ ( ( invg ` K ) ` b ) e. A ) -> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. A )
50 17 11 21 49 syl3anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. A )
51 4 19 grpinvinv 
 |-  ( ( K e. Grp /\ b e. A ) -> ( ( invg ` K ) ` ( ( invg ` K ) ` b ) ) = b )
52 17 18 51 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invg ` K ) ` ( ( invg ` K ) ` b ) ) = b )
53 simplr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> a =/= b )
54 53 necomd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> b =/= a )
55 52 54 eqnetrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invg ` K ) ` ( ( invg ` K ) ` b ) ) =/= a )
56 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
57 4 22 56 19 grpinvid2 
 |-  ( ( K e. Grp /\ ( ( invg ` K ) ` b ) e. A /\ a e. A ) -> ( ( ( invg ` K ) ` ( ( invg ` K ) ` b ) ) = a <-> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) = ( 0g ` K ) ) )
58 57 necon3bid 
 |-  ( ( K e. Grp /\ ( ( invg ` K ) ` b ) e. A /\ a e. A ) -> ( ( ( invg ` K ) ` ( ( invg ` K ) ` b ) ) =/= a <-> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) =/= ( 0g ` K ) ) )
59 17 21 11 58 syl3anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( ( invg ` K ) ` ( ( invg ` K ) ` b ) ) =/= a <-> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) =/= ( 0g ` K ) ) )
60 55 59 mpbid 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) =/= ( 0g ` K ) )
61 50 60 jca 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. A /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) =/= ( 0g ` K ) ) )
62 eqid 
 |-  ( Unit ` K ) = ( Unit ` K )
63 4 62 56 drngunit 
 |-  ( K e. DivRing -> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) <-> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. A /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) =/= ( 0g ` K ) ) ) )
64 15 63 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) <-> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. A /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) =/= ( 0g ` K ) ) ) )
65 61 64 mpbird 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) )
66 rhmunitinv 
 |-  ( ( F e. ( K RingHom L ) /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) ) -> ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) = ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) )
67 8 65 66 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) = ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) )
68 elrhmunit 
 |-  ( ( F e. ( K RingHom L ) /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) ) -> ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` L ) )
69 8 65 68 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` L ) )
70 eqid 
 |-  ( Unit ` L ) = ( Unit ` L )
71 eqid 
 |-  ( invr ` L ) = ( invr ` L )
72 70 71 unitinvcl 
 |-  ( ( L e. Ring /\ ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` L ) ) -> ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. ( Unit ` L ) )
73 38 69 72 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. ( Unit ` L ) )
74 5 70 42 drngunit 
 |-  ( L e. DivRing -> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. ( Unit ` L ) <-> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B /\ ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) =/= ( 0g ` L ) ) ) )
75 36 74 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. ( Unit ` L ) <-> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B /\ ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) =/= ( 0g ` L ) ) ) )
76 75 biimpd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. ( Unit ` L ) -> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B /\ ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) =/= ( 0g ` L ) ) ) )
77 73 76 mpd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B /\ ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) =/= ( 0g ` L ) ) )
78 77 simpld 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invr ` L ) ` ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B )
79 67 78 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B )
80 38 79 jca 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( L e. Ring /\ ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B ) )
81 eqid 
 |-  ( .r ` L ) = ( .r ` L )
82 5 81 42 ringlz 
 |-  ( ( L e. Ring /\ ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) e. B ) -> ( ( 0g ` L ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( 0g ` L ) )
83 80 82 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( 0g ` L ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( 0g ` L ) )
84 48 83 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( 0g ` L ) )
85 84 eqcomd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( 0g ` L ) = ( ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) )
86 13 simprd 
 |-  ( ph -> K e. CRing )
87 86 crngringd 
 |-  ( ph -> K e. Ring )
88 87 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> K e. Ring )
89 eqid 
 |-  ( invr ` K ) = ( invr ` K )
90 62 89 unitinvcl 
 |-  ( ( K e. Ring /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) ) -> ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` K ) )
91 88 65 90 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` K ) )
92 eqid 
 |-  ( Base ` K ) = ( Base ` K )
93 92 62 unitcl 
 |-  ( ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` K ) -> ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Base ` K ) )
94 4 eqcomi 
 |-  ( Base ` K ) = A
95 93 94 eleqtrdi 
 |-  ( ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. ( Unit ` K ) -> ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. A )
96 91 95 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. A )
97 eqid 
 |-  ( .r ` K ) = ( .r ` K )
98 4 97 81 rhmmul 
 |-  ( ( F e. ( K RingHom L ) /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. A /\ ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) e. A ) -> ( F ` ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) )
99 8 50 96 98 syl3anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) )
100 99 eqcomd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( F ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ( .r ` L ) ( F ` ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( F ` ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) )
101 drngring 
 |-  ( K e. DivRing -> K e. Ring )
102 15 101 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> K e. Ring )
103 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
104 62 89 97 103 unitrinv 
 |-  ( ( K e. Ring /\ ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) e. ( Unit ` K ) ) -> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) = ( 1r ` K ) )
105 102 65 104 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) = ( 1r ` K ) )
106 105 fveq2d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( F ` ( 1r ` K ) ) )
107 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
108 103 107 rhm1 
 |-  ( F e. ( K RingHom L ) -> ( F ` ( 1r ` K ) ) = ( 1r ` L ) )
109 8 108 syl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( 1r ` K ) ) = ( 1r ` L ) )
110 106 109 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ( .r ` K ) ( ( invr ` K ) ` ( a ( +g ` K ) ( ( invg ` K ) ` b ) ) ) ) ) = ( 1r ` L ) )
111 85 100 110 3eqtrd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( 0g ` L ) = ( 1r ` L ) )
112 42 107 drngunz 
 |-  ( L e. DivRing -> ( 1r ` L ) =/= ( 0g ` L ) )
113 35 112 syl 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> ( 1r ` L ) =/= ( 0g ` L ) )
114 113 necomd 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> ( 0g ` L ) =/= ( 1r ` L ) )
115 114 adantr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> ( 0g ` L ) =/= ( 1r ` L ) )
116 115 neneqd 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) /\ ( F ` a ) = ( F ` b ) ) -> -. ( 0g ` L ) = ( 1r ` L ) )
117 111 116 pm2.65da 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> -. ( F ` a ) = ( F ` b ) )
118 117 neqned 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. A ) /\ a =/= b ) -> ( F ` a ) =/= ( F ` b ) )
119 118 ex 
 |-  ( ( ( ph /\ a e. A ) /\ b e. A ) -> ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) )
120 119 ralrimiva 
 |-  ( ( ph /\ a e. A ) -> A. b e. A ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) )
121 120 ralrimiva 
 |-  ( ph -> A. a e. A A. b e. A ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) )
122 7 121 jca 
 |-  ( ph -> ( F : A --> B /\ A. a e. A A. b e. A ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) ) )
123 dff14a 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. a e. A A. b e. A ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) ) )
124 122 123 sylibr 
 |-  ( ph -> F : A -1-1-> B )