Proof of Theorem pgpfaclem1
Step | Hyp | Ref
| Expression |
1 | | pgpfac.t |
. . 3
⊢ 𝑇 = (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) |
2 | | pgpfac.2 |
. . 3
⊢ (𝜑 → 𝑆 ∈ Word 𝐶) |
3 | | pgpfac.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
4 | | pgpfac.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝐺 ↾s 𝑈) |
5 | 4 | subggrp 18069 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Grp) |
7 | | eqid 2778 |
. . . . . . . . 9
⊢
(Base‘𝐻) =
(Base‘𝐻) |
8 | 7 | subgacs 18101 |
. . . . . . . 8
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
9 | | acsmre 16784 |
. . . . . . . 8
⊢
((SubGrp‘𝐻)
∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) |
10 | 6, 8, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(Moore‘(Base‘𝐻))) |
11 | | pgpfac.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
12 | 4 | subgbas 18070 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻)) |
13 | 3, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (Base‘𝐻)) |
14 | 11, 13 | eleqtrd 2868 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) |
15 | | pgpfac.k |
. . . . . . . 8
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐻)) |
16 | 15 | mrcsncl 16744 |
. . . . . . 7
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
17 | 10, 14, 16 | syl2anc 576 |
. . . . . 6
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
18 | 4 | subsubg 18089 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
19 | 3, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
20 | 17, 19 | mpbid 224 |
. . . . 5
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)) |
21 | 20 | simpld 487 |
. . . 4
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) |
22 | 4 | oveq1i 6988 |
. . . . . . 7
⊢ (𝐻 ↾s (𝐾‘{𝑋})) = ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) |
23 | 20 | simprd 488 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈) |
24 | | ressabs 16422 |
. . . . . . . 8
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
25 | 3, 23, 24 | syl2anc 576 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
26 | 22, 25 | syl5eq 2826 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
27 | 7, 15 | cycsubgcyg2 18779 |
. . . . . . 7
⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
28 | 6, 14, 27 | syl2anc 576 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
29 | 26, 28 | eqeltrrd 2867 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
30 | | pgpfac.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
31 | | pgpprm 18482 |
. . . . . . 7
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
33 | | subgpgp 18486 |
. . . . . . 7
⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
34 | 30, 21, 33 | syl2anc 576 |
. . . . . 6
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
35 | | brelrng 5655 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
36 | 32, 29, 34, 35 | syl3anc 1351 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
37 | 29, 36 | elind 4061 |
. . . 4
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
)) |
38 | | oveq2 6986 |
. . . . . 6
⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾s 𝑟) = (𝐺 ↾s (𝐾‘{𝑋}))) |
39 | 38 | eleq1d 2850 |
. . . . 5
⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔
(𝐺 ↾s
(𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
40 | | pgpfac.c |
. . . . 5
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
41 | 39, 40 | elrab2 3599 |
. . . 4
⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
42 | 21, 37, 41 | sylanbrc 575 |
. . 3
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶) |
43 | 1, 2, 42 | cats1cld 14082 |
. 2
⊢ (𝜑 → 𝑇 ∈ Word 𝐶) |
44 | | wrdf 13680 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(♯‘𝑇))⟶𝐶) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶𝐶) |
46 | 40 | ssrab3 3949 |
. . . 4
⊢ 𝐶 ⊆ (SubGrp‘𝐺) |
47 | | fss 6359 |
. . . 4
⊢ ((𝑇:(0..^(♯‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺)) |
48 | 45, 46, 47 | sylancl 577 |
. . 3
⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺)) |
49 | | fzodisj 12889 |
. . . 4
⊢
((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅ |
50 | | lencl 13697 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈
ℕ0) |
51 | 2, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑆) ∈
ℕ0) |
52 | 51 | nn0zd 11901 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑆) ∈
ℤ) |
53 | | fzosn 12926 |
. . . . . 6
⊢
((♯‘𝑆)
∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)}) |
54 | 52, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)}) |
55 | 54 | ineq2d 4078 |
. . . 4
⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) =
((0..^(♯‘𝑆))
∩ {(♯‘𝑆)})) |
56 | 49, 55 | syl5reqr 2829 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅) |
57 | 1 | fveq2i 6504 |
. . . . . . 7
⊢
(♯‘𝑇) =
(♯‘(𝑆 ++
〈“(𝐾‘{𝑋})”〉)) |
58 | 42 | s1cld 13769 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) |
59 | | ccatlen 13741 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) → (♯‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉))) |
60 | 2, 58, 59 | syl2anc 576 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉))) |
61 | 57, 60 | syl5eq 2826 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉))) |
62 | | s1len 13772 |
. . . . . . 7
⊢
(♯‘〈“(𝐾‘{𝑋})”〉) = 1 |
63 | 62 | oveq2i 6989 |
. . . . . 6
⊢
((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉)) = ((♯‘𝑆) + 1) |
64 | 61, 63 | syl6eq 2830 |
. . . . 5
⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1)) |
65 | 64 | oveq2d 6994 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1))) |
66 | | nn0uz 12097 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
67 | 51, 66 | syl6eleq 2876 |
. . . . 5
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘0)) |
68 | | fzosplitsn 12963 |
. . . . 5
⊢
((♯‘𝑆)
∈ (ℤ≥‘0) → (0..^((♯‘𝑆) + 1)) =
((0..^(♯‘𝑆))
∪ {(♯‘𝑆)})) |
69 | 67, 68 | syl 17 |
. . . 4
⊢ (𝜑 → (0..^((♯‘𝑆) + 1)) =
((0..^(♯‘𝑆))
∪ {(♯‘𝑆)})) |
70 | 65, 69 | eqtrd 2814 |
. . 3
⊢ (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})) |
71 | | eqid 2778 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
72 | | eqid 2778 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
73 | | pgpfac.4 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
74 | | cats1un 13917 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
75 | 2, 42, 74 | syl2anc 576 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
76 | 1, 75 | syl5eq 2826 |
. . . . . 6
⊢ (𝜑 → 𝑇 = (𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
77 | 76 | reseq1d 5695 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(♯‘𝑆)))) |
78 | | wrdf 13680 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐶 → 𝑆:(0..^(♯‘𝑆))⟶𝐶) |
79 | | ffn 6346 |
. . . . . . 7
⊢ (𝑆:(0..^(♯‘𝑆))⟶𝐶 → 𝑆 Fn (0..^(♯‘𝑆))) |
80 | 2, 78, 79 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn (0..^(♯‘𝑆))) |
81 | | fzonel 12870 |
. . . . . 6
⊢ ¬
(♯‘𝑆) ∈
(0..^(♯‘𝑆)) |
82 | | fsnunres 6779 |
. . . . . 6
⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬
(♯‘𝑆) ∈
(0..^(♯‘𝑆)))
→ ((𝑆 ∪
{〈(♯‘𝑆),
(𝐾‘{𝑋})〉}) ↾ (0..^(♯‘𝑆))) = 𝑆) |
83 | 80, 81, 82 | sylancl 577 |
. . . . 5
⊢ (𝜑 → ((𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(♯‘𝑆))) = 𝑆) |
84 | 77, 83 | eqtrd 2814 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆) |
85 | 73, 84 | breqtrrd 4958 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆)))) |
86 | | fvex 6514 |
. . . . . 6
⊢
(♯‘𝑆)
∈ V |
87 | | dprdsn 18911 |
. . . . . 6
⊢
(((♯‘𝑆)
∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
88 | 86, 21, 87 | sylancr 578 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
89 | 88 | simpld 487 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) |
90 | | ffn 6346 |
. . . . . . 7
⊢ (𝑇:(0..^(♯‘𝑇))⟶𝐶 → 𝑇 Fn (0..^(♯‘𝑇))) |
91 | 43, 44, 90 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑇 Fn (0..^(♯‘𝑇))) |
92 | | ssun2 4040 |
. . . . . . . 8
⊢
{(♯‘𝑆)}
⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) |
93 | 86 | snss 4593 |
. . . . . . . 8
⊢
((♯‘𝑆)
∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) ↔ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})) |
94 | 92, 93 | mpbir 223 |
. . . . . . 7
⊢
(♯‘𝑆)
∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) |
95 | 94, 70 | syl5eleqr 2873 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑆) ∈
(0..^(♯‘𝑇))) |
96 | | fnressn 6745 |
. . . . . 6
⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈
(0..^(♯‘𝑇)))
→ (𝑇 ↾
{(♯‘𝑆)}) =
{〈(♯‘𝑆),
(𝑇‘(♯‘𝑆))〉}) |
97 | 91, 95, 96 | syl2anc 576 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {〈(♯‘𝑆), (𝑇‘(♯‘𝑆))〉}) |
98 | 1 | fveq1i 6502 |
. . . . . . . . 9
⊢ (𝑇‘(♯‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(♯‘𝑆)) |
99 | 51 | nn0cnd 11772 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑆) ∈
ℂ) |
100 | 99 | addid2d 10643 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆)) |
101 | 100 | eqcomd 2784 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆))) |
102 | 101 | fveq2d 6505 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(♯‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆)))) |
103 | 98, 102 | syl5eq 2826 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆)))) |
104 | | 1nn 11454 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ) |
106 | 62, 105 | syl5eqel 2870 |
. . . . . . . . . 10
⊢ (𝜑 →
(♯‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
107 | | lbfzo0 12895 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉)) ↔
(♯‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
108 | 106, 107 | sylibr 226 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉))) |
109 | | ccatval3 13745 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶 ∧ 0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉))) → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆))) =
(〈“(𝐾‘{𝑋})”〉‘0)) |
110 | 2, 58, 108, 109 | syl3anc 1351 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆))) =
(〈“(𝐾‘{𝑋})”〉‘0)) |
111 | | fvex 6514 |
. . . . . . . . 9
⊢ (𝐾‘{𝑋}) ∈ V |
112 | | s1fv 13776 |
. . . . . . . . 9
⊢ ((𝐾‘{𝑋}) ∈ V → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
113 | 111, 112 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
114 | 103, 110,
113 | 3eqtrd 2818 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋})) |
115 | 114 | opeq2d 4685 |
. . . . . 6
⊢ (𝜑 → 〈(♯‘𝑆), (𝑇‘(♯‘𝑆))〉 = 〈(♯‘𝑆), (𝐾‘{𝑋})〉) |
116 | 115 | sneqd 4454 |
. . . . 5
⊢ (𝜑 →
{〈(♯‘𝑆),
(𝑇‘(♯‘𝑆))〉} = {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) |
117 | 97, 116 | eqtrd 2814 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) |
118 | 89, 117 | breqtrrd 4958 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)})) |
119 | | pgpfac.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Abel) |
120 | | dprdsubg 18899 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺)) |
121 | 85, 120 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺)) |
122 | | dprdsubg 18899 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺)) |
123 | 118, 122 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺)) |
124 | 71, 119, 121, 123 | ablcntzd 18736 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})))) |
125 | | pgpfac.i |
. . . 4
⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
126 | 84 | oveq2d 6994 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆)) |
127 | | pgpfac.5 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) |
128 | 126, 127 | eqtrd 2814 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊) |
129 | 117 | oveq2d 6994 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
130 | 88 | simprd 488 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋})) |
131 | 129, 130 | eqtrd 2814 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋})) |
132 | 128, 131 | ineq12d 4079 |
. . . . 5
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋}))) |
133 | | incom 4068 |
. . . . 5
⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊) |
134 | 132, 133 | syl6eq 2830 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊)) |
135 | 4, 72 | subg0 18072 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
136 | 3, 135 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
137 | | pgpfac.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐻) |
138 | 136, 137 | syl6eqr 2832 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) = 0 ) |
139 | 138 | sneqd 4454 |
. . . 4
⊢ (𝜑 →
{(0g‘𝐺)} =
{ 0
}) |
140 | 125, 134,
139 | 3eqtr4d 2824 |
. . 3
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0g‘𝐺)}) |
141 | 48, 56, 70, 71, 72, 85, 118, 124, 140 | dmdprdsplit2 18921 |
. 2
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
142 | | eqid 2778 |
. . . . 5
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
143 | 48, 56, 70, 142, 141 | dprdsplit 18923 |
. . . 4
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})))) |
144 | 128, 131 | oveq12d 6996 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋}))) |
145 | 128, 121 | eqeltrrd 2867 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
146 | 142 | lsmcom 18737 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
147 | 119, 145,
21, 146 | syl3anc 1351 |
. . . 4
⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
148 | 143, 144,
147 | 3eqtrd 2818 |
. . 3
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
149 | | pgpfac.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) |
150 | 7 | subgss 18067 |
. . . . . 6
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻)) |
151 | 149, 150 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻)) |
152 | 151, 13 | sseqtr4d 3900 |
. . . 4
⊢ (𝜑 → 𝑊 ⊆ 𝑈) |
153 | | pgpfac.l |
. . . . 5
⊢ ⊕ =
(LSSum‘𝐻) |
154 | 4, 142, 153 | subglsm 18560 |
. . . 4
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
155 | 3, 23, 152, 154 | syl3anc 1351 |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
156 | | pgpfac.s |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
157 | 148, 155,
156 | 3eqtrd 2818 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈) |
158 | | breq2 4934 |
. . . 4
⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇)) |
159 | | oveq2 6986 |
. . . . 5
⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇)) |
160 | 159 | eqeq1d 2780 |
. . . 4
⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈)) |
161 | 158, 160 | anbi12d 621 |
. . 3
⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈))) |
162 | 161 | rspcev 3535 |
. 2
⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
163 | 43, 141, 157, 162 | syl12anc 824 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |