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 ⊢ B = Base G
ablfac.c ⊢ C = r ∈ SubGrp ⁡ G | G ↾ 𝑠 r ∈ CycGrp ∩ ran ⁡ pGrp
ablfac.1 ⊢ φ → G ∈ Abel
ablfac.2 ⊢ φ → B ∈ Fin
ablfac.o ⊢ O = od ⁡ G
ablfac.a ⊢ A = w ∈ ℙ | w ∥ B
ablfac.s ⊢ S = p ∈ A ⟼ x ∈ B | O ⁡ x ∥ p p pCnt B
ablfac.w ⊢ W = g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g
Assertion ablfaclem1 ⊢ U ∈ SubGrp ⁡ G → W ⁡ U = s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = U

Proof

Step Hyp Ref Expression
1 ablfac.b ⊢ B = Base G
2 ablfac.c ⊢ C = r ∈ SubGrp ⁡ G | G ↾ 𝑠 r ∈ CycGrp ∩ ran ⁡ pGrp
3 ablfac.1 ⊢ φ → G ∈ Abel
4 ablfac.2 ⊢ φ → B ∈ Fin
5 ablfac.o ⊢ O = od ⁡ G
6 ablfac.a ⊢ A = w ∈ ℙ | w ∥ B
7 ablfac.s ⊢ S = p ∈ A ⟼ x ∈ B | O ⁡ x ∥ p p pCnt B
8 ablfac.w ⊢ W = g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g
9 eqeq2 ⊢ g = U → G DProd s = g ↔ G DProd s = U
10 9 anbi2d ⊢ g = U → G dom ⁡ DProd s ∧ G DProd s = g ↔ G dom ⁡ DProd s ∧ G DProd s = U
11 10 rabbidv ⊢ g = U → s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g = s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = U
12 fvex ⊢ SubGrp ⁡ G ∈ V
13 2 12 rabex2 ⊢ C ∈ V
14 13 wrdexi ⊢ Word C ∈ V
15 14 rabex ⊢ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = U ∈ V
16 11 8 15 fvmpt ⊢ U ∈ SubGrp ⁡ G → W ⁡ U = s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = U