mulgrhm2

Description: The powers of the element 1 give the unique ring homomorphism from ZZ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypotheses	mulgghm2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mulgghm2.f	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
	mulgrhm.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	mulgrhm2	$⊢ R \in Ring \to ℤ_{ring} RingHom R = \{F\}$

Proof

Step	Hyp	Ref	Expression
1		mulgghm2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
2		mulgghm2.f	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
3		mulgrhm.1	$⊢ \underset{˙}{1} = 1_{R}$
4		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	4 5	rhmf	$⊢ f \in (ℤ_{ring} RingHom R) \to f : ℤ ⟶ {Base}_{R}$
7	6	adantl	$⊢ (R \in Ring \land f \in (ℤ_{ring} RingHom R)) \to f : ℤ ⟶ {Base}_{R}$
8	7	feqmptd	$⊢ (R \in Ring \land f \in (ℤ_{ring} RingHom R)) \to f = (n \in ℤ ⟼ f (n))$
9		rhmghm	$⊢ f \in (ℤ_{ring} RingHom R) \to f \in (ℤ_{ring} GrpHom R)$
10	9	ad2antlr	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to f \in (ℤ_{ring} GrpHom R)$
11		simpr	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to n \in ℤ$
12		1zzd	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to 1 \in ℤ$
13		eqid	$⊢ \cdot_{ℤ_{ring}} = \cdot_{ℤ_{ring}}$
14	4 13 1	ghmmulg	$⊢ (f \in (ℤ_{ring} GrpHom R) \land n \in ℤ \land 1 \in ℤ) \to f (n \cdot_{ℤ_{ring}} 1) = n \underset{˙}{\cdot} f (1)$
15	10 11 12 14	syl3anc	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to f (n \cdot_{ℤ_{ring}} 1) = n \underset{˙}{\cdot} f (1)$
16		ax-1cn	$⊢ 1 \in ℂ$
17		cnfldmulg	$⊢ (n \in ℤ \land 1 \in ℂ) \to n \cdot_{ℂ_{fld}} 1 = n \cdot 1$
18	16 17	mpan2	$⊢ n \in ℤ \to n \cdot_{ℂ_{fld}} 1 = n \cdot 1$
19		1z	$⊢ 1 \in ℤ$
20	18	adantr	$⊢ (n \in ℤ \land 1 \in ℤ) \to n \cdot_{ℂ_{fld}} 1 = n \cdot 1$
21		zringmulg	$⊢ (n \in ℤ \land 1 \in ℤ) \to n \cdot_{ℤ_{ring}} 1 = n \cdot 1$
22	20 21	eqtr4d	$⊢ (n \in ℤ \land 1 \in ℤ) \to n \cdot_{ℂ_{fld}} 1 = n \cdot_{ℤ_{ring}} 1$
23	19 22	mpan2	$⊢ n \in ℤ \to n \cdot_{ℂ_{fld}} 1 = n \cdot_{ℤ_{ring}} 1$
24		zcn	$⊢ n \in ℤ \to n \in ℂ$
25	24	mulid1d	$⊢ n \in ℤ \to n \cdot 1 = n$
26	18 23 25	3eqtr3d	$⊢ n \in ℤ \to n \cdot_{ℤ_{ring}} 1 = n$
27	26	adantl	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to n \cdot_{ℤ_{ring}} 1 = n$
28	27	fveq2d	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to f (n \cdot_{ℤ_{ring}} 1) = f (n)$
29		zring1	$⊢ 1 = 1_{ℤ_{ring}}$
30	29 3	rhm1	$⊢ f \in (ℤ_{ring} RingHom R) \to f (1) = \underset{˙}{1}$
31	30	ad2antlr	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to f (1) = \underset{˙}{1}$
32	31	oveq2d	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to n \underset{˙}{\cdot} f (1) = n \underset{˙}{\cdot} \underset{˙}{1}$
33	15 28 32	3eqtr3d	$⊢ ((R \in Ring \land f \in (ℤ_{ring} RingHom R)) \land n \in ℤ) \to f (n) = n \underset{˙}{\cdot} \underset{˙}{1}$
34	33	mpteq2dva	$⊢ (R \in Ring \land f \in (ℤ_{ring} RingHom R)) \to (n \in ℤ ⟼ f (n)) = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
35	8 34	eqtrd	$⊢ (R \in Ring \land f \in (ℤ_{ring} RingHom R)) \to f = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
36	35 2	eqtr4di	$⊢ (R \in Ring \land f \in (ℤ_{ring} RingHom R)) \to f = F$
37		velsn	$⊢ f \in \{F\} \leftrightarrow f = F$
38	36 37	sylibr	$⊢ (R \in Ring \land f \in (ℤ_{ring} RingHom R)) \to f \in \{F\}$
39	38	ex	$⊢ R \in Ring \to (f \in (ℤ_{ring} RingHom R) \to f \in \{F\})$
40	39	ssrdv	$⊢ R \in Ring \to ℤ_{ring} RingHom R \subseteq \{F\}$
41	1 2 3	mulgrhm	$⊢ R \in Ring \to F \in (ℤ_{ring} RingHom R)$
42	41	snssd	$⊢ R \in Ring \to \{F\} \subseteq ℤ_{ring} RingHom R$
43	40 42	eqssd	$⊢ R \in Ring \to ℤ_{ring} RingHom R = \{F\}$

Metamath Proof Explorer

Theorem mulgrhm2

Proof