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 ^s I )
pwsdiagrhm.b 
|- B = ( Base ` R )
pwsdiagrhm.f 
|- F = ( x e. B |-> ( I X. { x } ) )
Assertion pwsdiagrhm 
|- ( ( R e. Ring /\ I e. W ) -> F e. ( R RingHom Y ) )

Proof

Step Hyp Ref Expression
1 pwsdiagrhm.y 
 |-  Y = ( R ^s I )
2 pwsdiagrhm.b 
 |-  B = ( Base ` R )
3 pwsdiagrhm.f 
 |-  F = ( x e. B |-> ( I X. { x } ) )
4 simpl 
 |-  ( ( R e. Ring /\ I e. W ) -> R e. Ring )
5 1 pwsring 
 |-  ( ( R e. Ring /\ I e. W ) -> Y e. Ring )
6 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
7 1 2 3 pwsdiagghm 
 |-  ( ( R e. Grp /\ I e. W ) -> F e. ( R GrpHom Y ) )
8 6 7 sylan 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. ( R GrpHom Y ) )
9 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
10 9 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
11 eqid 
 |-  ( ( mulGrp ` R ) ^s I ) = ( ( mulGrp ` R ) ^s I )
12 9 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
13 11 12 3 pwsdiagmhm 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ I e. W ) -> F e. ( ( mulGrp ` R ) MndHom ( ( mulGrp ` R ) ^s I ) ) )
14 10 13 sylan 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. ( ( mulGrp ` R ) MndHom ( ( mulGrp ` R ) ^s I ) ) )
15 eqidd 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) ) )
16 eqidd 
 |-  ( ( R e. Ring /\ I e. W ) -> ( 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 ) ^s I ) ) = ( Base ` ( ( mulGrp ` R ) ^s I ) )
20 eqid 
 |-  ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( mulGrp ` Y ) )
21 eqid 
 |-  ( +g ` ( ( mulGrp ` R ) ^s I ) ) = ( +g ` ( ( mulGrp ` R ) ^s I ) )
22 1 9 11 17 18 19 20 21 pwsmgp 
 |-  ( ( R e. Ring /\ I e. W ) -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s I ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s I ) ) ) )
23 22 simpld 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s I ) ) )
24 eqidd 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ ( y e. ( Base ` ( mulGrp ` R ) ) /\ z e. ( Base ` ( mulGrp ` R ) ) ) ) -> ( y ( +g ` ( mulGrp ` R ) ) z ) = ( y ( +g ` ( mulGrp ` R ) ) z ) )
25 22 simprd 
 |-  ( ( R e. Ring /\ I e. W ) -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s I ) ) )
26 25 oveqdr 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ ( y e. ( Base ` ( mulGrp ` Y ) ) /\ z e. ( Base ` ( mulGrp ` Y ) ) ) ) -> ( y ( +g ` ( mulGrp ` Y ) ) z ) = ( y ( +g ` ( ( mulGrp ` R ) ^s I ) ) z ) )
27 15 16 15 23 24 26 mhmpropd 
 |-  ( ( R e. Ring /\ I e. W ) -> ( ( mulGrp ` R ) MndHom ( mulGrp ` Y ) ) = ( ( mulGrp ` R ) MndHom ( ( mulGrp ` R ) ^s I ) ) )
28 14 27 eleqtrrd 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` Y ) ) )
29 8 28 jca 
 |-  ( ( R e. Ring /\ I e. W ) -> ( F e. ( R GrpHom Y ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` Y ) ) ) )
30 9 17 isrhm 
 |-  ( F e. ( R RingHom Y ) <-> ( ( R e. Ring /\ Y e. Ring ) /\ ( F e. ( R GrpHom Y ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` Y ) ) ) ) )
31 4 5 29 30 syl21anbrc 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. ( R RingHom Y ) )