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	⊢ ( 𝜑 → 𝐾 ∈ Field )
	fldhmf1.2	⊢ ( 𝜑 → 𝐿 ∈ Field )
	fldhmf1.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐾 RingHom 𝐿 ) )
	fldhmf1.4	⊢ 𝐴 = ( Base ‘ 𝐾 )
	fldhmf1.5	⊢ 𝐵 = ( Base ‘ 𝐿 )
Assertion	fldhmf1	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

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