Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . 4
⊢ (𝜑 → (1...(#‘𝐵)) ∈ Fin) |
2 | | ablfac.a |
. . . . 5
⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} |
3 | | prmnn 15226 |
. . . . . . . 8
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℕ) |
4 | 3 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → 𝑤 ∈ ℕ) |
5 | | prmz 15227 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℤ) |
6 | | ablfac.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ Abel) |
7 | | ablgrp 18021 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
8 | | ablfac.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐺) |
9 | 8 | grpbn0 17274 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
10 | 6, 7, 9 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ ∅) |
11 | | ablfac.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ Fin) |
12 | | hashnncl 13018 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin →
((#‘𝐵) ∈ ℕ
↔ 𝐵 ≠
∅)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
14 | 10, 13 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐵) ∈ ℕ) |
15 | | dvdsle 14870 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℤ ∧
(#‘𝐵) ∈ ℕ)
→ (𝑤 ∥
(#‘𝐵) → 𝑤 ≤ (#‘𝐵))) |
16 | 5, 14, 15 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (#‘𝐵) → 𝑤 ≤ (#‘𝐵))) |
17 | 16 | 3impia 1253 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → 𝑤 ≤ (#‘𝐵)) |
18 | 14 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐵) ∈ ℤ) |
19 | 18 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → (#‘𝐵) ∈ ℤ) |
20 | | fznn 12278 |
. . . . . . . 8
⊢
((#‘𝐵) ∈
ℤ → (𝑤 ∈
(1...(#‘𝐵)) ↔
(𝑤 ∈ ℕ ∧
𝑤 ≤ (#‘𝐵)))) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → (𝑤 ∈ (1...(#‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (#‘𝐵)))) |
22 | 4, 17, 21 | mpbir2and 959 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → 𝑤 ∈ (1...(#‘𝐵))) |
23 | 22 | rabssdv 3645 |
. . . . 5
⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} ⊆ (1...(#‘𝐵))) |
24 | 2, 23 | syl5eqss 3612 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (1...(#‘𝐵))) |
25 | | ssfi 8065 |
. . . 4
⊢
(((1...(#‘𝐵))
∈ Fin ∧ 𝐴 ⊆
(1...(#‘𝐵))) →
𝐴 ∈
Fin) |
26 | 1, 24, 25 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
27 | | dfin5 3548 |
. . . . . . . 8
⊢ (Word
𝐶 ∩ (𝑊‘(𝑆‘𝑞))) = {𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ (𝑊‘(𝑆‘𝑞))} |
28 | | ablfac.o |
. . . . . . . . . . . . . 14
⊢ 𝑂 = (od‘𝐺) |
29 | | ablfac.s |
. . . . . . . . . . . . . 14
⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) |
30 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} ⊆
ℙ |
31 | 2, 30 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ⊆
ℙ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℙ) |
33 | 8, 28, 29, 6, 11, 32 | ablfac1b 18292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
34 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐺)
∈ V |
35 | 8, 34 | eqeltri 2684 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ∈ V |
36 | 35 | rabex 4740 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ V |
37 | 36, 29 | dmmpti 5936 |
. . . . . . . . . . . . . 14
⊢ dom 𝑆 = 𝐴 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝑆 = 𝐴) |
39 | 33, 38 | dprdf2 18229 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
40 | 39 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
41 | | ablfac.c |
. . . . . . . . . . . 12
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
42 | | ablfac.w |
. . . . . . . . . . . 12
⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) |
43 | 8, 41, 6, 11, 28, 2, 29, 42 | ablfaclem1 18307 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆‘𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))}) |
44 | 40, 43 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑊‘(𝑆‘𝑞)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))}) |
45 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))} ⊆ Word 𝐶 |
46 | 44, 45 | syl6eqss 3618 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑊‘(𝑆‘𝑞)) ⊆ Word 𝐶) |
47 | | sseqin2 3779 |
. . . . . . . . 9
⊢ ((𝑊‘(𝑆‘𝑞)) ⊆ Word 𝐶 ↔ (Word 𝐶 ∩ (𝑊‘(𝑆‘𝑞))) = (𝑊‘(𝑆‘𝑞))) |
48 | 46, 47 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (Word 𝐶 ∩ (𝑊‘(𝑆‘𝑞))) = (𝑊‘(𝑆‘𝑞))) |
49 | 27, 48 | syl5eqr 2658 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ (𝑊‘(𝑆‘𝑞))} = (𝑊‘(𝑆‘𝑞))) |
50 | 49, 44 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ (𝑊‘(𝑆‘𝑞))} = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))}) |
51 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(𝐺
↾s (𝑆‘𝑞))) = (Base‘(𝐺 ↾s (𝑆‘𝑞))) |
52 | | eqid 2610 |
. . . . . . . . 9
⊢ {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
53 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺 ∈ Abel) |
54 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s (𝑆‘𝑞)) = (𝐺 ↾s (𝑆‘𝑞)) |
55 | 54 | subgabl 18064 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Abel ∧ (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) → (𝐺 ↾s (𝑆‘𝑞)) ∈ Abel) |
56 | 53, 40, 55 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 ↾s (𝑆‘𝑞)) ∈ Abel) |
57 | 32 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) |
58 | 54 | subgbas 17421 |
. . . . . . . . . . . . . 14
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) |
59 | 40, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑆‘𝑞)) = (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞))))) |
61 | 8, 28, 29, 6, 11, 32 | ablfac1a 18291 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
62 | 60, 61 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞)))) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
63 | 62 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞))))) = (𝑞 pCnt (𝑞↑(𝑞 pCnt (#‘𝐵))))) |
64 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘𝐵) ∈ ℕ) |
65 | 57, 64 | pccld 15393 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ∈
ℕ0) |
66 | 65 | nn0zd 11356 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ∈ ℤ) |
67 | | pcid 15415 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℙ ∧ (𝑞 pCnt (#‘𝐵)) ∈ ℤ) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (#‘𝐵)))) = (𝑞 pCnt (#‘𝐵))) |
68 | 57, 66, 67 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (𝑞↑(𝑞 pCnt (#‘𝐵)))) = (𝑞 pCnt (#‘𝐵))) |
69 | 63, 68 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞))))) = (𝑞 pCnt (#‘𝐵))) |
70 | 69 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞)))))) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
71 | 62, 70 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞)))) = (𝑞↑(𝑞 pCnt (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞))))))) |
72 | 54 | subggrp 17420 |
. . . . . . . . . . . 12
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝐺 ↾s (𝑆‘𝑞)) ∈ Grp) |
73 | 40, 72 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 ↾s (𝑆‘𝑞)) ∈ Grp) |
74 | 11 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin) |
75 | 8 | subgss 17418 |
. . . . . . . . . . . . . 14
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵) |
76 | 40, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵) |
77 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ (𝑆‘𝑞) ⊆ 𝐵) → (𝑆‘𝑞) ∈ Fin) |
78 | 74, 76, 77 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin) |
79 | 59, 78 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (Base‘(𝐺 ↾s (𝑆‘𝑞))) ∈ Fin) |
80 | 51 | pgpfi2 17844 |
. . . . . . . . . . 11
⊢ (((𝐺 ↾s (𝑆‘𝑞)) ∈ Grp ∧ (Base‘(𝐺 ↾s (𝑆‘𝑞))) ∈ Fin) → (𝑞 pGrp (𝐺 ↾s (𝑆‘𝑞)) ↔ (𝑞 ∈ ℙ ∧
(#‘(Base‘(𝐺
↾s (𝑆‘𝑞)))) = (𝑞↑(𝑞 pCnt (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞))))))))) |
81 | 73, 79, 80 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pGrp (𝐺 ↾s (𝑆‘𝑞)) ↔ (𝑞 ∈ ℙ ∧
(#‘(Base‘(𝐺
↾s (𝑆‘𝑞)))) = (𝑞↑(𝑞 pCnt (#‘(Base‘(𝐺 ↾s (𝑆‘𝑞))))))))) |
82 | 57, 71, 81 | mpbir2and 959 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 pGrp (𝐺 ↾s (𝑆‘𝑞))) |
83 | 51, 52, 56, 82, 79 | pgpfac 18306 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠 ∧ ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞))))) |
84 | | ssrab2 3650 |
. . . . . . . . . . . . . 14
⊢ {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
(SubGrp‘(𝐺
↾s (𝑆‘𝑞))) |
85 | | sswrd 13168 |
. . . . . . . . . . . . . 14
⊢ ({𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
(SubGrp‘(𝐺
↾s (𝑆‘𝑞))) → Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
Word (SubGrp‘(𝐺
↾s (𝑆‘𝑞)))) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Word
{𝑟 ∈
(SubGrp‘(𝐺
↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
Word (SubGrp‘(𝐺
↾s (𝑆‘𝑞))) |
87 | 86 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} →
𝑠 ∈ Word
(SubGrp‘(𝐺
↾s (𝑆‘𝑞)))) |
88 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
90 | 54 | subgdmdprd 18256 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → ((𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆‘𝑞)))) |
91 | 88, 90 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) → ((𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 (𝑆‘𝑞)))) |
92 | 91 | simprbda 651 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → 𝐺dom DProd 𝑠) |
93 | 91 | simplbda 652 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → ran 𝑠 ⊆ 𝒫 (𝑆‘𝑞)) |
94 | 54, 89, 92, 93 | subgdprd 18257 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (𝐺 DProd 𝑠)) |
95 | 59 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → (𝑆‘𝑞) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) |
96 | 95 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → (Base‘(𝐺 ↾s (𝑆‘𝑞))) = (𝑆‘𝑞)) |
97 | 94, 96 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → (((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞))) ↔ (𝐺 DProd 𝑠) = (𝑆‘𝑞))) |
98 | 97 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → (((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞))) → (𝐺 DProd 𝑠) = (𝑆‘𝑞))) |
99 | 98, 92 | jctild 564 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) ∧ (𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠) → (((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞)))) |
100 | 99 | expimpd 627 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) → (((𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠 ∧ ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞)))) |
101 | 87, 100 | sylan2 490 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) →
(((𝐺 ↾s
(𝑆‘𝑞))dom DProd 𝑠 ∧ ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) → (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞)))) |
102 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑦 → ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) = ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦)) |
103 | 102 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑦 → (((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔
((𝐺 ↾s
(𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp
))) |
104 | 103 | cbvrabv 3172 |
. . . . . . . . . . . . . 14
⊢ {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} = {𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp
)} |
105 | 54 | subsubg 17440 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆‘𝑞)))) |
106 | 40, 105 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆‘𝑞)))) |
107 | 106 | simprbda 651 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) → 𝑦 ∈ (SubGrp‘𝐺)) |
108 | 107 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
𝑦 ∈
(SubGrp‘𝐺)) |
109 | 40 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
(𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
110 | 106 | simplbda 652 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞)))) → 𝑦 ⊆ (𝑆‘𝑞)) |
111 | 110 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
𝑦 ⊆ (𝑆‘𝑞)) |
112 | | ressabs 15766 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝑦 ⊆ (𝑆‘𝑞)) → ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) = (𝐺 ↾s 𝑦)) |
113 | 109, 111,
112 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
((𝐺 ↾s
(𝑆‘𝑞)) ↾s 𝑦) = (𝐺 ↾s 𝑦)) |
114 | | simp3 1056 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
((𝐺 ↾s
(𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp
)) |
115 | 113, 114 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
(𝐺 ↾s
𝑦) ∈ (CycGrp ∩ ran
pGrp )) |
116 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑦 → (𝐺 ↾s 𝑟) = (𝐺 ↾s 𝑦)) |
117 | 116 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑦 → ((𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔
(𝐺 ↾s
𝑦) ∈ (CycGrp ∩ ran
pGrp ))) |
118 | 117, 41 | elrab2 3333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐶 ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp
))) |
119 | 108, 115,
118 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∧ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )) →
𝑦 ∈ 𝐶) |
120 | 119 | rabssdv 3645 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {𝑦 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑦) ∈ (CycGrp ∩ ran pGrp )} ⊆
𝐶) |
121 | 104, 120 | syl5eqss 3612 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
𝐶) |
122 | | sswrd 13168 |
. . . . . . . . . . . . 13
⊢ ({𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
𝐶 → Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
Word 𝐶) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
Word 𝐶) |
124 | 123 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) →
𝑠 ∈ Word 𝐶) |
125 | 101, 124 | jctild 564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}) →
(((𝐺 ↾s
(𝑆‘𝑞))dom DProd 𝑠 ∧ ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))))) |
126 | 125 | expimpd 627 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ∧
((𝐺 ↾s
(𝑆‘𝑞))dom DProd 𝑠 ∧ ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞))))) → (𝑠 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))))) |
127 | 126 | reximdv2 2997 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (∃𝑠 ∈ Word {𝑟 ∈ (SubGrp‘(𝐺 ↾s (𝑆‘𝑞))) ∣ ((𝐺 ↾s (𝑆‘𝑞)) ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ((𝐺 ↾s (𝑆‘𝑞))dom DProd 𝑠 ∧ ((𝐺 ↾s (𝑆‘𝑞)) DProd 𝑠) = (Base‘(𝐺 ↾s (𝑆‘𝑞)))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞)))) |
128 | 83, 127 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))) |
129 | | rabn0 3912 |
. . . . . . 7
⊢ ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))) |
130 | 128, 129 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑞))} ≠ ∅) |
131 | 50, 130 | eqnetrd 2849 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ (𝑊‘(𝑆‘𝑞))} ≠ ∅) |
132 | | rabn0 3912 |
. . . . 5
⊢ ({𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ (𝑊‘(𝑆‘𝑞))} ≠ ∅ ↔ ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆‘𝑞))) |
133 | 131, 132 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆‘𝑞))) |
134 | 133 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑞 ∈ 𝐴 ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆‘𝑞))) |
135 | | eleq1 2676 |
. . . 4
⊢ (𝑦 = (𝑓‘𝑞) → (𝑦 ∈ (𝑊‘(𝑆‘𝑞)) ↔ (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) |
136 | 135 | ac6sfi 8089 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ ∀𝑞 ∈ 𝐴 ∃𝑦 ∈ Word 𝐶𝑦 ∈ (𝑊‘(𝑆‘𝑞))) → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) |
137 | 26, 134, 136 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) |
138 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑞 = 𝑦 → {𝑞} = {𝑦}) |
139 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑦 → (𝑓‘𝑞) = (𝑓‘𝑦)) |
140 | 139 | dmeqd 5248 |
. . . . . . . . 9
⊢ (𝑞 = 𝑦 → dom (𝑓‘𝑞) = dom (𝑓‘𝑦)) |
141 | 138, 140 | xpeq12d 5064 |
. . . . . . . 8
⊢ (𝑞 = 𝑦 → ({𝑞} × dom (𝑓‘𝑞)) = ({𝑦} × dom (𝑓‘𝑦))) |
142 | 141 | cbviunv 4495 |
. . . . . . 7
⊢ ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) = ∪
𝑦 ∈ 𝐴 ({𝑦} × dom (𝑓‘𝑦)) |
143 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → 𝐴 ∈ Fin) |
144 | | snfi 7923 |
. . . . . . . . . 10
⊢ {𝑦} ∈ Fin |
145 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → 𝑓:𝐴⟶Word 𝐶) |
146 | 145 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) ∈ Word 𝐶) |
147 | | wrdf 13165 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑦) ∈ Word 𝐶 → (𝑓‘𝑦):(0..^(#‘(𝑓‘𝑦)))⟶𝐶) |
148 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑦):(0..^(#‘(𝑓‘𝑦)))⟶𝐶 → dom (𝑓‘𝑦) = (0..^(#‘(𝑓‘𝑦)))) |
149 | 146, 147,
148 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) ∧ 𝑦 ∈ 𝐴) → dom (𝑓‘𝑦) = (0..^(#‘(𝑓‘𝑦)))) |
150 | | fzofi 12635 |
. . . . . . . . . . 11
⊢
(0..^(#‘(𝑓‘𝑦))) ∈ Fin |
151 | 149, 150 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) ∧ 𝑦 ∈ 𝐴) → dom (𝑓‘𝑦) ∈ Fin) |
152 | | xpfi 8116 |
. . . . . . . . . 10
⊢ (({𝑦} ∈ Fin ∧ dom (𝑓‘𝑦) ∈ Fin) → ({𝑦} × dom (𝑓‘𝑦)) ∈ Fin) |
153 | 144, 151,
152 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) ∧ 𝑦 ∈ 𝐴) → ({𝑦} × dom (𝑓‘𝑦)) ∈ Fin) |
154 | 153 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → ∀𝑦 ∈ 𝐴 ({𝑦} × dom (𝑓‘𝑦)) ∈ Fin) |
155 | | iunfi 8137 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ ∀𝑦 ∈ 𝐴 ({𝑦} × dom (𝑓‘𝑦)) ∈ Fin) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝑓‘𝑦)) ∈ Fin) |
156 | 143, 154,
155 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝑓‘𝑦)) ∈ Fin) |
157 | 142, 156 | syl5eqel 2692 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) ∈ Fin) |
158 | | hashcl 13009 |
. . . . . 6
⊢ (∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) ∈ Fin → (#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) ∈
ℕ0) |
159 | | hashfzo0 13077 |
. . . . . 6
⊢
((#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) ∈ ℕ0 →
(#‘(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))) = (#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) |
160 | 157, 158,
159 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → (#‘(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))) = (#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) |
161 | | fzofi 12635 |
. . . . . 6
⊢
(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) ∈ Fin |
162 | | hashen 12997 |
. . . . . 6
⊢
(((0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) ∈ Fin ∧ ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) ∈ Fin) →
((#‘(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))) = (#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) ↔ (0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) ≈ ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) |
163 | 161, 157,
162 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → ((#‘(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))) = (#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) ↔ (0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) ≈ ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) |
164 | 160, 163 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → (0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) ≈ ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) |
165 | | bren 7850 |
. . . 4
⊢
((0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) ≈ ∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) ↔ ∃ℎ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) |
166 | 164, 165 | sylib 207 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → ∃ℎ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) |
167 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → 𝐺 ∈ Abel) |
168 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → 𝐵 ∈ Fin) |
169 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑤 = 𝑎 → (𝑤 ∥ (#‘𝐵) ↔ 𝑎 ∥ (#‘𝐵))) |
170 | 169 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (#‘𝐵)} |
171 | 2, 170 | eqtri 2632 |
. . . . . 6
⊢ 𝐴 = {𝑎 ∈ ℙ ∣ 𝑎 ∥ (#‘𝐵)} |
172 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑐 → (𝑂‘𝑥) = (𝑂‘𝑐)) |
173 | 172 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑐 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) ↔ (𝑂‘𝑐) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))))) |
174 | 173 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} = {𝑐 ∈ 𝐵 ∣ (𝑂‘𝑐) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} |
175 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑏 → 𝑝 = 𝑏) |
176 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑏 → (𝑝 pCnt (#‘𝐵)) = (𝑏 pCnt (#‘𝐵))) |
177 | 175, 176 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑏 → (𝑝↑(𝑝 pCnt (#‘𝐵))) = (𝑏↑(𝑏 pCnt (#‘𝐵)))) |
178 | 177 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑏 → ((𝑂‘𝑐) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) ↔ (𝑂‘𝑐) ∥ (𝑏↑(𝑏 pCnt (#‘𝐵))))) |
179 | 178 | rabbidv 3164 |
. . . . . . . . 9
⊢ (𝑝 = 𝑏 → {𝑐 ∈ 𝐵 ∣ (𝑂‘𝑐) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} = {𝑐 ∈ 𝐵 ∣ (𝑂‘𝑐) ∥ (𝑏↑(𝑏 pCnt (#‘𝐵)))}) |
180 | 174, 179 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝑝 = 𝑏 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} = {𝑐 ∈ 𝐵 ∣ (𝑂‘𝑐) ∥ (𝑏↑(𝑏 pCnt (#‘𝐵)))}) |
181 | 180 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) = (𝑏 ∈ 𝐴 ↦ {𝑐 ∈ 𝐵 ∣ (𝑂‘𝑐) ∥ (𝑏↑(𝑏 pCnt (#‘𝐵)))}) |
182 | 29, 181 | eqtri 2632 |
. . . . . 6
⊢ 𝑆 = (𝑏 ∈ 𝐴 ↦ {𝑐 ∈ 𝐵 ∣ (𝑂‘𝑐) ∥ (𝑏↑(𝑏 pCnt (#‘𝐵)))}) |
183 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑡)) |
184 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑡)) |
185 | 184 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → ((𝐺 DProd 𝑠) = 𝑔 ↔ (𝐺 DProd 𝑡) = 𝑔)) |
186 | 183, 185 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔) ↔ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔))) |
187 | 186 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)} = {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)} |
188 | 187 | mpteq2i 4669 |
. . . . . . 7
⊢ (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)}) |
189 | 42, 188 | eqtri 2632 |
. . . . . 6
⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑡 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑡 ∧ (𝐺 DProd 𝑡) = 𝑔)}) |
190 | | simprll 798 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → 𝑓:𝐴⟶Word 𝐶) |
191 | | simprlr 799 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) |
192 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑦 → (𝑆‘𝑞) = (𝑆‘𝑦)) |
193 | 192 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑞 = 𝑦 → (𝑊‘(𝑆‘𝑞)) = (𝑊‘(𝑆‘𝑦))) |
194 | 139, 193 | eleq12d 2682 |
. . . . . . . 8
⊢ (𝑞 = 𝑦 → ((𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)) ↔ (𝑓‘𝑦) ∈ (𝑊‘(𝑆‘𝑦)))) |
195 | 194 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑞 ∈
𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)) ↔ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) |
196 | 191, 195 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) |
197 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))) |
198 | 8, 41, 167, 168, 28, 171, 182, 189, 190, 196, 142, 197 | ablfaclem2 18308 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞))) ∧ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)))) → (𝑊‘𝐵) ≠ ∅) |
199 | 198 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → (ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) → (𝑊‘𝐵) ≠ ∅)) |
200 | 199 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → (∃ℎ ℎ:(0..^(#‘∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞))))–1-1-onto→∪ 𝑞 ∈ 𝐴 ({𝑞} × dom (𝑓‘𝑞)) → (𝑊‘𝐵) ≠ ∅)) |
201 | 166, 200 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑓:𝐴⟶Word 𝐶 ∧ ∀𝑞 ∈ 𝐴 (𝑓‘𝑞) ∈ (𝑊‘(𝑆‘𝑞)))) → (𝑊‘𝐵) ≠ ∅) |
202 | 137, 201 | exlimddv 1850 |
1
⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) |