chrrhm

Description: The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015)

		Ref	Expression
	Assertion	chrrhm	$⊢ F \in (R RingHom S) \to chr (S) ∥ chr (R)$

Proof

Step	Hyp	Ref	Expression
1		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
2		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
3	2	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
4	1 3	syl	$⊢ F \in (R RingHom S) \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
5		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	5 6	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
8		ffn	$⊢ ℤRHom (R) : ℤ ⟶ {Base}_{R} \to ℤRHom (R) Fn ℤ$
9	4 7 8	3syl	$⊢ F \in (R RingHom S) \to ℤRHom (R) Fn ℤ$
10		eqid	$⊢ chr (R) = chr (R)$
11	10	chrcl	$⊢ R \in Ring \to chr (R) \in ℕ_{0}$
12		nn0z	$⊢ chr (R) \in ℕ_{0} \to chr (R) \in ℤ$
13	1 11 12	3syl	$⊢ F \in (R RingHom S) \to chr (R) \in ℤ$
14		fvco2	$⊢ (ℤRHom (R) Fn ℤ \land chr (R) \in ℤ) \to (F \circ ℤRHom (R)) (chr (R)) = F (ℤRHom (R) (chr (R)))$
15	9 13 14	syl2anc	$⊢ F \in (R RingHom S) \to (F \circ ℤRHom (R)) (chr (R)) = F (ℤRHom (R) (chr (R)))$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	10 2 16	chrid	$⊢ R \in Ring \to ℤRHom (R) (chr (R)) = 0_{R}$
18	1 17	syl	$⊢ F \in (R RingHom S) \to ℤRHom (R) (chr (R)) = 0_{R}$
19	18	fveq2d	$⊢ F \in (R RingHom S) \to F (ℤRHom (R) (chr (R))) = F (0_{R})$
20	15 19	eqtrd	$⊢ F \in (R RingHom S) \to (F \circ ℤRHom (R)) (chr (R)) = F (0_{R})$
21		rhmco	$⊢ (F \in (R RingHom S) \land ℤRHom (R) \in (ℤ_{ring} RingHom R)) \to F \circ ℤRHom (R) \in (ℤ_{ring} RingHom S)$
22	4 21	mpdan	$⊢ F \in (R RingHom S) \to F \circ ℤRHom (R) \in (ℤ_{ring} RingHom S)$
23		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
24		eqid	$⊢ ℤRHom (S) = ℤRHom (S)$
25	24	zrhrhmb	$⊢ S \in Ring \to (F \circ ℤRHom (R) \in (ℤ_{ring} RingHom S) \leftrightarrow F \circ ℤRHom (R) = ℤRHom (S))$
26	23 25	syl	$⊢ F \in (R RingHom S) \to (F \circ ℤRHom (R) \in (ℤ_{ring} RingHom S) \leftrightarrow F \circ ℤRHom (R) = ℤRHom (S))$
27	22 26	mpbid	$⊢ F \in (R RingHom S) \to F \circ ℤRHom (R) = ℤRHom (S)$
28	27	fveq1d	$⊢ F \in (R RingHom S) \to (F \circ ℤRHom (R)) (chr (R)) = ℤRHom (S) (chr (R))$
29		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
30		eqid	$⊢ 0_{S} = 0_{S}$
31	16 30	ghmid	$⊢ F \in (R GrpHom S) \to F (0_{R}) = 0_{S}$
32	29 31	syl	$⊢ F \in (R RingHom S) \to F (0_{R}) = 0_{S}$
33	20 28 32	3eqtr3d	$⊢ F \in (R RingHom S) \to ℤRHom (S) (chr (R)) = 0_{S}$
34		eqid	$⊢ chr (S) = chr (S)$
35	34 24 30	chrdvds	$⊢ (S \in Ring \land chr (R) \in ℤ) \to (chr (S) ∥ chr (R) \leftrightarrow ℤRHom (S) (chr (R)) = 0_{S})$
36	23 13 35	syl2anc	$⊢ F \in (R RingHom S) \to (chr (S) ∥ chr (R) \leftrightarrow ℤRHom (S) (chr (R)) = 0_{S})$
37	33 36	mpbird	$⊢ F \in (R RingHom S) \to chr (S) ∥ chr (R)$

Metamath Proof Explorer

Theorem chrrhm

Proof