mulgrhm

Description: The powers of the element 1 give a 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	mulgrhm	$⊢ R \in Ring \to F \in (ℤ_{ring} RingHom R)$

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		zring1	$⊢ 1 = 1_{ℤ_{ring}}$
6		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		zringring	$⊢ ℤ_{ring} \in Ring$
9	8	a1i	$⊢ R \in Ring \to ℤ_{ring} \in Ring$
10		id	$⊢ R \in Ring \to R \in Ring$
11		1z	$⊢ 1 \in ℤ$
12		oveq1	$⊢ n = 1 \to n \underset{˙}{\cdot} \underset{˙}{1} = 1 \underset{˙}{\cdot} \underset{˙}{1}$
13		ovex	$⊢ 1 \underset{˙}{\cdot} \underset{˙}{1} \in V$
14	12 2 13	fvmpt	$⊢ 1 \in ℤ \to F (1) = 1 \underset{˙}{\cdot} \underset{˙}{1}$
15	11 14	ax-mp	$⊢ F (1) = 1 \underset{˙}{\cdot} \underset{˙}{1}$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17	16 3	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
18	16 1	mulg1	$⊢ \underset{˙}{1} \in {Base}_{R} \to 1 \underset{˙}{\cdot} \underset{˙}{1} = \underset{˙}{1}$
19	17 18	syl	$⊢ R \in Ring \to 1 \underset{˙}{\cdot} \underset{˙}{1} = \underset{˙}{1}$
20	15 19	syl5eq	$⊢ R \in Ring \to F (1) = \underset{˙}{1}$
21		ringgrp	$⊢ R \in Ring \to R \in Grp$
22	21	adantr	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to R \in Grp$
23		simprr	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
24	17	adantr	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to \underset{˙}{1} \in {Base}_{R}$
25	16 1	mulgcl	$⊢ (R \in Grp \land y \in ℤ \land \underset{˙}{1} \in {Base}_{R}) \to y \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{R}$
26	22 23 24 25	syl3anc	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to y \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{R}$
27	16 7 3	ringlidm	$⊢ (R \in Ring \land y \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{R}) \to \underset{˙}{1} \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1}) = y \underset{˙}{\cdot} \underset{˙}{1}$
28	26 27	syldan	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to \underset{˙}{1} \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1}) = y \underset{˙}{\cdot} \underset{˙}{1}$
29	28	oveq2d	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to x \underset{˙}{\cdot} (\underset{˙}{1} \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1})) = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} \underset{˙}{1})$
30		simpl	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to R \in Ring$
31		simprl	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
32	16 1 7	mulgass2	$⊢ (R \in Ring \land (x \in ℤ \land \underset{˙}{1} \in {Base}_{R} \land y \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{R})) \to (x \underset{˙}{\cdot} \underset{˙}{1}) \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1}) = x \underset{˙}{\cdot} (\underset{˙}{1} \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1}))$
33	30 31 24 26 32	syl13anc	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to (x \underset{˙}{\cdot} \underset{˙}{1}) \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1}) = x \underset{˙}{\cdot} (\underset{˙}{1} \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1}))$
34	16 1	mulgass	$⊢ (R \in Grp \land (x \in ℤ \land y \in ℤ \land \underset{˙}{1} \in {Base}_{R})) \to x y \underset{˙}{\cdot} \underset{˙}{1} = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} \underset{˙}{1})$
35	22 31 23 24 34	syl13anc	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to x y \underset{˙}{\cdot} \underset{˙}{1} = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} \underset{˙}{1})$
36	29 33 35	3eqtr4rd	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to x y \underset{˙}{\cdot} \underset{˙}{1} = (x \underset{˙}{\cdot} \underset{˙}{1}) \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
37		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
38	37	adantl	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
39		oveq1	$⊢ n = x y \to n \underset{˙}{\cdot} \underset{˙}{1} = x y \underset{˙}{\cdot} \underset{˙}{1}$
40		ovex	$⊢ x y \underset{˙}{\cdot} \underset{˙}{1} \in V$
41	39 2 40	fvmpt	$⊢ x y \in ℤ \to F (x y) = x y \underset{˙}{\cdot} \underset{˙}{1}$
42	38 41	syl	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to F (x y) = x y \underset{˙}{\cdot} \underset{˙}{1}$
43		oveq1	$⊢ n = x \to n \underset{˙}{\cdot} \underset{˙}{1} = x \underset{˙}{\cdot} \underset{˙}{1}$
44		ovex	$⊢ x \underset{˙}{\cdot} \underset{˙}{1} \in V$
45	43 2 44	fvmpt	$⊢ x \in ℤ \to F (x) = x \underset{˙}{\cdot} \underset{˙}{1}$
46		oveq1	$⊢ n = y \to n \underset{˙}{\cdot} \underset{˙}{1} = y \underset{˙}{\cdot} \underset{˙}{1}$
47		ovex	$⊢ y \underset{˙}{\cdot} \underset{˙}{1} \in V$
48	46 2 47	fvmpt	$⊢ y \in ℤ \to F (y) = y \underset{˙}{\cdot} \underset{˙}{1}$
49	45 48	oveqan12d	$⊢ (x \in ℤ \land y \in ℤ) \to F (x) \cdot_{R} F (y) = (x \underset{˙}{\cdot} \underset{˙}{1}) \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
50	49	adantl	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to F (x) \cdot_{R} F (y) = (x \underset{˙}{\cdot} \underset{˙}{1}) \cdot_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
51	36 42 50	3eqtr4d	$⊢ (R \in Ring \land (x \in ℤ \land y \in ℤ)) \to F (x y) = F (x) \cdot_{R} F (y)$
52	1 2 16	mulgghm2	$⊢ (R \in Grp \land \underset{˙}{1} \in {Base}_{R}) \to F \in (ℤ_{ring} GrpHom R)$
53	21 17 52	syl2anc	$⊢ R \in Ring \to F \in (ℤ_{ring} GrpHom R)$
54	4 5 3 6 7 9 10 20 51 53	isrhm2d	$⊢ R \in Ring \to F \in (ℤ_{ring} RingHom R)$

Metamath Proof Explorer

Theorem mulgrhm

Proof