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 ) )