pwsdiagrhm

Description: Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	pwsdiagrhm.y	$⊢ Y = R ↑_{𝑠} I$
	pwsdiagrhm.b	$⊢ B = {Base}_{R}$
	pwsdiagrhm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
Assertion	pwsdiagrhm	$⊢ (R \in Ring \land I \in W) \to F \in (R RingHom Y)$

Proof

Step	Hyp	Ref	Expression
1		pwsdiagrhm.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsdiagrhm.b	$⊢ B = {Base}_{R}$
3		pwsdiagrhm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
4		simpl	$⊢ (R \in Ring \land I \in W) \to R \in Ring$
5	1	pwsring	$⊢ (R \in Ring \land I \in W) \to Y \in Ring$
6		ringgrp	$⊢ R \in Ring \to R \in Grp$
7	1 2 3	pwsdiagghm	$⊢ (R \in Grp \land I \in W) \to F \in (R GrpHom Y)$
8	6 7	sylan	$⊢ (R \in Ring \land I \in W) \to F \in (R GrpHom Y)$
9		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
10	9	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
11		eqid	$⊢ {mulGrp}_{R} ↑_{𝑠} I = {mulGrp}_{R} ↑_{𝑠} I$
12	9 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
13	11 12 3	pwsdiagmhm	$⊢ ({mulGrp}_{R} \in Mnd \land I \in W) \to F \in ({mulGrp}_{R} MndHom ({mulGrp}_{R} ↑_{𝑠} I))$
14	10 13	sylan	$⊢ (R \in Ring \land I \in W) \to F \in ({mulGrp}_{R} MndHom ({mulGrp}_{R} ↑_{𝑠} I))$
15		eqidd	$⊢ (R \in Ring \land I \in W) \to {Base}_{{mulGrp}_{R}} = {Base}_{{mulGrp}_{R}}$
16		eqidd	$⊢ (R \in Ring \land I \in W) \to {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
17		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
18		eqid	$⊢ {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
19		eqid	$⊢ {Base}_{({mulGrp}_{R} ↑_{𝑠} I)} = {Base}_{({mulGrp}_{R} ↑_{𝑠} I)}$
20		eqid	$⊢ +_{{mulGrp}_{Y}} = +_{{mulGrp}_{Y}}$
21		eqid	$⊢ +_{({mulGrp}_{R} ↑_{𝑠} I)} = +_{({mulGrp}_{R} ↑_{𝑠} I)}$
22	1 9 11 17 18 19 20 21	pwsmgp	$⊢ (R \in Ring \land I \in W) \to ({Base}_{{mulGrp}_{Y}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} I)} \land +_{{mulGrp}_{Y}} = +_{({mulGrp}_{R} ↑_{𝑠} I)})$
23	22	simpld	$⊢ (R \in Ring \land I \in W) \to {Base}_{{mulGrp}_{Y}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} I)}$
24		eqidd	$⊢ ((R \in Ring \land I \in W) \land (y \in {Base}_{{mulGrp}_{R}} \land z \in {Base}_{{mulGrp}_{R}})) \to y +_{{mulGrp}_{R}} z = y +_{{mulGrp}_{R}} z$
25	22	simprd	$⊢ (R \in Ring \land I \in W) \to +_{{mulGrp}_{Y}} = +_{({mulGrp}_{R} ↑_{𝑠} I)}$
26	25	oveqdr	$⊢ ((R \in Ring \land I \in W) \land (y \in {Base}_{{mulGrp}_{Y}} \land z \in {Base}_{{mulGrp}_{Y}})) \to y +_{{mulGrp}_{Y}} z = y +_{({mulGrp}_{R} ↑_{𝑠} I)} z$
27	15 16 15 23 24 26	mhmpropd	$⊢ (R \in Ring \land I \in W) \to {mulGrp}_{R} MndHom {mulGrp}_{Y} = {mulGrp}_{R} MndHom ({mulGrp}_{R} ↑_{𝑠} I)$
28	14 27	eleqtrrd	$⊢ (R \in Ring \land I \in W) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{Y})$
29	8 28	jca	$⊢ (R \in Ring \land I \in W) \to (F \in (R GrpHom Y) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{Y}))$
30	9 17	isrhm	$⊢ F \in (R RingHom Y) \leftrightarrow ((R \in Ring \land Y \in Ring) \land (F \in (R GrpHom Y) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{Y})))$
31	4 5 29 30	syl21anbrc	$⊢ (R \in Ring \land I \in W) \to F \in (R RingHom Y)$

Metamath Proof Explorer

Theorem pwsdiagrhm

Proof