ablfaclem1

	Ref	Expression
Hypotheses	ablfac.b	$⊢ B = {Base}_{G}$
	ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
	ablfac.1	$⊢ φ \to G \in Abel$
	ablfac.2	$⊢ φ \to B \in Fin$
	ablfac.o	$⊢ O = od (G)$
	ablfac.a	$⊢ A = \{w \in ℙ \| w ∥ \|B\|\}$
	ablfac.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
	ablfac.w	$⊢ W = (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\})$
Assertion	ablfaclem1	$⊢ U \in SubGrp (G) \to W (U) = \{s \in Word C \| (G dom DProd s \land G DProd s = U)\}$

Step	Hyp	Ref	Expression
1		ablfac.b	$⊢ B = {Base}_{G}$
2		ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
3		ablfac.1	$⊢ φ \to G \in Abel$
4		ablfac.2	$⊢ φ \to B \in Fin$
5		ablfac.o	$⊢ O = od (G)$
6		ablfac.a	$⊢ A = \{w \in ℙ \| w ∥ \|B\|\}$
7		ablfac.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
8		ablfac.w	$⊢ W = (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\})$
9		eqeq2	$⊢ g = U \to (G DProd s = g \leftrightarrow G DProd s = U)$
10	9	anbi2d	$⊢ g = U \to ((G dom DProd s \land G DProd s = g) \leftrightarrow (G dom DProd s \land G DProd s = U))$
11	10	rabbidv	$⊢ g = U \to \{s \in Word C \| (G dom DProd s \land G DProd s = g)\} = \{s \in Word C \| (G dom DProd s \land G DProd s = U)\}$
12		fvex	$⊢ SubGrp (G) \in V$
13	2 12	rabex2	$⊢ C \in V$
14	13	wrdexi	$⊢ Word C \in V$
15	14	rabex	$⊢ \{s \in Word C \| (G dom DProd s \land G DProd s = U)\} \in V$
16	11 8 15	fvmpt	$⊢ U \in SubGrp (G) \to W (U) = \{s \in Word C \| (G dom DProd s \land G DProd s = U)\}$

Metamath Proof Explorer