pwsdiagghm

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

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

Step	Hyp	Ref	Expression
1		pwsdiagghm.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsdiagghm.b	$⊢ B = {Base}_{R}$
3		pwsdiagghm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
4		grpmnd	$⊢ R \in Grp \to R \in Mnd$
5	1 2 3	pwsdiagmhm	$⊢ (R \in Mnd \land I \in W) \to F \in (R MndHom Y)$
6	4 5	sylan	$⊢ (R \in Grp \land I \in W) \to F \in (R MndHom Y)$
7	1	pwsgrp	$⊢ (R \in Grp \land I \in W) \to Y \in Grp$
8		ghmmhmb	$⊢ (R \in Grp \land Y \in Grp) \to R GrpHom Y = R MndHom Y$
9	7 8	syldan	$⊢ (R \in Grp \land I \in W) \to R GrpHom Y = R MndHom Y$
10	6 9	eleqtrrd	$⊢ (R \in Grp \land I \in W) \to F \in (R GrpHom Y)$

Metamath Proof Explorer