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

Theorem ablfaclem3 18695
Description: Lemma for ablfac 18696. (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 12981 . . . 4 (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
2 ablfac.a . . . . 5 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
3 prmnn 15596 . . . . . . . 8 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
433ad2ant2 1128 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
5 prmz 15597 . . . . . . . . 9 (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
6 ablfac.1 . . . . . . . . . . 11 (𝜑𝐺 ∈ Abel)
7 ablgrp 18406 . . . . . . . . . . 11 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
8 ablfac.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
98grpbn0 17660 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
106, 7, 93syl 18 . . . . . . . . . 10 (𝜑𝐵 ≠ ∅)
11 ablfac.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ Fin)
12 hashnncl 13360 . . . . . . . . . . 11 (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1311, 12syl 17 . . . . . . . . . 10 (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1410, 13mpbird 247 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ)
15 dvdsle 15242 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
165, 14, 15syl2anr 578 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
17163impia 1109 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
1814nnzd 11684 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℤ)
19183ad2ant1 1127 . . . . . . . 8 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
20 fznn 12616 . . . . . . . 8 ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
224, 17, 21mpbir2and 686 . . . . . 6 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
2322rabssdv 3832 . . . . 5 (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
242, 23syl5eqss 3799 . . . 4 (𝜑𝐴 ⊆ (1...(♯‘𝐵)))
25 ssfi 8337 . . . 4 (((1...(♯‘𝐵)) ∈ Fin ∧ 𝐴 ⊆ (1...(♯‘𝐵))) → 𝐴 ∈ Fin)
261, 24, 25syl2anc 567 . . 3 (𝜑𝐴 ∈ Fin)
27 dfin5 3732 . . . . . . . 8 (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))}
28 ablfac.o . . . . . . . . . . . . . 14 𝑂 = (od‘𝐺)
29 ablfac.s . . . . . . . . . . . . . 14 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
30 ssrab2 3837 . . . . . . . . . . . . . . . 16 {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ ℙ
312, 30eqsstri 3785 . . . . . . . . . . . . . . 15 𝐴 ⊆ ℙ
3231a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℙ)
338, 28, 29, 6, 11, 32ablfac1b 18678 . . . . . . . . . . . . 13 (𝜑𝐺dom DProd 𝑆)
34 fvex 6343 . . . . . . . . . . . . . . . . 17 (Base‘𝐺) ∈ V
358, 34eqeltri 2846 . . . . . . . . . . . . . . . 16 𝐵 ∈ V
3635rabex 4947 . . . . . . . . . . . . . . 15 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
3736, 29dmmpti 6164 . . . . . . . . . . . . . 14 dom 𝑆 = 𝐴
3837a1i 11 . . . . . . . . . . . . 13 (𝜑 → dom 𝑆 = 𝐴)
3933, 38dprdf2 18615 . . . . . . . . . . . 12 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
4039ffvelrnda 6503 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
41 ablfac.c . . . . . . . . . . . 12 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
42 ablfac.w . . . . . . . . . . . 12 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})
438, 41, 6, 11, 28, 2, 29, 42ablfaclem1 18693 . . . . . . . . . . 11 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
4440, 43syl 17 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
45 ssrab2 3837 . . . . . . . . . 10 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ⊆ Word 𝐶
4644, 45syl6eqss 3805 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑊‘(𝑆𝑞)) ⊆ Word 𝐶)
47 sseqin2 3969 . . . . . . . . 9 ((𝑊‘(𝑆𝑞)) ⊆ Word 𝐶 ↔ (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4846, 47sylib 208 . . . . . . . 8 ((𝜑𝑞𝐴) → (Word 𝐶 ∩ (𝑊‘(𝑆𝑞))) = (𝑊‘(𝑆𝑞)))
4927, 48syl5eqr 2819 . . . . . . 7 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = (𝑊‘(𝑆𝑞)))
5049, 44eqtrd 2805 . . . . . 6 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))})
51 eqid 2771 . . . . . . . . 9 (Base‘(𝐺s (𝑆𝑞))) = (Base‘(𝐺s (𝑆𝑞)))
52 eqid 2771 . . . . . . . . 9 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
536adantr 466 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝐺 ∈ Abel)
54 eqid 2771 . . . . . . . . . . 11 (𝐺s (𝑆𝑞)) = (𝐺s (𝑆𝑞))
5554subgabl 18449 . . . . . . . . . 10 ((𝐺 ∈ Abel ∧ (𝑆𝑞) ∈ (SubGrp‘𝐺)) → (𝐺s (𝑆𝑞)) ∈ Abel)
5653, 40, 55syl2anc 567 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Abel)
5732sselda 3753 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝑞 ∈ ℙ)
5854subgbas 17807 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
5940, 58syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
6059fveq2d 6337 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (♯‘(Base‘(𝐺s (𝑆𝑞)))))
618, 28, 29, 6, 11, 32ablfac1a 18677 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
6260, 61eqtr3d 2807 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
6362oveq2d 6810 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
6414adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑞𝐴) → (♯‘𝐵) ∈ ℕ)
6557, 64pccld 15763 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
6665nn0zd 11683 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
67 pcid 15785 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℙ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6857, 66, 67syl2anc 567 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (♯‘𝐵)))) = (𝑞 pCnt (♯‘𝐵)))
6963, 68eqtrd 2805 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞))))) = (𝑞 pCnt (♯‘𝐵)))
7069oveq2d 6810 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
7162, 70eqtr4d 2808 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))
7254subggrp 17806 . . . . . . . . . . . 12 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝐺s (𝑆𝑞)) ∈ Grp)
7340, 72syl 17 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺s (𝑆𝑞)) ∈ Grp)
7411adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → 𝐵 ∈ Fin)
758subgss 17804 . . . . . . . . . . . . . 14 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) ⊆ 𝐵)
7640, 75syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝑆𝑞) ⊆ 𝐵)
77 ssfi 8337 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑆𝑞) ⊆ 𝐵) → (𝑆𝑞) ∈ Fin)
7874, 76, 77syl2anc 567 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ Fin)
7959, 78eqeltrrd 2851 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (Base‘(𝐺s (𝑆𝑞))) ∈ Fin)
8051pgpfi2 18229 . . . . . . . . . . 11 (((𝐺s (𝑆𝑞)) ∈ Grp ∧ (Base‘(𝐺s (𝑆𝑞))) ∈ Fin) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
8173, 79, 80syl2anc 567 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑞 pGrp (𝐺s (𝑆𝑞)) ↔ (𝑞 ∈ ℙ ∧ (♯‘(Base‘(𝐺s (𝑆𝑞)))) = (𝑞↑(𝑞 pCnt (♯‘(Base‘(𝐺s (𝑆𝑞)))))))))
8257, 71, 81mpbir2and 686 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝑞 pGrp (𝐺s (𝑆𝑞)))
8351, 52, 56, 82, 79pgpfac 18692 . . . . . . . 8 ((𝜑𝑞𝐴) → ∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))))
84 ssrab2 3837 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘(𝐺s (𝑆𝑞)))
85 sswrd 13510 . . . . . . . . . . . . . 14 ({𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘(𝐺s (𝑆𝑞))) → Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word (SubGrp‘(𝐺s (𝑆𝑞))))
8684, 85ax-mp 5 . . . . . . . . . . . . 13 Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word (SubGrp‘(𝐺s (𝑆𝑞)))
8786sseli 3749 . . . . . . . . . . . 12 (𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} → 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞))))
8840adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
8988adantr 466 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
9054subgdmdprd 18642 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
9188, 90syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → ((𝐺s (𝑆𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆𝑞))))
9291simprbda 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → 𝐺dom DProd 𝑠)
9391simplbda 483 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ran 𝑠 ⊆ 𝒫 (𝑆𝑞))
9454, 89, 92, 93subgdprd 18643 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → ((𝐺s (𝑆𝑞)) DProd 𝑠) = (𝐺 DProd 𝑠))
9559ad2antrr 699 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (𝑆𝑞) = (Base‘(𝐺s (𝑆𝑞))))
9695eqcomd 2777 . . . . . . . . . . . . . . . 16 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (Base‘(𝐺s (𝑆𝑞))) = (𝑆𝑞))
9794, 96eqeq12d 2786 . . . . . . . . . . . . . . 15 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) ↔ (𝐺 DProd 𝑠) = (𝑆𝑞)))
9897biimpd 219 . . . . . . . . . . . . . 14 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺 DProd 𝑠) = (𝑆𝑞)))
9998, 92jctild 511 . . . . . . . . . . . . 13 ((((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) ∧ (𝐺s (𝑆𝑞))dom DProd 𝑠) → (((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
10099expimpd 441 . . . . . . . . . . . 12 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺s (𝑆𝑞)))) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
10187, 100sylan2 574 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
102 oveq2 6802 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑦 → ((𝐺s (𝑆𝑞)) ↾s 𝑟) = ((𝐺s (𝑆𝑞)) ↾s 𝑦))
103102eleq1d 2835 . . . . . . . . . . . . . . 15 (𝑟 = 𝑦 → (((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
104103cbvrabv 3349 . . . . . . . . . . . . . 14 {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )}
10554subsubg 17826 . . . . . . . . . . . . . . . . . . 19 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
10640, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐴) → (𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞))))
107106simprbda 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ∈ (SubGrp‘𝐺))
1081073adant3 1126 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ∈ (SubGrp‘𝐺))
109403ad2ant1 1127 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
110106simplbda 483 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞)))) → 𝑦 ⊆ (𝑆𝑞))
1111103adant3 1126 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦 ⊆ (𝑆𝑞))
112 ressabs 16148 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑞) ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆𝑞)) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
113109, 111, 112syl2anc 567 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) = (𝐺s 𝑦))
114 simp3 1132 . . . . . . . . . . . . . . . . 17 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
115113, 114eqeltrrd 2851 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp ))
116 oveq2 6802 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑦 → (𝐺s 𝑟) = (𝐺s 𝑦))
117116eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑦 → ((𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
118117, 41elrab2 3519 . . . . . . . . . . . . . . . 16 (𝑦𝐶 ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (𝐺s 𝑦) ∈ (CycGrp ∩ ran pGrp )))
119108, 115, 118sylanbrc 566 . . . . . . . . . . . . . . 15 (((𝜑𝑞𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∧ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) → 𝑦𝐶)
120119rabssdv 3832 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → {𝑦 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
121104, 120syl5eqss 3799 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶)
122 sswrd 13510 . . . . . . . . . . . . 13 ({𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ 𝐶 → Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word 𝐶)
123121, 122syl 17 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ Word 𝐶)
124123sselda 3753 . . . . . . . . . . 11 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → 𝑠 ∈ Word 𝐶)
125101, 124jctild 511 . . . . . . . . . 10 (((𝜑𝑞𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) → (((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
126125expimpd 441 . . . . . . . . 9 ((𝜑𝑞𝐴) → ((𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ∧ ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞))))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))))
127126reximdv2 3162 . . . . . . . 8 ((𝜑𝑞𝐴) → (∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺s (𝑆𝑞))) ∣ ((𝐺s (𝑆𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺s (𝑆𝑞))dom DProd 𝑠 ∧ ((𝐺s (𝑆𝑞)) DProd 𝑠) = (Base‘(𝐺s (𝑆𝑞)))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))))
12883, 127mpd 15 . . . . . . 7 ((𝜑𝑞𝐴) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))
129 rabn0 4105 . . . . . . 7 ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞)))
130128, 129sylibr 224 . . . . . 6 ((𝜑𝑞𝐴) → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑞))} ≠ ∅)
13150, 130eqnetrd 3010 . . . . 5 ((𝜑𝑞𝐴) → {𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅)
132 rabn0 4105 . . . . 5 ({𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))} ≠ ∅ ↔ ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
133131, 132sylib 208 . . . 4 ((𝜑𝑞𝐴) → ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
134133ralrimiva 3115 . . 3 (𝜑 → ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞)))
135 eleq1 2838 . . . 4 (𝑦 = (𝑓𝑞) → (𝑦 ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
136135ac6sfi 8361 . . 3 ((𝐴 ∈ Fin ∧ ∀𝑞𝐴𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆𝑞))) → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
13726, 134, 136syl2anc 567 . 2 (𝜑 → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))))
138 sneq 4327 . . . . . . . . 9 (𝑞 = 𝑦 → {𝑞} = {𝑦})
139 fveq2 6333 . . . . . . . . . 10 (𝑞 = 𝑦 → (𝑓𝑞) = (𝑓𝑦))
140139dmeqd 5465 . . . . . . . . 9 (𝑞 = 𝑦 → dom (𝑓𝑞) = dom (𝑓𝑦))
141138, 140xpeq12d 5281 . . . . . . . 8 (𝑞 = 𝑦 → ({𝑞} × dom (𝑓𝑞)) = ({𝑦} × dom (𝑓𝑦)))
142141cbviunv 4694 . . . . . . 7 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) = 𝑦𝐴 ({𝑦} × dom (𝑓𝑦))
14326adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝐴 ∈ Fin)
144 snfi 8195 . . . . . . . . . 10 {𝑦} ∈ Fin
145 simprl 748 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
146145ffvelrnda 6503 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → (𝑓𝑦) ∈ Word 𝐶)
147 wrdf 13507 . . . . . . . . . . . 12 ((𝑓𝑦) ∈ Word 𝐶 → (𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶)
148 fdm 6192 . . . . . . . . . . . 12 ((𝑓𝑦):(0..^(♯‘(𝑓𝑦)))⟶𝐶 → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
149146, 147, 1483syl 18 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) = (0..^(♯‘(𝑓𝑦))))
150 fzofi 12982 . . . . . . . . . . 11 (0..^(♯‘(𝑓𝑦))) ∈ Fin
151149, 150syl6eqel 2858 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → dom (𝑓𝑦) ∈ Fin)
152 xpfi 8388 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ dom (𝑓𝑦) ∈ Fin) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
153144, 151, 152sylancr 569 . . . . . . . . 9 (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) ∧ 𝑦𝐴) → ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
154153ralrimiva 3115 . . . . . . . 8 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
155 iunfi 8411 . . . . . . . 8 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
156143, 154, 155syl2anc 567 . . . . . . 7 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑦𝐴 ({𝑦} × dom (𝑓𝑦)) ∈ Fin)
157142, 156syl5eqel 2854 . . . . . 6 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin)
158 hashcl 13350 . . . . . 6 ( 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin → (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0)
159 hashfzo0 13420 . . . . . 6 ((♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ∈ ℕ0 → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
160157, 158, 1593syl 18 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
161 fzofi 12982 . . . . . 6 (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin
162 hashen 13340 . . . . . 6 (((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ∈ Fin ∧ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ∈ Fin) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
163161, 157, 162sylancr 569 . . . . 5 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ((♯‘(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))) = (♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))) ↔ (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))
164160, 163mpbid 222 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
165 bren 8119 . . . 4 ((0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) ≈ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) ↔ ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
166164, 165sylib 208 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → ∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
1676adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐺 ∈ Abel)
16811adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝐵 ∈ Fin)
169 breq1 4790 . . . . . . . 8 (𝑤 = 𝑎 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑎 ∥ (♯‘𝐵)))
170169cbvrabv 3349 . . . . . . 7 {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
1712, 170eqtri 2793 . . . . . 6 𝐴 = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (♯‘𝐵)}
172 fveq2 6333 . . . . . . . . . . 11 (𝑥 = 𝑐 → (𝑂𝑥) = (𝑂𝑐))
173172breq1d 4797 . . . . . . . . . 10 (𝑥 = 𝑐 → ((𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))))
174173cbvrabv 3349 . . . . . . . . 9 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}
175 id 22 . . . . . . . . . . . 12 (𝑝 = 𝑏𝑝 = 𝑏)
176 oveq1 6801 . . . . . . . . . . . 12 (𝑝 = 𝑏 → (𝑝 pCnt (♯‘𝐵)) = (𝑏 pCnt (♯‘𝐵)))
177175, 176oveq12d 6812 . . . . . . . . . . 11 (𝑝 = 𝑏 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑏↑(𝑏 pCnt (♯‘𝐵))))
178177breq2d 4799 . . . . . . . . . 10 (𝑝 = 𝑏 → ((𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))))
179178rabbidv 3339 . . . . . . . . 9 (𝑝 = 𝑏 → {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
180174, 179syl5eq 2817 . . . . . . . 8 (𝑝 = 𝑏 → {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
181180cbvmptv 4885 . . . . . . 7 (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
18229, 181eqtri 2793 . . . . . 6 𝑆 = (𝑏𝐴 ↦ {𝑐𝐵 ∣ (𝑂𝑐) ∥ (𝑏↑(𝑏 pCnt (♯‘𝐵)))})
183 breq2 4791 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐺dom DProd 𝑠𝐺dom DProd 𝑡))
184 oveq2 6802 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑡))
185184eqeq1d 2773 . . . . . . . . . 10 (𝑠 = 𝑡 → ((𝐺 DProd 𝑠) = 𝑔 ↔ (𝐺 DProd 𝑡) = 𝑔))
186183, 185anbi12d 610 . . . . . . . . 9 (𝑠 = 𝑡 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔) ↔ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)))
187186cbvrabv 3349 . . . . . . . 8 {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)} = {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)}
188187mpteq2i 4876 . . . . . . 7 (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
18942, 188eqtri 2793 . . . . . 6 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)})
190 simprll 758 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → 𝑓:𝐴⟶Word 𝐶)
191 simprlr 759 . . . . . . 7 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))
192 fveq2 6333 . . . . . . . . . 10 (𝑞 = 𝑦 → (𝑆𝑞) = (𝑆𝑦))
193192fveq2d 6337 . . . . . . . . 9 (𝑞 = 𝑦 → (𝑊‘(𝑆𝑞)) = (𝑊‘(𝑆𝑦)))
194139, 193eleq12d 2844 . . . . . . . 8 (𝑞 = 𝑦 → ((𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦))))
195194cbvralv 3320 . . . . . . 7 (∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)) ↔ ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
196191, 195sylib 208 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → ∀𝑦𝐴 (𝑓𝑦) ∈ (𝑊‘(𝑆𝑦)))
197 simprr 750 . . . . . 6 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))
1988, 41, 167, 168, 28, 171, 182, 189, 190, 196, 142, 197ablfaclem2 18694 . . . . 5 ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞))) ∧ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)))) → (𝑊𝐵) ≠ ∅)
199198expr 444 . . . 4 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (:(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
200199exlimdv 2013 . . 3 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (∃ :(0..^(♯‘ 𝑞𝐴 ({𝑞} × dom (𝑓𝑞))))–1-1-onto 𝑞𝐴 ({𝑞} × dom (𝑓𝑞)) → (𝑊𝐵) ≠ ∅))
201166, 200mpd 15 . 2 ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞𝐴 (𝑓𝑞) ∈ (𝑊‘(𝑆𝑞)))) → (𝑊𝐵) ≠ ∅)
202137, 201exlimddv 2015 1 (𝜑 → (𝑊𝐵) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cin 3723  wss 3724  c0 4064  𝒫 cpw 4298  {csn 4317   ciun 4655   class class class wbr 4787  cmpt 4864   × cxp 5248  dom cdm 5250  ran crn 5251  wf 6028  1-1-ontowf1o 6031  cfv 6032  (class class class)co 6794  cen 8107  Fincfn 8110  0cc0 10139  1c1 10140  cle 10278  cn 11223  0cn0 11495  cz 11580  ...cfz 12534  ..^cfzo 12674  cexp 13068  chash 13322  Word cword 13488  cdvds 15190  cprime 15593   pCnt cpc 15749  Basecbs 16065  s cress 16066  Grpcgrp 17631  SubGrpcsubg 17797  odcod 18152   pGrp cpgp 18154  Abelcabl 18402  CycGrpccyg 18487   DProd cdprd 18601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-disj 4756  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-of 7045  df-rpss 7085  df-om 7214  df-1st 7316  df-2nd 7317  df-supp 7448  df-tpos 7505  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-omul 7719  df-er 7897  df-ec 7899  df-qs 7903  df-map 8012  df-pm 8013  df-ixp 8064  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fsupp 8433  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8966  df-acn 8969  df-cda 9193  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-n0 11496  df-xnn0 11567  df-z 11581  df-uz 11890  df-q 11993  df-rp 12037  df-fz 12535  df-fzo 12675  df-fl 12802  df-mod 12878  df-seq 13010  df-exp 13069  df-fac 13266  df-bc 13295  df-hash 13323  df-word 13496  df-concat 13498  df-s1 13499  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-clim 14428  df-sum 14626  df-dvds 15191  df-gcd 15426  df-prm 15594  df-pc 15750  df-ndx 16068  df-slot 16069  df-base 16071  df-sets 16072  df-ress 16073  df-plusg 16163  df-0g 16311  df-gsum 16312  df-mre 16455  df-mrc 16456  df-acs 16458  df-mgm 17451  df-sgrp 17493  df-mnd 17504  df-mhm 17544  df-submnd 17545  df-grp 17634  df-minusg 17635  df-sbg 17636  df-mulg 17750  df-subg 17800  df-eqg 17802  df-ghm 17867  df-gim 17910  df-ga 17931  df-cntz 17958  df-oppg 17984  df-od 18156  df-gex 18157  df-pgp 18158  df-lsm 18259  df-pj1 18260  df-cmn 18403  df-abl 18404  df-cyg 18488  df-dprd 18603
This theorem is referenced by:  ablfac  18696
  Copyright terms: Public domain W3C validator