isrhm2d

Description: Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015)

	Ref	Expression
Hypotheses	isrhmd.b	$⊢ B = {Base}_{R}$
	isrhmd.o	$⊢ \underset{˙}{1} = 1_{R}$
	isrhmd.n	$⊢ N = 1_{S}$
	isrhmd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	isrhmd.u	$⊢ \underset{˙}{\times} = \cdot_{S}$
	isrhmd.r	$⊢ φ \to R \in Ring$
	isrhmd.s	$⊢ φ \to S \in Ring$
	isrhmd.ho	$⊢ φ \to F (\underset{˙}{1}) = N$
	isrhmd.ht	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)$
	isrhm2d.f	$⊢ φ \to F \in (R GrpHom S)$
Assertion	isrhm2d	$⊢ φ \to F \in (R RingHom S)$

Proof

Step	Hyp	Ref	Expression
1		isrhmd.b	$⊢ B = {Base}_{R}$
2		isrhmd.o	$⊢ \underset{˙}{1} = 1_{R}$
3		isrhmd.n	$⊢ N = 1_{S}$
4		isrhmd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		isrhmd.u	$⊢ \underset{˙}{\times} = \cdot_{S}$
6		isrhmd.r	$⊢ φ \to R \in Ring$
7		isrhmd.s	$⊢ φ \to S \in Ring$
8		isrhmd.ho	$⊢ φ \to F (\underset{˙}{1}) = N$
9		isrhmd.ht	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)$
10		isrhm2d.f	$⊢ φ \to F \in (R GrpHom S)$
11		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
12	11	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
13	6 12	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
14		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
15	14	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
16	7 15	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
17		eqid	$⊢ {Base}_{S} = {Base}_{S}$
18	1 17	ghmf	$⊢ F \in (R GrpHom S) \to F : B ⟶ {Base}_{S}$
19	10 18	syl	$⊢ φ \to F : B ⟶ {Base}_{S}$
20	9	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)$
21	11 2	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
22	21	fveq2i	$⊢ F (\underset{˙}{1}) = F (0_{{mulGrp}_{R}})$
23	14 3	ringidval	$⊢ N = 0_{{mulGrp}_{S}}$
24	8 22 23	3eqtr3g	$⊢ φ \to F (0_{{mulGrp}_{R}}) = 0_{{mulGrp}_{S}}$
25	19 20 24	3jca	$⊢ φ \to (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y) \land F (0_{{mulGrp}_{R}}) = 0_{{mulGrp}_{S}})$
26	11 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
27	14 17	mgpbas	$⊢ {Base}_{S} = {Base}_{{mulGrp}_{S}}$
28	11 4	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
29	14 5	mgpplusg	$⊢ \underset{˙}{\times} = +_{{mulGrp}_{S}}$
30		eqid	$⊢ 0_{{mulGrp}_{R}} = 0_{{mulGrp}_{R}}$
31		eqid	$⊢ 0_{{mulGrp}_{S}} = 0_{{mulGrp}_{S}}$
32	26 27 28 29 30 31	ismhm	$⊢ F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}) \leftrightarrow (({mulGrp}_{R} \in Mnd \land {mulGrp}_{S} \in Mnd) \land (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y) \land F (0_{{mulGrp}_{R}}) = 0_{{mulGrp}_{S}}))$
33	13 16 25 32	syl21anbrc	$⊢ φ \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
34	10 33	jca	$⊢ φ \to (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}))$
35	11 14	isrhm	$⊢ F \in (R RingHom S) \leftrightarrow ((R \in Ring \land S \in Ring) \land (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})))$
36	6 7 34 35	syl21anbrc	$⊢ φ \to F \in (R RingHom S)$

Metamath Proof Explorer

Theorem isrhm2d

Proof