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 𝑆 ) )