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	$⊢ φ \to K \in Field$
	fldhmf1.2	$⊢ φ \to L \in Field$
	fldhmf1.3	$⊢ φ \to F \in (K RingHom L)$
	fldhmf1.4	$⊢ A = {Base}_{K}$
	fldhmf1.5	$⊢ B = {Base}_{L}$
Assertion	fldhmf1	$⊢ φ \to F : A \underset{1-1}{⟶} B$

Proof

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

Metamath Proof Explorer

Theorem fldhmf1

Proof