Theorem ablfaclem1

Description: Lemma for ablfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

	Ref	Expression
Hypotheses	ablfac.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablfac.c	⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
	ablfac.1	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablfac.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	ablfac.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	ablfac.a	⊢ 𝐴 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
	ablfac.s	⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
	ablfac.w	⊢ 𝑊 = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } )
Assertion	ablfaclem1	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ‘ 𝑈 ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) } )

Proof

Step	Hyp	Ref	Expression
1		ablfac.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablfac.c	⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3		ablfac.1	⊢ ( 𝜑 → 𝐺 ∈ Abel )
4		ablfac.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
5		ablfac.o	⊢ 𝑂 = ( od ‘ 𝐺 )
6		ablfac.a	⊢ 𝐴 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
7		ablfac.s	⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
8		ablfac.w	⊢ 𝑊 = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } )
9		eqeq2	⊢ ( 𝑔 = 𝑈 → ( ( 𝐺 DProd 𝑠 ) = 𝑔 ↔ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
10	9	anbi2d	⊢ ( 𝑔 = 𝑈 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) ) )
11	10	rabbidv	⊢ ( 𝑔 = 𝑈 → { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) } )
12		fvex	⊢ ( SubGrp ‘ 𝐺 ) ∈ V
13	2 12	rabex2	⊢ 𝐶 ∈ V
14	13	wrdexi	⊢ Word 𝐶 ∈ V
15	14	rabex	⊢ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) } ∈ V
16	11 8 15	fvmpt	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ‘ 𝑈 ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) } )