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

Theorem ablfaclem3 19209
Description: Lemma for ablfac 19210. (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 13345 . . . 4 (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
2 ablfac.a . . . . 5 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
3 prmnn 16016 . . . . . . . 8 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
433ad2ant2 1131 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
5 prmz 16017 . . . . . . . . 9 (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
6 ablfac.1 . . . . . . . . . . 11 (𝜑𝐺 ∈ Abel)
7 ablgrp 18911 . . . . . . . . . . 11 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
8 ablfac.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
98grpbn0 18132 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
106, 7, 93syl 18 . . . . . . . . . 10 (𝜑𝐵 ≠ ∅)
11 ablfac.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ Fin)
12 hashnncl 13732 . . . . . . . . . . 11 (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1311, 12syl 17 . . . . . . . . . 10 (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1410, 13mpbird 260 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ)
15 dvdsle 15660 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
165, 14, 15syl2anr 599 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
17163impia 1114 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
1814nnzd 12083 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℤ)
19183ad2ant1 1130 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
20 fznn 12979 . . . . . . . 8 ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
224, 17, 21mpbir2and 712 . . . . . 6 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
2322rabssdv 4037 . . . . 5 (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
242, 23eqsstrid 4001 . . . 4 (𝜑𝐴 ⊆ (1...(♯‘𝐵)))
251, 24ssfid 8738 . . 3 (𝜑𝐴 ∈ Fin)
26 dfin5 3927 . . . . . . . 8 (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))}
27 ablfac.o . . . . . . . . . . . . . 14 𝑂 = (od‘𝐺)
28 ablfac.s . . . . . . . . . . . . . 14 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
292ssrab3 4043 . . . . . . . . . . . . . . 15 𝐴 ⊆ ℙ
3029a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℙ)
318, 27, 28, 6, 11, 30ablfac1b 19192 . . . . . . . . . . . . 13 (𝜑𝐺dom DProd 𝑆)
328fvexi 6675 . . . . . . . . . . . . . . . 16 𝐵 ∈ V
3332rabex 5221 . . . . . . . . . . . . . . 15 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
3433, 28dmmpti 6481 . . . . . . . . . . . . . 14 dom 𝑆 = 𝐴
3534a1i 11 . . . . . . . . . . . . 13 (𝜑 → dom 𝑆 = 𝐴)
3631, 35dprdf2 19129 . . . . . . . . . . . 12 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
3736ffvelrnda 6842 . . . . . . . . . . 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 19207 . . . . . . . . . . 11 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
4137, 40syl 17 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
42 ssrab2 4042 . . . . . . . . . 10 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ⊆ Word 𝐶
4341, 42eqsstrdi 4007 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) ⊆ Word 𝐶)
44 sseqin2 4177 . . . . . . . . 9 ((𝑊‘(𝑆𝑞)) ⊆ Word 𝐶 ↔ (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4543, 44sylib 221 . . . . . . . 8 ((𝜑𝑞𝐴) → (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4626, 45syl5eqr 2873 . . . . . . 7 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = (𝑊‘(𝑆𝑞)))
4746, 41eqtrd 2859 . . . . . 6 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
48 eqid 2824 . . . . . . . . 9 (Base‘(𝐺s (𝑆𝑞))) = (Base‘(𝐺s (𝑆𝑞)))
49 eqid 2824 . . . . . . . . 9 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
50 eqid 2824 . . . . . . . . . . 11 (𝐺s (𝑆𝑞)) = (𝐺s (𝑆𝑞))
5150subgabl 18956 . . . . . . . . . 10 ((𝐺 ∈ Abel ∧ (𝑆𝑞) ∈ (SubGrp‘𝐺)) → (𝐺s (𝑆𝑞)) ∈ Abel)
526, 37, 51syl2an2r 684 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Abel)
5330sselda 3953 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝑞 ∈ ℙ)
5450subgbas 18283 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5537, 54syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5655fveq2d 6665 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (♯‘(Base‘(𝐺s (𝑆𝑞)))))
578, 27, 28, 6, 11, 30ablfac1a 19191 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
5856, 57eqtr3d 2861 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
5958oveq2d 7165 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
6014adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑞𝐴) → (♯‘𝐵) ∈ ℕ)
6153, 60pccld 16185 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
6261nn0zd 12082 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
63 pcid 16207 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℙ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6453, 62, 63syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6559, 64eqtrd 2859 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (♯‘𝐵)))
6665oveq2d 7165 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
6758, 66eqtr4d 2862 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))
6850subggrp 18282 . . . . . . . . . . . 12 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝐺s (𝑆𝑞)) ∈ Grp)
6937, 68syl 17 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Grp)
7011adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → 𝐵 ∈ Fin)
718subgss 18280 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) ⊆ 𝐵)
7237, 71syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) ⊆ 𝐵)
7370, 72ssfid 8738 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ Fin)
7455, 73eqeltrrd 2917 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (Base‘(𝐺s (𝑆𝑞))) ∈ Fin)
7548pgpfi2 18731 . . . . . . . . . . 11 (((𝐺s (𝑆𝑞)) ∈ Grp ∧ (Base‘(𝐺s (𝑆𝑞))) ∈ Fin) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
7669, 74, 75syl2anc 587 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
7753, 67, 76mpbir2and 712 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝑞 pGrp (𝐺s (𝑆𝑞)))
7848, 49, 52, 77, 74pgpfac 19206 . . . . . . . 8 ((𝜑𝑞𝐴) → ∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))))
79 ssrab2 4042 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘(𝐺s (𝑆𝑞)))
80 sswrd 13874 . . . . . . . . . . . . . 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 3949 . . . . . . . . . . . 12 (𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} → 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞))))
8337adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8483adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8550subgdmdprd 19156 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
8683, 85syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
8786simprbda 502 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → 𝐺dom DProd 𝑠)
8886simplbda 503 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ran 𝑠 ⊆ 𝒫 (𝑆𝑞))
8950, 84, 87, 88subgdprd 19157 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ((𝐺s (𝑆𝑞)) DProd 𝑠) = (𝐺 DProd 𝑠))
9055ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
9190eqcomd 2830 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (Base‘(𝐺s (𝑆𝑞))) = (𝑆𝑞))
9289, 91eqeq12d 2840 . . . . . . . . . . . . . . 15 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) ↔ (𝐺 DProd 𝑠) = (𝑆𝑞)))
9392biimpd 232 . . . . . . . . . . . . . 14 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺 DProd 𝑠) = (𝑆𝑞)))
9493, 87jctild 529 . . . . . . . . . . . . 13 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
9594expimpd 457 . . . . . . . . . . . 12 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
9682, 95sylan2 595 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
97 oveq2 7157 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑦 → ((𝐺s (𝑆𝑞)) ↾s 𝑟) = ((𝐺s (𝑆𝑞)) ↾s 𝑦))
9897eleq1d 2900 . . . . . . . . . . . . . . 15 (𝑟 = 𝑦 → (((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
9998cbvrabv 3477 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )}
10050subsubg 18302 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
10137, 100syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐴) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
102101simprbda 502 . . . . . . . . . . . . . . . . 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 503 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ⊆ (𝑆𝑞))
1061053adant3 1129 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ⊆ (𝑆𝑞))
107 ressabs 16563 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑞) ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞)) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
108104, 106, 107syl2anc 587 . . . . . . . . . . . . . . . . 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 2917 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
111 oveq2 7157 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑦 → (𝐺s 𝑟) = (𝐺s 𝑦))
112111eleq1d 2900 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑦 → ((𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
113112, 38elrab2 3669 . . . . . . . . . . . . . . . 16 (𝑦𝐶 ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
114103, 110, 113sylanbrc 586 . . . . . . . . . . . . . . 15 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦𝐶)
115114rabssdv 4037 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
11699, 115eqsstrid 4001 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
117 sswrd 13874 . . . . . . . . . . . . 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 3953 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → 𝑠 ∈ Word 𝐶)
12096, 119jctild 529 . . . . . . . . . 10 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
121120expimpd 457 . . . . . . . . 9 ((𝜑𝑞𝐴) → ((𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ∧ ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
122121reximdv2 3263 . . . . . . . 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 4322 . . . . . . 7 ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))
125123, 124sylibr 237 . . . . . 6 ((𝜑𝑞𝐴) → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅)
12647, 125eqnetrd 3081 . . . . 5 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅)
127 rabn0 4322 . . . . 5 ({𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅ ↔ ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
128126, 127sylib 221 . . . 4 ((𝜑𝑞𝐴) → ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
129128ralrimiva 3177 . . 3 (𝜑 → ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
130 eleq1 2903 . . . 4 (𝑦 = (𝑓𝑞) → (𝑦 ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
131130ac6sfi 8759 . . 3 ((𝐴 ∈ Fin ∧ ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))) → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
13225, 129, 131syl2anc 587 . 2 (𝜑 → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
133 sneq 4560 . . . . . . . . 9 (𝑞 = 𝑦 → {𝑞} = {𝑦})
134 fveq2 6661 . . . . . . . . . 10 (𝑞 = 𝑦 → (𝑓𝑞) = (𝑓𝑦))
135134dmeqd 5761 . . . . . . . . 9 (𝑞 = 𝑦 → dom (𝑓𝑞) = dom (𝑓𝑦))
136133, 135xpeq12d 5573 . . . . . . . 8 (𝑞 = 𝑦 → ({𝑞} × dom (𝑓𝑞)) = ({𝑦} × dom (𝑓𝑦)))
137136cbviunv 4951 . . . . . . 7 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) = 𝑦𝐴 ({𝑦} × dom (𝑓𝑦))
138 snfi 8590 . . . . . . . . . 10 {𝑦} ∈ Fin
139 simprl 770 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
140139ffvelrnda 6842 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ Word 𝐶)
141 wrdf 13871 . . . . . . . . . . . 12 ((𝑓𝑦) ∈ Word 𝐶 → (𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶)
142 fdm 6511 . . . . . . . . . . . 12 ((𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶 → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
143140, 141, 1423syl 18 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
144 fzofi 13346 . . . . . . . . . . 11 (0..^(♯‘(𝑓𝑦))) ∈ Fin
145143, 144eqeltrdi 2924 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) ∈ Fin)
146 xpfi 8786 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ dom (𝑓𝑦) ∈ Fin) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
147138, 145, 146sylancr 590 . . . . . . . . 9 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
148147ralrimiva 3177 . . . . . . . 8 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
149 iunfi 8809 . . . . . . . 8 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
15025, 148, 149syl2an2r 684 . . . . . . 7 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
151137, 150eqeltrid 2920 . . . . . 6 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin)
152 hashcl 13722 . . . . . 6 ( 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin → (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0)
153 hashfzo0 13796 . . . . . 6 ((♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0 → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
154151, 152, 1533syl 18 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
155 fzofi 13346 . . . . . 6 (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin
156 hashen 13712 . . . . . 6 (((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin ∧ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
157155, 151, 156sylancr 590 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
158154, 157mpbid 235 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
159 bren 8514 . . . 4 ((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ↔ ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
160158, 159sylib 221 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
1616adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐺 ∈ Abel)
16211adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐵 ∈ Fin)
163 breq1 5055 . . . . . . . 8 (𝑤 = 𝑎 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑎 ∥ (♯‘𝐵)))
164163cbvrabv 3477 . . . . . . 7 {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
1652, 164eqtri 2847 . . . . . 6 𝐴 = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
166 fveq2 6661 . . . . . . . . . . 11 (𝑥 = 𝑐 → (𝑂𝑥) = (𝑂𝑐))
167166breq1d 5062 . . . . . . . . . 10 (𝑥 = 𝑐 → ((𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))))
168167cbvrabv 3477 . . . . . . . . 9 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}
169 id 22 . . . . . . . . . . . 12 (𝑝 = 𝑏𝑝 = 𝑏)
170 oveq1 7156 . . . . . . . . . . . 12 (𝑝 = 𝑏 → (𝑝 pCnt (♯‘𝐵)) = (𝑏 pCnt (♯‘𝐵)))
171169, 170oveq12d 7167 . . . . . . . . . . 11 (𝑝 = 𝑏 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑏↑(𝑏 pCnt (♯‘𝐵))))
172171breq2d 5064 . . . . . . . . . 10 (𝑝 = 𝑏 → ((𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))))
173172rabbidv 3465 . . . . . . . . 9 (𝑝 = 𝑏 → {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
174168, 173syl5eq 2871 . . . . . . . 8 (𝑝 = 𝑏 → {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
175174cbvmptv 5155 . . . . . . 7 (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
17628, 175eqtri 2847 . . . . . 6 𝑆 = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
177 breq2 5056 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐺dom DProd 𝑠𝐺dom DProd 𝑡))
178 oveq2 7157 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑡))
179178eqeq1d 2826 . . . . . . . . . 10 (𝑠 = 𝑡 → ((𝐺 DProd 𝑠) = 𝑔 ↔ (𝐺 DProd 𝑡) = 𝑔))
180177, 179anbi12d 633 . . . . . . . . 9 (𝑠 = 𝑡 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔) ↔ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)))
181180cbvrabv 3477 . . . . . . . 8 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)} = {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)}
182181mpteq2i 5144 . . . . . . 7 (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
18339, 182eqtri 2847 . . . . . 6 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
184 simprll 778 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
185 simprlr 779 . . . . . . 7 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))
186 2fveq3 6666 . . . . . . . . 9 (𝑞 = 𝑦 → (𝑊‘(𝑆𝑞)) = (𝑊‘(𝑆𝑦)))
187134, 186eleq12d 2910 . . . . . . . 8 (𝑞 = 𝑦 → ((𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦))))
188187cbvralvw 3434 . . . . . . 7 (∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
189185, 188sylib 221 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
190 simprr 772 . . . . . 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 19208 . . . . 5 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → (𝑊𝐵) ≠ ∅)
192191expr 460 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (:(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
193192exlimdv 1935 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
194160, 193mpd 15 . 2 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (𝑊𝐵) ≠ ∅)
195132, 194exlimddv 1937 1 (𝜑 → (𝑊𝐵) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2115  wne 3014  wral 3133  wrex 3134  {crab 3137  cin 3918  wss 3919  c0 4276  𝒫 cpw 4522  {csn 4550   ciun 4905   class class class wbr 5052  cmpt 5132   × cxp 5540  dom cdm 5542  ran crn 5543  wf 6339  1-1-ontowf1o 6342  cfv 6343  (class class class)co 7149  cen 8502  Fincfn 8505  0cc0 10535  1c1 10536  cle 10674  cn 11634  0cn0 11894  cz 11978  ...cfz 12894  ..^cfzo 13037  cexp 13434  chash 13695  Word cword 13866  cdvds 15607  cprime 16013   pCnt cpc 16171  Basecbs 16483  s cress 16484  Grpcgrp 18103  SubGrpcsubg 18273  odcod 18652   pGrp cpgp 18654  Abelcabl 18907  CycGrpccyg 18996   DProd cdprd 19115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-rpss 7443  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-tpos 7888  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8285  df-ec 8287  df-qs 8291  df-map 8404  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-acn 9368  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-n0 11895  df-xnn0 11965  df-z 11979  df-uz 12241  df-q 12346  df-rp 12387  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-fac 13639  df-bc 13668  df-hash 13696  df-word 13867  df-concat 13923  df-s1 13950  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-sum 15043  df-dvds 15608  df-gcd 15842  df-prm 16014  df-pc 16172  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-0g 16715  df-gsum 16716  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-grp 18106  df-minusg 18107  df-sbg 18108  df-mulg 18225  df-subg 18276  df-eqg 18278  df-ghm 18356  df-gim 18399  df-ga 18420  df-cntz 18447  df-oppg 18474  df-od 18656  df-gex 18657  df-pgp 18658  df-lsm 18761  df-pj1 18762  df-cmn 18908  df-abl 18909  df-cyg 18997  df-dprd 19117
This theorem is referenced by:  ablfac  19210
  Copyright terms: Public domain W3C validator