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

Metamath Proof Explorer

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 𝑠 ) = 𝑈 ) } )