Metamath Proof Explorer

Theorem isrhmd

Description: Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015)

Ref Expression
Hypotheses isrhmd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isrhmd.o ⊢ 1 = ( 1r ‘ 𝑅 )
isrhmd.n ⊢ 𝑁 = ( 1r ‘ 𝑆 )
isrhmd.t ⊢ · = ( .r ‘ 𝑅 )
isrhmd.u ⊢ × = ( .r ‘ 𝑆 )
isrhmd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
isrhmd.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
isrhmd.ho ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑁 )
isrhmd.ht ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) × ( 𝐹 ‘ 𝑦 ) ) )
isrhmd.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
isrhmd.p ⊢ + = ( +g ‘ 𝑅 )
isrhmd.q ⊢ ⨣ = ( +g ‘ 𝑆 )
isrhmd.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
isrhmd.hp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
Assertion isrhmd ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )

Proof

Step Hyp Ref Expression
1 isrhmd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isrhmd.o ⊢ 1 = ( 1r ‘ 𝑅 )
3 isrhmd.n ⊢ 𝑁 = ( 1r ‘ 𝑆 )
4 isrhmd.t ⊢ · = ( .r ‘ 𝑅 )
5 isrhmd.u ⊢ × = ( .r ‘ 𝑆 )
6 isrhmd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 isrhmd.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
8 isrhmd.ho ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑁 )
9 isrhmd.ht ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) × ( 𝐹 ‘ 𝑦 ) ) )
10 isrhmd.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
11 isrhmd.p ⊢ + = ( +g ‘ 𝑅 )
12 isrhmd.q ⊢ ⨣ = ( +g ‘ 𝑆 )
13 isrhmd.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
14 isrhmd.hp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
15 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
16 6 15 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
17 ringgrp ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
18 7 17 syl ⊢ ( 𝜑 → 𝑆 ∈ Grp )
19 1 10 11 12 16 18 13 14 isghmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
20 1 2 3 4 5 6 7 8 9 19 isrhm2d ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )