Step |
Hyp |
Ref |
Expression |
1 |
|
pgpfac.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
pgpfac.c |
⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } |
3 |
|
pgpfac.g |
⊢ ( 𝜑 → 𝐺 ∈ Abel ) |
4 |
|
pgpfac.p |
⊢ ( 𝜑 → 𝑃 pGrp 𝐺 ) |
5 |
|
pgpfac.f |
⊢ ( 𝜑 → 𝐵 ∈ Fin ) |
6 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
7 |
1
|
subgid |
⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ) |
8 |
3 6 7
|
3syl |
⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ) |
9 |
|
eleq1 |
⊢ ( 𝑡 = 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) |
10 |
|
eqeq2 |
⊢ ( 𝑡 = 𝑢 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) |
11 |
10
|
anbi2d |
⊢ ( 𝑡 = 𝑢 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) |
12 |
11
|
rexbidv |
⊢ ( 𝑡 = 𝑢 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) |
13 |
9 12
|
imbi12d |
⊢ ( 𝑡 = 𝑢 → ( ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) |
14 |
13
|
imbi2d |
⊢ ( 𝑡 = 𝑢 → ( ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝜑 → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) ) |
15 |
|
eleq1 |
⊢ ( 𝑡 = 𝐵 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ) ) |
16 |
|
eqeq2 |
⊢ ( 𝑡 = 𝐵 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) |
17 |
16
|
anbi2d |
⊢ ( 𝑡 = 𝐵 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) |
18 |
17
|
rexbidv |
⊢ ( 𝑡 = 𝐵 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) |
19 |
15 18
|
imbi12d |
⊢ ( 𝑡 = 𝐵 → ( ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) ) |
20 |
19
|
imbi2d |
⊢ ( 𝑡 = 𝐵 → ( ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝜑 → ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) ) ) |
21 |
|
bi2.04 |
⊢ ( ( 𝑡 ⊊ 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) |
22 |
21
|
imbi2i |
⊢ ( ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ) |
23 |
|
bi2.04 |
⊢ ( ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ) |
24 |
|
bi2.04 |
⊢ ( ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ) |
25 |
22 23 24
|
3bitr4i |
⊢ ( ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ) |
26 |
25
|
albii |
⊢ ( ∀ 𝑡 ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ) |
27 |
|
df-ral |
⊢ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ) |
28 |
|
r19.21v |
⊢ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) |
29 |
26 27 28
|
3bitr2i |
⊢ ( ∀ 𝑡 ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) |
30 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝐺 ∈ Abel ) |
31 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑃 pGrp 𝐺 ) |
32 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝐵 ∈ Fin ) |
33 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) |
34 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) |
35 |
|
psseq1 |
⊢ ( 𝑡 = 𝑥 → ( 𝑡 ⊊ 𝑢 ↔ 𝑥 ⊊ 𝑢 ) ) |
36 |
|
eqeq2 |
⊢ ( 𝑡 = 𝑥 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) |
37 |
36
|
anbi2d |
⊢ ( 𝑡 = 𝑥 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) ) |
38 |
37
|
rexbidv |
⊢ ( 𝑡 = 𝑥 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) ) |
39 |
35 38
|
imbi12d |
⊢ ( 𝑡 = 𝑥 → ( ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝑥 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) ) ) |
40 |
39
|
cbvralvw |
⊢ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑥 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) ) |
41 |
34 40
|
sylib |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑥 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) ) |
42 |
1 2 30 31 32 33 41
|
pgpfaclem3 |
⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) |
43 |
42
|
exp32 |
⊢ ( 𝜑 → ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) |
44 |
43
|
a1i |
⊢ ( 𝑢 ∈ Fin → ( 𝜑 → ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) ) |
45 |
44
|
a2d |
⊢ ( 𝑢 ∈ Fin → ( ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) → ( 𝜑 → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) ) |
46 |
29 45
|
syl5bi |
⊢ ( 𝑢 ∈ Fin → ( ∀ 𝑡 ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) → ( 𝜑 → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) ) |
47 |
14 20 46
|
findcard3 |
⊢ ( 𝐵 ∈ Fin → ( 𝜑 → ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) ) |
48 |
5 47
|
mpcom |
⊢ ( 𝜑 → ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) |
49 |
8 48
|
mpd |
⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) |