MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablfaclem3 Structured version   Visualization version   GIF version

Theorem ablfaclem3 20083
Description: Lemma for ablfac 20084. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
Hypotheses
Ref Expression
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
Ref Expression
ablfaclem3 (𝜑 → (𝑊𝐵) ≠ ∅)
Distinct variable groups:   𝑠,𝑝,𝑥,𝐴   𝑔,𝑟,𝑠,𝑆   𝑔,𝑝,𝑤,𝑥,𝐵,𝑟,𝑠   𝑂,𝑝,𝑥   𝐶,𝑔,𝑝,𝑠,𝑤,𝑥   𝑊,𝑝,𝑤,𝑥   𝜑,𝑝,𝑠,𝑤,𝑥   𝑔,𝐺,𝑝,𝑟,𝑠,𝑤,𝑥
Allowed substitution hints:   𝜑(𝑔,𝑟)   𝐴(𝑤,𝑔,𝑟)   𝐶(𝑟)   𝑆(𝑥,𝑤,𝑝)   𝑂(𝑤,𝑔,𝑠,𝑟)   𝑊(𝑔,𝑠,𝑟)

Proof of Theorem ablfaclem3
Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑞 𝑡 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 13987 . . . 4 (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
2 ablfac.a . . . . 5 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
3 prmnn 16670 . . . . . . . 8 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
433ad2ant2 1131 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
5 prmz 16671 . . . . . . . . 9 (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
6 ablfac.1 . . . . . . . . . . 11 (𝜑𝐺 ∈ Abel)
7 ablgrp 19779 . . . . . . . . . . 11 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
8 ablfac.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
98grpbn0 18956 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
106, 7, 93syl 18 . . . . . . . . . 10 (𝜑𝐵 ≠ ∅)
11 ablfac.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ Fin)
12 hashnncl 14378 . . . . . . . . . . 11 (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1311, 12syl 17 . . . . . . . . . 10 (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1410, 13mpbird 256 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ)
15 dvdsle 16307 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
165, 14, 15syl2anr 595 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
17163impia 1114 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
1814nnzd 12631 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℤ)
19183ad2ant1 1130 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
20 fznn 13617 . . . . . . . 8 ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
224, 17, 21mpbir2and 711 . . . . . 6 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
2322rabssdv 4068 . . . . 5 (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
242, 23eqsstrid 4027 . . . 4 (𝜑𝐴 ⊆ (1...(♯‘𝐵)))
251, 24ssfid 9294 . . 3 (𝜑𝐴 ∈ Fin)
26 dfin5 3954 . . . . . . . 8 (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))}
27 ablfac.o . . . . . . . . . . . . . 14 𝑂 = (od‘𝐺)
28 ablfac.s . . . . . . . . . . . . . 14 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
292ssrab3 4076 . . . . . . . . . . . . . . 15 𝐴 ⊆ ℙ
3029a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℙ)
318, 27, 28, 6, 11, 30ablfac1b 20066 . . . . . . . . . . . . 13 (𝜑𝐺dom DProd 𝑆)
328fvexi 6907 . . . . . . . . . . . . . . . 16 𝐵 ∈ V
3332rabex 5331 . . . . . . . . . . . . . . 15 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
3433, 28dmmpti 6697 . . . . . . . . . . . . . 14 dom 𝑆 = 𝐴
3534a1i 11 . . . . . . . . . . . . 13 (𝜑 → dom 𝑆 = 𝐴)
3631, 35dprdf2 20003 . . . . . . . . . . . 12 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
3736ffvelcdmda 7090 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
38 ablfac.c . . . . . . . . . . . 12 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
39 ablfac.w . . . . . . . . . . . 12 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})
408, 38, 6, 11, 27, 2, 28, 39ablfaclem1 20081 . . . . . . . . . . 11 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
4137, 40syl 17 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
42 ssrab2 4073 . . . . . . . . . 10 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ⊆ Word 𝐶
4341, 42eqsstrdi 4033 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) ⊆ Word 𝐶)
44 sseqin2 4213 . . . . . . . . 9 ((𝑊‘(𝑆𝑞)) ⊆ Word 𝐶 ↔ (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4543, 44sylib 217 . . . . . . . 8 ((𝜑𝑞𝐴) → (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4626, 45eqtr3id 2780 . . . . . . 7 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = (𝑊‘(𝑆𝑞)))
4746, 41eqtrd 2766 . . . . . 6 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
48 eqid 2726 . . . . . . . . 9 (Base‘(𝐺s (𝑆𝑞))) = (Base‘(𝐺s (𝑆𝑞)))
49 eqid 2726 . . . . . . . . 9 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
50 eqid 2726 . . . . . . . . . . 11 (𝐺s (𝑆𝑞)) = (𝐺s (𝑆𝑞))
5150subgabl 19830 . . . . . . . . . 10 ((𝐺 ∈ Abel ∧ (𝑆𝑞) ∈ (SubGrp‘𝐺)) → (𝐺s (𝑆𝑞)) ∈ Abel)
526, 37, 51syl2an2r 683 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Abel)
5330sselda 3978 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝑞 ∈ ℙ)
5450subgbas 19120 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5537, 54syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5655fveq2d 6897 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (♯‘(Base‘(𝐺s (𝑆𝑞)))))
578, 27, 28, 6, 11, 30ablfac1a 20065 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
5856, 57eqtr3d 2768 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
5958oveq2d 7432 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
6014adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑞𝐴) → (♯‘𝐵) ∈ ℕ)
6153, 60pccld 16847 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
6261nn0zd 12630 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
63 pcid 16870 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℙ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6453, 62, 63syl2anc 582 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6559, 64eqtrd 2766 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (♯‘𝐵)))
6665oveq2d 7432 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
6758, 66eqtr4d 2769 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))
6850subggrp 19119 . . . . . . . . . . . 12 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝐺s (𝑆𝑞)) ∈ Grp)
6937, 68syl 17 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Grp)
7011adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → 𝐵 ∈ Fin)
718subgss 19117 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) ⊆ 𝐵)
7237, 71syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) ⊆ 𝐵)
7370, 72ssfid 9294 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ Fin)
7455, 73eqeltrrd 2827 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (Base‘(𝐺s (𝑆𝑞))) ∈ Fin)
7548pgpfi2 19600 . . . . . . . . . . 11 (((𝐺s (𝑆𝑞)) ∈ Grp ∧ (Base‘(𝐺s (𝑆𝑞))) ∈ Fin) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
7669, 74, 75syl2anc 582 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
7753, 67, 76mpbir2and 711 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝑞 pGrp (𝐺s (𝑆𝑞)))
7848, 49, 52, 77, 74pgpfac 20080 . . . . . . . 8 ((𝜑𝑞𝐴) → ∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))))
79 ssrab2 4073 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘(𝐺s (𝑆𝑞)))
80 sswrd 14525 . . . . . . . . . . . . . 14 ({𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘(𝐺s (𝑆𝑞))) → Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word (SubGrp‘(𝐺s (𝑆𝑞))))
8179, 80ax-mp 5 . . . . . . . . . . . . 13 Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word (SubGrp‘(𝐺s (𝑆𝑞)))
8281sseli 3974 . . . . . . . . . . . 12 (𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} → 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞))))
8337adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8483adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8550subgdmdprd 20030 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
8683, 85syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
8786simprbda 497 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → 𝐺dom DProd 𝑠)
8886simplbda 498 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ran 𝑠 ⊆ 𝒫 (𝑆𝑞))
8950, 84, 87, 88subgdprd 20031 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ((𝐺s (𝑆𝑞)) DProd 𝑠) = (𝐺 DProd 𝑠))
9055ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
9190eqcomd 2732 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (Base‘(𝐺s (𝑆𝑞))) = (𝑆𝑞))
9289, 91eqeq12d 2742 . . . . . . . . . . . . . . 15 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) ↔ (𝐺 DProd 𝑠) = (𝑆𝑞)))
9392biimpd 228 . . . . . . . . . . . . . 14 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺 DProd 𝑠) = (𝑆𝑞)))
9493, 87jctild 524 . . . . . . . . . . . . 13 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
9594expimpd 452 . . . . . . . . . . . 12 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
9682, 95sylan2 591 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
97 oveq2 7424 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑦 → ((𝐺s (𝑆𝑞)) ↾s 𝑟) = ((𝐺s (𝑆𝑞)) ↾s 𝑦))
9897eleq1d 2811 . . . . . . . . . . . . . . 15 (𝑟 = 𝑦 → (((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
9998cbvrabv 3430 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )}
10050subsubg 19139 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
10137, 100syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐴) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
102101simprbda 497 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ∈ (SubGrp‘𝐺))
1031023adant3 1129 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ∈ (SubGrp‘𝐺))
104373ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
105101simplbda 498 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ⊆ (𝑆𝑞))
1061053adant3 1129 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ⊆ (𝑆𝑞))
107 ressabs 17258 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑞) ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞)) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
108104, 106, 107syl2anc 582 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
109 simp3 1135 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
110108, 109eqeltrrd 2827 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
111 oveq2 7424 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑦 → (𝐺s 𝑟) = (𝐺s 𝑦))
112111eleq1d 2811 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑦 → ((𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
113112, 38elrab2 3683 . . . . . . . . . . . . . . . 16 (𝑦𝐶 ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
114103, 110, 113sylanbrc 581 . . . . . . . . . . . . . . 15 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦𝐶)
115114rabssdv 4068 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
11699, 115eqsstrid 4027 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
117 sswrd 14525 . . . . . . . . . . . . 13 ({𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶 → Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word 𝐶)
118116, 117syl 17 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word 𝐶)
119118sselda 3978 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → 𝑠 ∈ Word 𝐶)
12096, 119jctild 524 . . . . . . . . . 10 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
121120expimpd 452 . . . . . . . . 9 ((𝜑𝑞𝐴) → ((𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ∧ ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
122121reximdv2 3154 . . . . . . . 8 ((𝜑𝑞𝐴) → (∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
12378, 122mpd 15 . . . . . . 7 ((𝜑𝑞𝐴) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))
124 rabn0 4383 . . . . . . 7 ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))
125123, 124sylibr 233 . . . . . 6 ((𝜑𝑞𝐴) → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅)
12647, 125eqnetrd 2998 . . . . 5 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅)
127 rabn0 4383 . . . . 5 ({𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅ ↔ ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
128126, 127sylib 217 . . . 4 ((𝜑𝑞𝐴) → ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
129128ralrimiva 3136 . . 3 (𝜑 → ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
130 eleq1 2814 . . . 4 (𝑦 = (𝑓𝑞) → (𝑦 ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
131130ac6sfi 9314 . . 3 ((𝐴 ∈ Fin ∧ ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))) → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
13225, 129, 131syl2anc 582 . 2 (𝜑 → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
133 sneq 4633 . . . . . . . . 9 (𝑞 = 𝑦 → {𝑞} = {𝑦})
134 fveq2 6893 . . . . . . . . . 10 (𝑞 = 𝑦 → (𝑓𝑞) = (𝑓𝑦))
135134dmeqd 5904 . . . . . . . . 9 (𝑞 = 𝑦 → dom (𝑓𝑞) = dom (𝑓𝑦))
136133, 135xpeq12d 5705 . . . . . . . 8 (𝑞 = 𝑦 → ({𝑞} × dom (𝑓𝑞)) = ({𝑦} × dom (𝑓𝑦)))
137136cbviunv 5040 . . . . . . 7 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) = 𝑦𝐴 ({𝑦} × dom (𝑓𝑦))
138 snfi 9073 . . . . . . . . . 10 {𝑦} ∈ Fin
139 simprl 769 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
140139ffvelcdmda 7090 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ Word 𝐶)
141 wrdf 14522 . . . . . . . . . . . 12 ((𝑓𝑦) ∈ Word 𝐶 → (𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶)
142 fdm 6729 . . . . . . . . . . . 12 ((𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶 → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
143140, 141, 1423syl 18 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
144 fzofi 13988 . . . . . . . . . . 11 (0..^(♯‘(𝑓𝑦))) ∈ Fin
145143, 144eqeltrdi 2834 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) ∈ Fin)
146 xpfi 9353 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ dom (𝑓𝑦) ∈ Fin) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
147138, 145, 146sylancr 585 . . . . . . . . 9 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
148147ralrimiva 3136 . . . . . . . 8 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
149 iunfi 9378 . . . . . . . 8 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
15025, 148, 149syl2an2r 683 . . . . . . 7 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
151137, 150eqeltrid 2830 . . . . . 6 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin)
152 hashcl 14368 . . . . . 6 ( 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin → (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0)
153 hashfzo0 14442 . . . . . 6 ((♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0 → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
154151, 152, 1533syl 18 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
155 fzofi 13988 . . . . . 6 (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin
156 hashen 14359 . . . . . 6 (((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin ∧ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
157155, 151, 156sylancr 585 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
158154, 157mpbid 231 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
159 bren 8976 . . . 4 ((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ↔ ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
160158, 159sylib 217 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
1616adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐺 ∈ Abel)
16211adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐵 ∈ Fin)
163 breq1 5148 . . . . . . . 8 (𝑤 = 𝑎 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑎 ∥ (♯‘𝐵)))
164163cbvrabv 3430 . . . . . . 7 {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
1652, 164eqtri 2754 . . . . . 6 𝐴 = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
166 fveq2 6893 . . . . . . . . . . 11 (𝑥 = 𝑐 → (𝑂𝑥) = (𝑂𝑐))
167166breq1d 5155 . . . . . . . . . 10 (𝑥 = 𝑐 → ((𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))))
168167cbvrabv 3430 . . . . . . . . 9 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}
169 id 22 . . . . . . . . . . . 12 (𝑝 = 𝑏𝑝 = 𝑏)
170 oveq1 7423 . . . . . . . . . . . 12 (𝑝 = 𝑏 → (𝑝 pCnt (♯‘𝐵)) = (𝑏 pCnt (♯‘𝐵)))
171169, 170oveq12d 7434 . . . . . . . . . . 11 (𝑝 = 𝑏 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑏↑(𝑏 pCnt (♯‘𝐵))))
172171breq2d 5157 . . . . . . . . . 10 (𝑝 = 𝑏 → ((𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))))
173172rabbidv 3427 . . . . . . . . 9 (𝑝 = 𝑏 → {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
174168, 173eqtrid 2778 . . . . . . . 8 (𝑝 = 𝑏 → {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
175174cbvmptv 5258 . . . . . . 7 (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
17628, 175eqtri 2754 . . . . . 6 𝑆 = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
177 breq2 5149 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐺dom DProd 𝑠𝐺dom DProd 𝑡))
178 oveq2 7424 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑡))
179178eqeq1d 2728 . . . . . . . . . 10 (𝑠 = 𝑡 → ((𝐺 DProd 𝑠) = 𝑔 ↔ (𝐺 DProd 𝑡) = 𝑔))
180177, 179anbi12d 630 . . . . . . . . 9 (𝑠 = 𝑡 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔) ↔ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)))
181180cbvrabv 3430 . . . . . . . 8 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)} = {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)}
182181mpteq2i 5250 . . . . . . 7 (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
18339, 182eqtri 2754 . . . . . 6 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
184 simprll 777 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
185 simprlr 778 . . . . . . 7 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))
186 2fveq3 6898 . . . . . . . . 9 (𝑞 = 𝑦 → (𝑊‘(𝑆𝑞)) = (𝑊‘(𝑆𝑦)))
187134, 186eleq12d 2820 . . . . . . . 8 (𝑞 = 𝑦 → ((𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦))))
188187cbvralvw 3225 . . . . . . 7 (∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
189185, 188sylib 217 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
190 simprr 771 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
1918, 38, 161, 162, 27, 165, 176, 183, 184, 189, 137, 190ablfaclem2 20082 . . . . 5 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → (𝑊𝐵) ≠ ∅)
192191expr 455 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (:(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
193192exlimdv 1929 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
194160, 193mpd 15 . 2 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (𝑊𝐵) ≠ ∅)
195132, 194exlimddv 1931 1 (𝜑 → (𝑊𝐵) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wex 1774  wcel 2099  wne 2930  wral 3051  wrex 3060  {crab 3419  cin 3945  wss 3946  c0 4322  𝒫 cpw 4597  {csn 4623   ciun 4993   class class class wbr 5145  cmpt 5228   × cxp 5672  dom cdm 5674  ran crn 5675  wf 6542  1-1-ontowf1o 6545  cfv 6546  (class class class)co 7416  cen 8963  Fincfn 8966  0cc0 11149  1c1 11150  cle 11290  cn 12258  0cn0 12518  cz 12604  ...cfz 13532  ..^cfzo 13675  cexp 14075  chash 14342  Word cword 14517  cdvds 16251  cprime 16667   pCnt cpc 16833  Basecbs 17208  s cress 17237  Grpcgrp 18923  SubGrpcsubg 19110  odcod 19518   pGrp cpgp 19520  Abelcabl 19775  CycGrpccyg 19871   DProd cdprd 19989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-disj 5111  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-rpss 7726  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-tpos 8233  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-oadd 8492  df-omul 8493  df-er 8726  df-ec 8728  df-qs 8732  df-map 8849  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-sup 9478  df-inf 9479  df-oi 9546  df-dju 9937  df-card 9975  df-acn 9978  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-n0 12519  df-xnn0 12591  df-z 12605  df-uz 12869  df-q 12979  df-rp 13023  df-fz 13533  df-fzo 13676  df-fl 13806  df-mod 13884  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-word 14518  df-concat 14574  df-s1 14599  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485  df-sum 15686  df-dvds 16252  df-gcd 16490  df-prm 16668  df-pc 16834  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-0g 17451  df-gsum 17452  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-mhm 18768  df-submnd 18769  df-grp 18926  df-minusg 18927  df-sbg 18928  df-mulg 19058  df-subg 19113  df-eqg 19115  df-ghm 19203  df-gim 19249  df-ga 19280  df-cntz 19307  df-oppg 19336  df-od 19522  df-gex 19523  df-pgp 19524  df-lsm 19630  df-pj1 19631  df-cmn 19776  df-abl 19777  df-cyg 19872  df-dprd 19991
This theorem is referenced by:  ablfac  20084
  Copyright terms: Public domain W3C validator