# Metamath Proof Explorer

## Theorem 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}={\mathrm{Base}}_{{R}}$
pwsdiagrhm.f ${⊢}{F}=\left({x}\in {B}⟼{I}×\left\{{x}\right\}\right)$
Assertion pwsdiagrhm ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {F}\in \left({R}\mathrm{RingHom}{Y}\right)$

### Proof

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