Metamath Proof Explorer

Theorem isrhm2d

Description: Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-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 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) × ( 𝐹 ‘ 𝑦 ) ) )
isrhm2d.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
Assertion isrhm2d ( 𝜑 → 𝐹 ∈ ( 𝑅 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 isrhm2d.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
11 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
12 11 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
13 6 12 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
14 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
15 14 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
16 7 15 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
17 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18 1 17 ghmf ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
19 10 18 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
20 9 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) × ( 𝐹 ‘ 𝑦 ) ) )
21 11 2 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
22 21 fveq2i ⊢ ( 𝐹 ‘ 1 ) = ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
23 14 3 ringidval ⊢ 𝑁 = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
24 8 22 23 3eqtr3g ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) )
25 19 20 24 3jca ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) × ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) ) )
26 11 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
27 14 17 mgpbas ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
28 11 4 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
29 14 5 mgpplusg ⊢ × = ( +g ‘ ( mulGrp ‘ 𝑆 ) )
30 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
31 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
32 26 27 28 29 30 31 ismhm ⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ↔ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( mulGrp ‘ 𝑆 ) ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) × ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) ) ) )
33 13 16 25 32 syl21anbrc ⊢ ( 𝜑 → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
34 10 33 jca ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
35 11 14 isrhm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) )
36 6 7 34 35 syl21anbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )