Metamath Proof Explorer

Theorem chrrhm

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

Ref Expression
Assertion chrrhm ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( chr ‘ 𝑆 ) ∥ ( chr ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
2 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
3 2 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
4 1 3 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
5 zringbas ⊢ ℤ = ( Base ‘ ℤring )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 5 6 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
8 ffn ⊢ ( ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
9 4 7 8 3syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
10 eqid ⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
11 10 chrcl ⊢ ( 𝑅 ∈ Ring → ( chr ‘ 𝑅 ) ∈ ℕ0 )
12 nn0z ⊢ ( ( chr ‘ 𝑅 ) ∈ ℕ0 → ( chr ‘ 𝑅 ) ∈ ℤ )
13 1 11 12 3syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( chr ‘ 𝑅 ) ∈ ℤ )
14 fvco2 ⊢ ( ( ( ℤRHom ‘ 𝑅 ) Fn ℤ ∧ ( chr ‘ 𝑅 ) ∈ ℤ ) → ( ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ‘ ( chr ‘ 𝑅 ) ) = ( 𝐹 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( chr ‘ 𝑅 ) ) ) )
15 9 13 14 syl2anc ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ‘ ( chr ‘ 𝑅 ) ) = ( 𝐹 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( chr ‘ 𝑅 ) ) ) )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 10 2 16 chrid ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ ( chr ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
18 1 17 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( chr ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
19 18 fveq2d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( chr ‘ 𝑅 ) ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) )
20 15 19 eqtrd ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ‘ ( chr ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) )
21 rhmco ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) ) → ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ∈ ( ℤring RingHom 𝑆 ) )
22 4 21 mpdan ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ∈ ( ℤring RingHom 𝑆 ) )
23 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
24 eqid ⊢ ( ℤRHom ‘ 𝑆 ) = ( ℤRHom ‘ 𝑆 )
25 24 zrhrhmb ⊢ ( 𝑆 ∈ Ring → ( ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ∈ ( ℤring RingHom 𝑆 ) ↔ ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) = ( ℤRHom ‘ 𝑆 ) ) )
26 23 25 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ∈ ( ℤring RingHom 𝑆 ) ↔ ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) = ( ℤRHom ‘ 𝑆 ) ) )
27 22 26 mpbid ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) = ( ℤRHom ‘ 𝑆 ) )
28 27 fveq1d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹 ∘ ( ℤRHom ‘ 𝑅 ) ) ‘ ( chr ‘ 𝑅 ) ) = ( ( ℤRHom ‘ 𝑆 ) ‘ ( chr ‘ 𝑅 ) ) )
29 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
30 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
31 16 30 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
32 29 31 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
33 20 28 32 3eqtr3d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( ℤRHom ‘ 𝑆 ) ‘ ( chr ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
34 eqid ⊢ ( chr ‘ 𝑆 ) = ( chr ‘ 𝑆 )
35 34 24 30 chrdvds ⊢ ( ( 𝑆 ∈ Ring ∧ ( chr ‘ 𝑅 ) ∈ ℤ ) → ( ( chr ‘ 𝑆 ) ∥ ( chr ‘ 𝑅 ) ↔ ( ( ℤRHom ‘ 𝑆 ) ‘ ( chr ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) ) )
36 23 13 35 syl2anc ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( chr ‘ 𝑆 ) ∥ ( chr ‘ 𝑅 ) ↔ ( ( ℤRHom ‘ 𝑆 ) ‘ ( chr ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) ) )
37 33 36 mpbird ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( chr ‘ 𝑆 ) ∥ ( chr ‘ 𝑅 ) )