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	⊢ · = ( ._g ‘ 𝑅 )
	mulgghm2.f	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
	mulgrhm.1	⊢ 1 = ( 1_r ‘ 𝑅 )
Assertion	mulgrhm2	⊢ ( 𝑅 ∈ Ring → ( ℤ_ring RingHom 𝑅 ) = { 𝐹 } )

Proof

Step	Hyp	Ref	Expression
1		mulgghm2.m	⊢ · = ( ._g ‘ 𝑅 )
2		mulgghm2.f	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
3		mulgrhm.1	⊢ 1 = ( 1_r ‘ 𝑅 )
4		zringbas	⊢ ℤ = ( Base ‘ ℤ_ring )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	4 5	rhmf	⊢ ( 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) → 𝑓 : ℤ ⟶ ( Base ‘ 𝑅 ) )
7	6	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) → 𝑓 : ℤ ⟶ ( Base ‘ 𝑅 ) )
8	7	feqmptd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) → 𝑓 = ( 𝑛 ∈ ℤ ↦ ( 𝑓 ‘ 𝑛 ) ) )
9		rhmghm	⊢ ( 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) → 𝑓 ∈ ( ℤ_ring GrpHom 𝑅 ) )
10	9	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → 𝑓 ∈ ( ℤ_ring GrpHom 𝑅 ) )
11		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
12		1zzd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℤ )
13		eqid	⊢ ( ._g ‘ ℤ_ring ) = ( ._g ‘ ℤ_ring )
14	4 13 1	ghmmulg	⊢ ( ( 𝑓 ∈ ( ℤ_ring GrpHom 𝑅 ) ∧ 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑓 ‘ ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) ) = ( 𝑛 · ( 𝑓 ‘ 1 ) ) )
15	10 11 12 14	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑓 ‘ ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) ) = ( 𝑛 · ( 𝑓 ‘ 1 ) ) )
16		ax-1cn	⊢ 1 ∈ ℂ
17		cnfldmulg	⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℂ ) → ( 𝑛 ( ._g ‘ ℂ_fld ) 1 ) = ( 𝑛 · 1 ) )
18	16 17	mpan2	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( ._g ‘ ℂ_fld ) 1 ) = ( 𝑛 · 1 ) )
19		1z	⊢ 1 ∈ ℤ
20	18	adantr	⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑛 ( ._g ‘ ℂ_fld ) 1 ) = ( 𝑛 · 1 ) )
21		zringmulg	⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) = ( 𝑛 · 1 ) )
22	20 21	eqtr4d	⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑛 ( ._g ‘ ℂ_fld ) 1 ) = ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) )
23	19 22	mpan2	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( ._g ‘ ℂ_fld ) 1 ) = ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) )
24		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
25	24	mulridd	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 1 ) = 𝑛 )
26	18 23 25	3eqtr3d	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) = 𝑛 )
27	26	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) = 𝑛 )
28	27	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑓 ‘ ( 𝑛 ( ._g ‘ ℤ_ring ) 1 ) ) = ( 𝑓 ‘ 𝑛 ) )
29		zring1	⊢ 1 = ( 1_r ‘ ℤ_ring )
30	29 3	rhm1	⊢ ( 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) → ( 𝑓 ‘ 1 ) = 1 )
31	30	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑓 ‘ 1 ) = 1 )
32	31	oveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · ( 𝑓 ‘ 1 ) ) = ( 𝑛 · 1 ) )
33	15 28 32	3eqtr3d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑓 ‘ 𝑛 ) = ( 𝑛 · 1 ) )
34	33	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) → ( 𝑛 ∈ ℤ ↦ ( 𝑓 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )
35	8 34	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) → 𝑓 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )
36	35 2	eqtr4di	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) → 𝑓 = 𝐹 )
37		velsn	⊢ ( 𝑓 ∈ { 𝐹 } ↔ 𝑓 = 𝐹 )
38	36 37	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) ) → 𝑓 ∈ { 𝐹 } )
39	38	ex	⊢ ( 𝑅 ∈ Ring → ( 𝑓 ∈ ( ℤ_ring RingHom 𝑅 ) → 𝑓 ∈ { 𝐹 } ) )
40	39	ssrdv	⊢ ( 𝑅 ∈ Ring → ( ℤ_ring RingHom 𝑅 ) ⊆ { 𝐹 } )
41	1 2 3	mulgrhm	⊢ ( 𝑅 ∈ Ring → 𝐹 ∈ ( ℤ_ring RingHom 𝑅 ) )
42	41	snssd	⊢ ( 𝑅 ∈ Ring → { 𝐹 } ⊆ ( ℤ_ring RingHom 𝑅 ) )
43	40 42	eqssd	⊢ ( 𝑅 ∈ Ring → ( ℤ_ring RingHom 𝑅 ) = { 𝐹 } )

Metamath Proof Explorer

Theorem mulgrhm2

Proof