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

Theorem ablfaclem3 18962
Description: Lemma for ablfac 18963. (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 13159 . . . 4 (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
2 ablfac.a . . . . 5 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
3 prmnn 15877 . . . . . . . 8 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
433ad2ant2 1114 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
5 prmz 15878 . . . . . . . . 9 (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
6 ablfac.1 . . . . . . . . . . 11 (𝜑𝐺 ∈ Abel)
7 ablgrp 18674 . . . . . . . . . . 11 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
8 ablfac.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
98grpbn0 17923 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
106, 7, 93syl 18 . . . . . . . . . 10 (𝜑𝐵 ≠ ∅)
11 ablfac.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ Fin)
12 hashnncl 13545 . . . . . . . . . . 11 (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1311, 12syl 17 . . . . . . . . . 10 (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1410, 13mpbird 249 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ)
15 dvdsle 15523 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
165, 14, 15syl2anr 587 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
17163impia 1097 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
1814nnzd 11902 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℤ)
19183ad2ant1 1113 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
20 fznn 12794 . . . . . . . 8 ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
224, 17, 21mpbir2and 700 . . . . . 6 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
2322rabssdv 3943 . . . . 5 (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
242, 23syl5eqss 3907 . . . 4 (𝜑𝐴 ⊆ (1...(♯‘𝐵)))
251, 24ssfid 8538 . . 3 (𝜑𝐴 ∈ Fin)
26 dfin5 3839 . . . . . . . 8 (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))}
27 ablfac.o . . . . . . . . . . . . . 14 𝑂 = (od‘𝐺)
28 ablfac.s . . . . . . . . . . . . . 14 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
292ssrab3 3949 . . . . . . . . . . . . . . 15 𝐴 ⊆ ℙ
3029a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℙ)
318, 27, 28, 6, 11, 30ablfac1b 18945 . . . . . . . . . . . . 13 (𝜑𝐺dom DProd 𝑆)
328fvexi 6515 . . . . . . . . . . . . . . . 16 𝐵 ∈ V
3332rabex 5092 . . . . . . . . . . . . . . 15 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
3433, 28dmmpti 6324 . . . . . . . . . . . . . 14 dom 𝑆 = 𝐴
3534a1i 11 . . . . . . . . . . . . 13 (𝜑 → dom 𝑆 = 𝐴)
3631, 35dprdf2 18882 . . . . . . . . . . . 12 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
3736ffvelrnda 6678 . . . . . . . . . . 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 18960 . . . . . . . . . . 11 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
4137, 40syl 17 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
42 ssrab2 3948 . . . . . . . . . 10 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ⊆ Word 𝐶
4341, 42syl6eqss 3913 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) ⊆ Word 𝐶)
44 sseqin2 4081 . . . . . . . . 9 ((𝑊‘(𝑆𝑞)) ⊆ Word 𝐶 ↔ (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4543, 44sylib 210 . . . . . . . 8 ((𝜑𝑞𝐴) → (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4626, 45syl5eqr 2828 . . . . . . 7 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = (𝑊‘(𝑆𝑞)))
4746, 41eqtrd 2814 . . . . . 6 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
48 eqid 2778 . . . . . . . . 9 (Base‘(𝐺s (𝑆𝑞))) = (Base‘(𝐺s (𝑆𝑞)))
49 eqid 2778 . . . . . . . . 9 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
50 eqid 2778 . . . . . . . . . . 11 (𝐺s (𝑆𝑞)) = (𝐺s (𝑆𝑞))
5150subgabl 18717 . . . . . . . . . 10 ((𝐺 ∈ Abel ∧ (𝑆𝑞) ∈ (SubGrp‘𝐺)) → (𝐺s (𝑆𝑞)) ∈ Abel)
526, 37, 51syl2an2r 672 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Abel)
5330sselda 3860 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝑞 ∈ ℙ)
5450subgbas 18070 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5537, 54syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5655fveq2d 6505 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (♯‘(Base‘(𝐺s (𝑆𝑞)))))
578, 27, 28, 6, 11, 30ablfac1a 18944 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
5856, 57eqtr3d 2816 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
5958oveq2d 6994 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
6014adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑞𝐴) → (♯‘𝐵) ∈ ℕ)
6153, 60pccld 16046 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
6261nn0zd 11901 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
63 pcid 16068 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℙ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6453, 62, 63syl2anc 576 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6559, 64eqtrd 2814 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (♯‘𝐵)))
6665oveq2d 6994 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
6758, 66eqtr4d 2817 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))
6850subggrp 18069 . . . . . . . . . . . 12 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝐺s (𝑆𝑞)) ∈ Grp)
6937, 68syl 17 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Grp)
7011adantr 473 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → 𝐵 ∈ Fin)
718subgss 18067 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) ⊆ 𝐵)
7237, 71syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) ⊆ 𝐵)
7370, 72ssfid 8538 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ Fin)
7455, 73eqeltrrd 2867 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (Base‘(𝐺s (𝑆𝑞))) ∈ Fin)
7548pgpfi2 18495 . . . . . . . . . . 11 (((𝐺s (𝑆𝑞)) ∈ Grp ∧ (Base‘(𝐺s (𝑆𝑞))) ∈ Fin) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
7669, 74, 75syl2anc 576 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
7753, 67, 76mpbir2and 700 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝑞 pGrp (𝐺s (𝑆𝑞)))
7848, 49, 52, 77, 74pgpfac 18959 . . . . . . . 8 ((𝜑𝑞𝐴) → ∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))))
79 ssrab2 3948 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘(𝐺s (𝑆𝑞)))
80 sswrd 13683 . . . . . . . . . . . . . 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 3856 . . . . . . . . . . . 12 (𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} → 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞))))
8337adantr 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8483adantr 473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8550subgdmdprd 18909 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
8683, 85syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
8786simprbda 491 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → 𝐺dom DProd 𝑠)
8886simplbda 492 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ran 𝑠 ⊆ 𝒫 (𝑆𝑞))
8950, 84, 87, 88subgdprd 18910 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ((𝐺s (𝑆𝑞)) DProd 𝑠) = (𝐺 DProd 𝑠))
9055ad2antrr 713 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
9190eqcomd 2784 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (Base‘(𝐺s (𝑆𝑞))) = (𝑆𝑞))
9289, 91eqeq12d 2793 . . . . . . . . . . . . . . 15 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) ↔ (𝐺 DProd 𝑠) = (𝑆𝑞)))
9392biimpd 221 . . . . . . . . . . . . . 14 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺 DProd 𝑠) = (𝑆𝑞)))
9493, 87jctild 518 . . . . . . . . . . . . 13 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
9594expimpd 446 . . . . . . . . . . . 12 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
9682, 95sylan2 583 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
97 oveq2 6986 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑦 → ((𝐺s (𝑆𝑞)) ↾s 𝑟) = ((𝐺s (𝑆𝑞)) ↾s 𝑦))
9897eleq1d 2850 . . . . . . . . . . . . . . 15 (𝑟 = 𝑦 → (((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
9998cbvrabv 3412 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )}
10050subsubg 18089 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
10137, 100syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐴) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
102101simprbda 491 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ∈ (SubGrp‘𝐺))
1031023adant3 1112 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ∈ (SubGrp‘𝐺))
104373ad2ant1 1113 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
105101simplbda 492 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ⊆ (𝑆𝑞))
1061053adant3 1112 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ⊆ (𝑆𝑞))
107 ressabs 16422 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑞) ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞)) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
108104, 106, 107syl2anc 576 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
109 simp3 1118 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
110108, 109eqeltrrd 2867 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
111 oveq2 6986 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑦 → (𝐺s 𝑟) = (𝐺s 𝑦))
112111eleq1d 2850 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑦 → ((𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
113112, 38elrab2 3599 . . . . . . . . . . . . . . . 16 (𝑦𝐶 ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
114103, 110, 113sylanbrc 575 . . . . . . . . . . . . . . 15 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦𝐶)
115114rabssdv 3943 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
11699, 115syl5eqss 3907 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
117 sswrd 13683 . . . . . . . . . . . . 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 3860 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → 𝑠 ∈ Word 𝐶)
12096, 119jctild 518 . . . . . . . . . 10 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
121120expimpd 446 . . . . . . . . 9 ((𝜑𝑞𝐴) → ((𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ∧ ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
122121reximdv2 3216 . . . . . . . 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 4227 . . . . . . 7 ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))
125123, 124sylibr 226 . . . . . 6 ((𝜑𝑞𝐴) → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅)
12647, 125eqnetrd 3034 . . . . 5 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅)
127 rabn0 4227 . . . . 5 ({𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅ ↔ ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
128126, 127sylib 210 . . . 4 ((𝜑𝑞𝐴) → ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
129128ralrimiva 3132 . . 3 (𝜑 → ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
130 eleq1 2853 . . . 4 (𝑦 = (𝑓𝑞) → (𝑦 ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
131130ac6sfi 8559 . . 3 ((𝐴 ∈ Fin ∧ ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))) → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
13225, 129, 131syl2anc 576 . 2 (𝜑 → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
133 sneq 4452 . . . . . . . . 9 (𝑞 = 𝑦 → {𝑞} = {𝑦})
134 fveq2 6501 . . . . . . . . . 10 (𝑞 = 𝑦 → (𝑓𝑞) = (𝑓𝑦))
135134dmeqd 5625 . . . . . . . . 9 (𝑞 = 𝑦 → dom (𝑓𝑞) = dom (𝑓𝑦))
136133, 135xpeq12d 5439 . . . . . . . 8 (𝑞 = 𝑦 → ({𝑞} × dom (𝑓𝑞)) = ({𝑦} × dom (𝑓𝑦)))
137136cbviunv 4834 . . . . . . 7 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) = 𝑦𝐴 ({𝑦} × dom (𝑓𝑦))
138 snfi 8393 . . . . . . . . . 10 {𝑦} ∈ Fin
139 simprl 758 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
140139ffvelrnda 6678 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ Word 𝐶)
141 wrdf 13680 . . . . . . . . . . . 12 ((𝑓𝑦) ∈ Word 𝐶 → (𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶)
142 fdm 6354 . . . . . . . . . . . 12 ((𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶 → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
143140, 141, 1423syl 18 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
144 fzofi 13160 . . . . . . . . . . 11 (0..^(♯‘(𝑓𝑦))) ∈ Fin
145143, 144syl6eqel 2874 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) ∈ Fin)
146 xpfi 8586 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ dom (𝑓𝑦) ∈ Fin) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
147138, 145, 146sylancr 578 . . . . . . . . 9 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
148147ralrimiva 3132 . . . . . . . 8 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
149 iunfi 8609 . . . . . . . 8 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
15025, 148, 149syl2an2r 672 . . . . . . 7 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
151137, 150syl5eqel 2870 . . . . . 6 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin)
152 hashcl 13535 . . . . . 6 ( 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin → (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0)
153 hashfzo0 13607 . . . . . 6 ((♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0 → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
154151, 152, 1533syl 18 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
155 fzofi 13160 . . . . . 6 (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin
156 hashen 13525 . . . . . 6 (((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin ∧ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
157155, 151, 156sylancr 578 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
158154, 157mpbid 224 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
159 bren 8317 . . . 4 ((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ↔ ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
160158, 159sylib 210 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
1616adantr 473 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐺 ∈ Abel)
16211adantr 473 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐵 ∈ Fin)
163 breq1 4933 . . . . . . . 8 (𝑤 = 𝑎 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑎 ∥ (♯‘𝐵)))
164163cbvrabv 3412 . . . . . . 7 {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
1652, 164eqtri 2802 . . . . . 6 𝐴 = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
166 fveq2 6501 . . . . . . . . . . 11 (𝑥 = 𝑐 → (𝑂𝑥) = (𝑂𝑐))
167166breq1d 4940 . . . . . . . . . 10 (𝑥 = 𝑐 → ((𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))))
168167cbvrabv 3412 . . . . . . . . 9 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}
169 id 22 . . . . . . . . . . . 12 (𝑝 = 𝑏𝑝 = 𝑏)
170 oveq1 6985 . . . . . . . . . . . 12 (𝑝 = 𝑏 → (𝑝 pCnt (♯‘𝐵)) = (𝑏 pCnt (♯‘𝐵)))
171169, 170oveq12d 6996 . . . . . . . . . . 11 (𝑝 = 𝑏 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑏↑(𝑏 pCnt (♯‘𝐵))))
172171breq2d 4942 . . . . . . . . . 10 (𝑝 = 𝑏 → ((𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))))
173172rabbidv 3403 . . . . . . . . 9 (𝑝 = 𝑏 → {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
174168, 173syl5eq 2826 . . . . . . . 8 (𝑝 = 𝑏 → {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
175174cbvmptv 5029 . . . . . . 7 (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
17628, 175eqtri 2802 . . . . . 6 𝑆 = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
177 breq2 4934 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐺dom DProd 𝑠𝐺dom DProd 𝑡))
178 oveq2 6986 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑡))
179178eqeq1d 2780 . . . . . . . . . 10 (𝑠 = 𝑡 → ((𝐺 DProd 𝑠) = 𝑔 ↔ (𝐺 DProd 𝑡) = 𝑔))
180177, 179anbi12d 621 . . . . . . . . 9 (𝑠 = 𝑡 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔) ↔ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)))
181180cbvrabv 3412 . . . . . . . 8 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)} = {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)}
182181mpteq2i 5020 . . . . . . 7 (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
18339, 182eqtri 2802 . . . . . 6 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
184 simprll 766 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
185 simprlr 767 . . . . . . 7 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))
186 2fveq3 6506 . . . . . . . . 9 (𝑞 = 𝑦 → (𝑊‘(𝑆𝑞)) = (𝑊‘(𝑆𝑦)))
187134, 186eleq12d 2860 . . . . . . . 8 (𝑞 = 𝑦 → ((𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦))))
188187cbvralv 3383 . . . . . . 7 (∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
189185, 188sylib 210 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
190 simprr 760 . . . . . 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 18961 . . . . 5 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → (𝑊𝐵) ≠ ∅)
192191expr 449 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (:(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
193192exlimdv 1892 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
194160, 193mpd 15 . 2 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (𝑊𝐵) ≠ ∅)
195132, 194exlimddv 1894 1 (𝜑 → (𝑊𝐵) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wex 1742  wcel 2050  wne 2967  wral 3088  wrex 3089  {crab 3092  cin 3830  wss 3831  c0 4180  𝒫 cpw 4423  {csn 4442   ciun 4793   class class class wbr 4930  cmpt 5009   × cxp 5406  dom cdm 5408  ran crn 5409  wf 6186  1-1-ontowf1o 6189  cfv 6190  (class class class)co 6978  cen 8305  Fincfn 8308  0cc0 10337  1c1 10338  cle 10477  cn 11441  0cn0 11710  cz 11796  ...cfz 12711  ..^cfzo 12852  cexp 13247  chash 13508  Word cword 13675  cdvds 15470  cprime 15874   pCnt cpc 16032  Basecbs 16342  s cress 16343  Grpcgrp 17894  SubGrpcsubg 18060  odcod 18417   pGrp cpgp 18419  Abelcabl 18670  CycGrpccyg 18755   DProd cdprd 18868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5050  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-inf2 8900  ax-cnex 10393  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414  ax-pre-sup 10415
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-int 4751  df-iun 4795  df-iin 4796  df-disj 4899  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-se 5368  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-isom 6199  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-of 7229  df-rpss 7269  df-om 7399  df-1st 7503  df-2nd 7504  df-supp 7636  df-tpos 7697  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-1o 7907  df-2o 7908  df-oadd 7911  df-omul 7912  df-er 8091  df-ec 8093  df-qs 8097  df-map 8210  df-ixp 8262  df-en 8309  df-dom 8310  df-sdom 8311  df-fin 8312  df-fsupp 8631  df-sup 8703  df-inf 8704  df-oi 8771  df-dju 9126  df-card 9164  df-acn 9167  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-div 11101  df-nn 11442  df-2 11506  df-3 11507  df-n0 11711  df-xnn0 11783  df-z 11797  df-uz 12062  df-q 12166  df-rp 12208  df-fz 12712  df-fzo 12853  df-fl 12980  df-mod 13056  df-seq 13188  df-exp 13248  df-fac 13452  df-bc 13481  df-hash 13509  df-word 13676  df-concat 13737  df-s1 13762  df-cj 14322  df-re 14323  df-im 14324  df-sqrt 14458  df-abs 14459  df-clim 14709  df-sum 14907  df-dvds 15471  df-gcd 15707  df-prm 15875  df-pc 16033  df-ndx 16345  df-slot 16346  df-base 16348  df-sets 16349  df-ress 16350  df-plusg 16437  df-0g 16574  df-gsum 16575  df-mre 16718  df-mrc 16719  df-acs 16721  df-mgm 17713  df-sgrp 17755  df-mnd 17766  df-mhm 17806  df-submnd 17807  df-grp 17897  df-minusg 17898  df-sbg 17899  df-mulg 18015  df-subg 18063  df-eqg 18065  df-ghm 18130  df-gim 18173  df-ga 18194  df-cntz 18221  df-oppg 18248  df-od 18421  df-gex 18422  df-pgp 18423  df-lsm 18525  df-pj1 18526  df-cmn 18671  df-abl 18672  df-cyg 18756  df-dprd 18870
This theorem is referenced by:  ablfac  18963
  Copyright terms: Public domain W3C validator