| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fldhmf1.3 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐾 RingHom 𝐿)) | 
| 2 |  | fldhmf1.4 | . . . . 5
⊢ 𝐴 = (Base‘𝐾) | 
| 3 |  | fldhmf1.5 | . . . . 5
⊢ 𝐵 = (Base‘𝐿) | 
| 4 | 2, 3 | rhmf 20486 | . . . 4
⊢ (𝐹 ∈ (𝐾 RingHom 𝐿) → 𝐹:𝐴⟶𝐵) | 
| 5 | 1, 4 | syl 17 | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 6 | 1 | ad4antr 732 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐹 ∈ (𝐾 RingHom 𝐿)) | 
| 7 |  | rhmghm 20485 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝐾 RingHom 𝐿) → 𝐹 ∈ (𝐾 GrpHom 𝐿)) | 
| 8 | 6, 7 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐹 ∈ (𝐾 GrpHom 𝐿)) | 
| 9 |  | simp-4r 783 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ 𝐴) | 
| 10 |  | fldhmf1.1 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ Field) | 
| 11 |  | isfld 20741 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ Field ↔ (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing)) | 
| 12 | 10, 11 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing)) | 
| 13 | 12 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ DivRing) | 
| 14 | 13 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐾 ∈ DivRing) | 
| 15 |  | drnggrp 20740 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ DivRing → 𝐾 ∈ Grp) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐾 ∈ Grp) | 
| 17 |  | simpllr 775 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ 𝐴) | 
| 18 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(invg‘𝐾) = (invg‘𝐾) | 
| 19 | 2, 18 | grpinvcl 19006 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Grp ∧ 𝑏 ∈ 𝐴) → ((invg‘𝐾)‘𝑏) ∈ 𝐴) | 
| 20 | 16, 17, 19 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invg‘𝐾)‘𝑏) ∈ 𝐴) | 
| 21 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(+g‘𝐾) = (+g‘𝐾) | 
| 22 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(+g‘𝐿) = (+g‘𝐿) | 
| 23 | 2, 21, 22 | ghmlin 19240 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝐾 GrpHom 𝐿) ∧ 𝑎 ∈ 𝐴 ∧ ((invg‘𝐾)‘𝑏) ∈ 𝐴) → (𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) = ((𝐹‘𝑎)(+g‘𝐿)(𝐹‘((invg‘𝐾)‘𝑏)))) | 
| 24 | 8, 9, 20, 23 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) = ((𝐹‘𝑎)(+g‘𝐿)(𝐹‘((invg‘𝐾)‘𝑏)))) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(invg‘𝐿) = (invg‘𝐿) | 
| 26 | 2, 18, 25 | ghminv 19242 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (𝐾 GrpHom 𝐿) ∧ 𝑏 ∈ 𝐴) → (𝐹‘((invg‘𝐾)‘𝑏)) = ((invg‘𝐿)‘(𝐹‘𝑏))) | 
| 27 | 8, 17, 26 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘((invg‘𝐾)‘𝑏)) = ((invg‘𝐿)‘(𝐹‘𝑏))) | 
| 28 | 27 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘𝑎)(+g‘𝐿)(𝐹‘((invg‘𝐾)‘𝑏))) = ((𝐹‘𝑎)(+g‘𝐿)((invg‘𝐿)‘(𝐹‘𝑏)))) | 
| 29 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑏)) | 
| 30 | 29 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘𝑎)(+g‘𝐿)((invg‘𝐿)‘(𝐹‘𝑏))) = ((𝐹‘𝑏)(+g‘𝐿)((invg‘𝐿)‘(𝐹‘𝑏)))) | 
| 31 |  | fldhmf1.2 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐿 ∈ Field) | 
| 32 | 31 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → 𝐿 ∈ Field) | 
| 33 |  | isfld 20741 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ Field ↔ (𝐿 ∈ DivRing ∧ 𝐿 ∈ CRing)) | 
| 34 | 32, 33 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → (𝐿 ∈ DivRing ∧ 𝐿 ∈ CRing)) | 
| 35 | 34 | simpld 494 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → 𝐿 ∈ DivRing) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐿 ∈ DivRing) | 
| 37 |  | drngring 20737 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ DivRing → 𝐿 ∈ Ring) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐿 ∈ Ring) | 
| 39 | 38 | ringgrpd 20240 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐿 ∈ Grp) | 
| 40 | 6, 4 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐹:𝐴⟶𝐵) | 
| 41 | 40, 17 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑏) ∈ 𝐵) | 
| 42 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘𝐿) = (0g‘𝐿) | 
| 43 | 3, 22, 42, 25 | grprinv 19009 | . . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ Grp ∧ (𝐹‘𝑏) ∈ 𝐵) → ((𝐹‘𝑏)(+g‘𝐿)((invg‘𝐿)‘(𝐹‘𝑏))) = (0g‘𝐿)) | 
| 44 | 39, 41, 43 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘𝑏)(+g‘𝐿)((invg‘𝐿)‘(𝐹‘𝑏))) = (0g‘𝐿)) | 
| 45 | 30, 44 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘𝑎)(+g‘𝐿)((invg‘𝐿)‘(𝐹‘𝑏))) = (0g‘𝐿)) | 
| 46 | 28, 45 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘𝑎)(+g‘𝐿)(𝐹‘((invg‘𝐾)‘𝑏))) = (0g‘𝐿)) | 
| 47 | 24, 46 | eqtrd 2776 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) = (0g‘𝐿)) | 
| 48 | 47 | oveq1d 7447 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = ((0g‘𝐿)(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))))) | 
| 49 | 2, 21 | grpcl 18960 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Grp ∧ 𝑎 ∈ 𝐴 ∧ ((invg‘𝐾)‘𝑏) ∈ 𝐴) → (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ 𝐴) | 
| 50 | 16, 9, 20, 49 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ 𝐴) | 
| 51 | 2, 18 | grpinvinv 19024 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ Grp ∧ 𝑏 ∈ 𝐴) → ((invg‘𝐾)‘((invg‘𝐾)‘𝑏)) = 𝑏) | 
| 52 | 16, 17, 51 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invg‘𝐾)‘((invg‘𝐾)‘𝑏)) = 𝑏) | 
| 53 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ≠ 𝑏) | 
| 54 | 53 | necomd 2995 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ≠ 𝑎) | 
| 55 | 52, 54 | eqnetrd 3007 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invg‘𝐾)‘((invg‘𝐾)‘𝑏)) ≠ 𝑎) | 
| 56 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘𝐾) = (0g‘𝐾) | 
| 57 | 2, 21, 56, 18 | grpinvid2 19011 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ Grp ∧
((invg‘𝐾)‘𝑏) ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) → (((invg‘𝐾)‘((invg‘𝐾)‘𝑏)) = 𝑎 ↔ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) = (0g‘𝐾))) | 
| 58 | 57 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ Grp ∧
((invg‘𝐾)‘𝑏) ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) → (((invg‘𝐾)‘((invg‘𝐾)‘𝑏)) ≠ 𝑎 ↔ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ≠ (0g‘𝐾))) | 
| 59 | 16, 20, 9, 58 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (((invg‘𝐾)‘((invg‘𝐾)‘𝑏)) ≠ 𝑎 ↔ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ≠ (0g‘𝐾))) | 
| 60 | 55, 59 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ≠ (0g‘𝐾)) | 
| 61 | 50, 60 | jca 511 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ 𝐴 ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ≠ (0g‘𝐾))) | 
| 62 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Unit‘𝐾) =
(Unit‘𝐾) | 
| 63 | 2, 62, 56 | drngunit 20735 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ DivRing → ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾) ↔ ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ 𝐴 ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ≠ (0g‘𝐾)))) | 
| 64 | 14, 63 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾) ↔ ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ 𝐴 ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ≠ (0g‘𝐾)))) | 
| 65 | 61, 64 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾)) | 
| 66 |  | rhmunitinv 20512 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (𝐾 RingHom 𝐿) ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾)) → (𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) = ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) | 
| 67 | 6, 65, 66 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) = ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) | 
| 68 |  | elrhmunit 20511 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (𝐾 RingHom 𝐿) ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾)) → (𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐿)) | 
| 69 | 6, 65, 68 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐿)) | 
| 70 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Unit‘𝐿) =
(Unit‘𝐿) | 
| 71 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(invr‘𝐿) = (invr‘𝐿) | 
| 72 | 70, 71 | unitinvcl 20391 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ Ring ∧ (𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐿)) → ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ (Unit‘𝐿)) | 
| 73 | 38, 69, 72 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ (Unit‘𝐿)) | 
| 74 | 3, 70, 42 | drngunit 20735 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ DivRing →
(((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ (Unit‘𝐿) ↔ (((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵 ∧ ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ≠ (0g‘𝐿)))) | 
| 75 | 36, 74 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ (Unit‘𝐿) ↔ (((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵 ∧ ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ≠ (0g‘𝐿)))) | 
| 76 | 75 | biimpd 229 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ (Unit‘𝐿) → (((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵 ∧ ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ≠ (0g‘𝐿)))) | 
| 77 | 73, 76 | mpd 15 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵 ∧ ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ≠ (0g‘𝐿))) | 
| 78 | 77 | simpld 494 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invr‘𝐿)‘(𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵) | 
| 79 | 67, 78 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵) | 
| 80 | 38, 79 | jca 511 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐿 ∈ Ring ∧ (𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵)) | 
| 81 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(.r‘𝐿) = (.r‘𝐿) | 
| 82 | 3, 81, 42 | ringlz 20291 | . . . . . . . . . . . 12
⊢ ((𝐿 ∈ Ring ∧ (𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) ∈ 𝐵) → ((0g‘𝐿)(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = (0g‘𝐿)) | 
| 83 | 80, 82 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((0g‘𝐿)(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = (0g‘𝐿)) | 
| 84 | 48, 83 | eqtrd 2776 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = (0g‘𝐿)) | 
| 85 | 84 | eqcomd 2742 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (0g‘𝐿) = ((𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))))) | 
| 86 | 12 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ CRing) | 
| 87 | 86 | crngringd 20244 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ Ring) | 
| 88 | 87 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐾 ∈ Ring) | 
| 89 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(invr‘𝐾) = (invr‘𝐾) | 
| 90 | 62, 89 | unitinvcl 20391 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Ring ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾)) → ((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐾)) | 
| 91 | 88, 65, 90 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐾)) | 
| 92 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 93 | 92, 62 | unitcl 20376 | . . . . . . . . . . . . 13
⊢
(((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐾) → ((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Base‘𝐾)) | 
| 94 | 2 | eqcomi 2745 | . . . . . . . . . . . . 13
⊢
(Base‘𝐾) =
𝐴 | 
| 95 | 93, 94 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢
(((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ (Unit‘𝐾) → ((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ 𝐴) | 
| 96 | 91, 95 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ 𝐴) | 
| 97 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(.r‘𝐾) = (.r‘𝐾) | 
| 98 | 2, 97, 81 | rhmmul 20487 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐾 RingHom 𝐿) ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ 𝐴 ∧ ((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))) ∈ 𝐴) → (𝐹‘((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = ((𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))))) | 
| 99 | 6, 50, 96, 98 | syl3anc 1372 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = ((𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))))) | 
| 100 | 99 | eqcomd 2742 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝐹‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))(.r‘𝐿)(𝐹‘((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = (𝐹‘((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))))) | 
| 101 |  | drngring 20737 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ DivRing → 𝐾 ∈ Ring) | 
| 102 | 14, 101 | syl 17 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝐾 ∈ Ring) | 
| 103 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(1r‘𝐾) = (1r‘𝐾) | 
| 104 | 62, 89, 97, 103 | unitrinv 20395 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ Ring ∧ (𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)) ∈ (Unit‘𝐾)) → ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) = (1r‘𝐾)) | 
| 105 | 102, 65, 104 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏)))) = (1r‘𝐾)) | 
| 106 | 105 | fveq2d 6909 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = (𝐹‘(1r‘𝐾))) | 
| 107 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(1r‘𝐿) = (1r‘𝐿) | 
| 108 | 103, 107 | rhm1 20490 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (𝐾 RingHom 𝐿) → (𝐹‘(1r‘𝐾)) = (1r‘𝐿)) | 
| 109 | 6, 108 | syl 17 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘(1r‘𝐾)) = (1r‘𝐿)) | 
| 110 | 106, 109 | eqtrd 2776 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘((𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))(.r‘𝐾)((invr‘𝐾)‘(𝑎(+g‘𝐾)((invg‘𝐾)‘𝑏))))) = (1r‘𝐿)) | 
| 111 | 85, 100, 110 | 3eqtrd 2780 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (0g‘𝐿) = (1r‘𝐿)) | 
| 112 | 42, 107 | drngunz 20748 | . . . . . . . . . . . 12
⊢ (𝐿 ∈ DivRing →
(1r‘𝐿)
≠ (0g‘𝐿)) | 
| 113 | 35, 112 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → (1r‘𝐿) ≠
(0g‘𝐿)) | 
| 114 | 113 | necomd 2995 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → (0g‘𝐿) ≠
(1r‘𝐿)) | 
| 115 | 114 | adantr 480 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (0g‘𝐿) ≠
(1r‘𝐿)) | 
| 116 | 115 | neneqd 2944 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ (0g‘𝐿) = (1r‘𝐿)) | 
| 117 | 111, 116 | pm2.65da 816 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → ¬ (𝐹‘𝑎) = (𝐹‘𝑏)) | 
| 118 | 117 | neqned 2946 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) ∧ 𝑎 ≠ 𝑏) → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) | 
| 119 | 118 | ex 412 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐴) → (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏))) | 
| 120 | 119 | ralrimiva 3145 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏))) | 
| 121 | 120 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏))) | 
| 122 | 5, 121 | jca 511 | . 2
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)))) | 
| 123 |  | dff14a 7291 | . 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)))) | 
| 124 | 122, 123 | sylibr 234 | 1
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) |