This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwsdiagghm

Description: Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwsdiagghm.y 
|- Y = ( R ^s I )
pwsdiagghm.b 
|- B = ( Base ` R )
pwsdiagghm.f 
|- F = ( x e. B |-> ( I X. { x } ) )
Assertion pwsdiagghm 
|- ( ( R e. Grp /\ I e. W ) -> F e. ( R GrpHom Y ) )

Proof

Step Hyp Ref Expression
1 pwsdiagghm.y 
 |-  Y = ( R ^s I )
2 pwsdiagghm.b 
 |-  B = ( Base ` R )
3 pwsdiagghm.f 
 |-  F = ( x e. B |-> ( I X. { x } ) )
4 grpmnd 
 |-  ( R e. Grp -> R e. Mnd )
5 1 2 3 pwsdiagmhm 
 |-  ( ( R e. Mnd /\ I e. W ) -> F e. ( R MndHom Y ) )
6 4 5 sylan 
 |-  ( ( R e. Grp /\ I e. W ) -> F e. ( R MndHom Y ) )
7 1 pwsgrp 
 |-  ( ( R e. Grp /\ I e. W ) -> Y e. Grp )
8 ghmmhmb 
 |-  ( ( R e. Grp /\ Y e. Grp ) -> ( R GrpHom Y ) = ( R MndHom Y ) )
9 7 8 syldan 
 |-  ( ( R e. Grp /\ I e. W ) -> ( R GrpHom Y ) = ( R MndHom Y ) )
10 6 9 eleqtrrd 
 |-  ( ( R e. Grp /\ I e. W ) -> F e. ( R GrpHom Y ) )