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 17420 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Grp) |
7 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐻) =
(Base‘𝐻) |
8 | 7 | subgacs 17452 |
. . . . . . . 8
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
9 | | acsmre 16136 |
. . . . . . . 8
⊢
((SubGrp‘𝐻)
∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) |
10 | 6, 8, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(Moore‘(Base‘𝐻))) |
11 | | pgpfac.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
12 | 4 | subgbas 17421 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻)) |
13 | 3, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (Base‘𝐻)) |
14 | 11, 13 | eleqtrd 2690 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) |
15 | | pgpfac.k |
. . . . . . . 8
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐻)) |
16 | 15 | mrcsncl 16095 |
. . . . . . 7
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
17 | 10, 14, 16 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
18 | 4 | subsubg 17440 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
19 | 3, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
20 | 17, 19 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)) |
21 | 20 | simpld 474 |
. . . 4
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) |
22 | 4 | oveq1i 6559 |
. . . . . . 7
⊢ (𝐻 ↾s (𝐾‘{𝑋})) = ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) |
23 | 20 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈) |
24 | | ressabs 15766 |
. . . . . . . 8
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
25 | 3, 23, 24 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
26 | 22, 25 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
27 | 7, 15 | cycsubgcyg2 18126 |
. . . . . . 7
⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
28 | 6, 14, 27 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
29 | 26, 28 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
30 | | pgpfac.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
31 | | pgpprm 17831 |
. . . . . . 7
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
33 | | subgpgp 17835 |
. . . . . . 7
⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
34 | 30, 21, 33 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
35 | | brelrng 5276 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
36 | 32, 29, 34, 35 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
37 | 29, 36 | elind 3760 |
. . . 4
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
)) |
38 | | oveq2 6557 |
. . . . . 6
⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾s 𝑟) = (𝐺 ↾s (𝐾‘{𝑋}))) |
39 | 38 | eleq1d 2672 |
. . . . 5
⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔
(𝐺 ↾s
(𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
40 | | pgpfac.c |
. . . . 5
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
41 | 39, 40 | elrab2 3333 |
. . . 4
⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
42 | 21, 37, 41 | sylanbrc 695 |
. . 3
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶) |
43 | 1, 2, 42 | cats1cld 13451 |
. 2
⊢ (𝜑 → 𝑇 ∈ Word 𝐶) |
44 | | wrdf 13165 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(#‘𝑇))⟶𝐶) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇:(0..^(#‘𝑇))⟶𝐶) |
46 | | ssrab2 3650 |
. . . . 5
⊢ {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
(SubGrp‘𝐺) |
47 | 40, 46 | eqsstri 3598 |
. . . 4
⊢ 𝐶 ⊆ (SubGrp‘𝐺) |
48 | | fss 5969 |
. . . 4
⊢ ((𝑇:(0..^(#‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(#‘𝑇))⟶(SubGrp‘𝐺)) |
49 | 45, 47, 48 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝑇:(0..^(#‘𝑇))⟶(SubGrp‘𝐺)) |
50 | | fzodisj 12371 |
. . . 4
⊢
((0..^(#‘𝑆))
∩ ((#‘𝑆)..^((#‘𝑆) + 1))) = ∅ |
51 | | lencl 13179 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐶 → (#‘𝑆) ∈
ℕ0) |
52 | 2, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑆) ∈
ℕ0) |
53 | 52 | nn0zd 11356 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) ∈ ℤ) |
54 | | fzosn 12405 |
. . . . . 6
⊢
((#‘𝑆) ∈
ℤ → ((#‘𝑆)..^((#‘𝑆) + 1)) = {(#‘𝑆)}) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ((#‘𝑆)..^((#‘𝑆) + 1)) = {(#‘𝑆)}) |
56 | 55 | ineq2d 3776 |
. . . 4
⊢ (𝜑 → ((0..^(#‘𝑆)) ∩ ((#‘𝑆)..^((#‘𝑆) + 1))) = ((0..^(#‘𝑆)) ∩ {(#‘𝑆)})) |
57 | 50, 56 | syl5reqr 2659 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝑆)) ∩ {(#‘𝑆)}) = ∅) |
58 | 1 | fveq2i 6106 |
. . . . . . 7
⊢
(#‘𝑇) =
(#‘(𝑆 ++
〈“(𝐾‘{𝑋})”〉)) |
59 | 42 | s1cld 13236 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) |
60 | | ccatlen 13213 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) → (#‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((#‘𝑆) + (#‘〈“(𝐾‘{𝑋})”〉))) |
61 | 2, 59, 60 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((#‘𝑆) + (#‘〈“(𝐾‘{𝑋})”〉))) |
62 | 58, 61 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → (#‘𝑇) = ((#‘𝑆) + (#‘〈“(𝐾‘{𝑋})”〉))) |
63 | | s1len 13238 |
. . . . . . 7
⊢
(#‘〈“(𝐾‘{𝑋})”〉) = 1 |
64 | 63 | oveq2i 6560 |
. . . . . 6
⊢
((#‘𝑆) +
(#‘〈“(𝐾‘{𝑋})”〉)) = ((#‘𝑆) + 1) |
65 | 62, 64 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → (#‘𝑇) = ((#‘𝑆) + 1)) |
66 | 65 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (0..^(#‘𝑇)) = (0..^((#‘𝑆) + 1))) |
67 | | nn0uz 11598 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
68 | 52, 67 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → (#‘𝑆) ∈
(ℤ≥‘0)) |
69 | | fzosplitsn 12442 |
. . . . 5
⊢
((#‘𝑆) ∈
(ℤ≥‘0) → (0..^((#‘𝑆) + 1)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})) |
70 | 68, 69 | syl 17 |
. . . 4
⊢ (𝜑 → (0..^((#‘𝑆) + 1)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})) |
71 | 66, 70 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (0..^(#‘𝑇)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})) |
72 | | eqid 2610 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
73 | | eqid 2610 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
74 | | pgpfac.4 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
75 | | cats1un 13327 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
76 | 2, 42, 75 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
77 | 1, 76 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → 𝑇 = (𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
78 | 77 | reseq1d 5316 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ (0..^(#‘𝑆))) = ((𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(#‘𝑆)))) |
79 | | wrdf 13165 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐶 → 𝑆:(0..^(#‘𝑆))⟶𝐶) |
80 | | ffn 5958 |
. . . . . . 7
⊢ (𝑆:(0..^(#‘𝑆))⟶𝐶 → 𝑆 Fn (0..^(#‘𝑆))) |
81 | 2, 79, 80 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn (0..^(#‘𝑆))) |
82 | | fzonel 12352 |
. . . . . 6
⊢ ¬
(#‘𝑆) ∈
(0..^(#‘𝑆)) |
83 | | fsnunres 6359 |
. . . . . 6
⊢ ((𝑆 Fn (0..^(#‘𝑆)) ∧ ¬ (#‘𝑆) ∈ (0..^(#‘𝑆))) → ((𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(#‘𝑆))) = 𝑆) |
84 | 81, 82, 83 | sylancl 693 |
. . . . 5
⊢ (𝜑 → ((𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(#‘𝑆))) = 𝑆) |
85 | 78, 84 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ (0..^(#‘𝑆))) = 𝑆) |
86 | 74, 85 | breqtrrd 4611 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(#‘𝑆)))) |
87 | | fvex 6113 |
. . . . . 6
⊢
(#‘𝑆) ∈
V |
88 | | dprdsn 18258 |
. . . . . 6
⊢
(((#‘𝑆) ∈
V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
89 | 87, 21, 88 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
90 | 89 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) |
91 | | ffn 5958 |
. . . . . . 7
⊢ (𝑇:(0..^(#‘𝑇))⟶𝐶 → 𝑇 Fn (0..^(#‘𝑇))) |
92 | 43, 44, 91 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑇 Fn (0..^(#‘𝑇))) |
93 | | ssun2 3739 |
. . . . . . . 8
⊢
{(#‘𝑆)}
⊆ ((0..^(#‘𝑆))
∪ {(#‘𝑆)}) |
94 | 87 | snss 4259 |
. . . . . . . 8
⊢
((#‘𝑆) ∈
((0..^(#‘𝑆)) ∪
{(#‘𝑆)}) ↔
{(#‘𝑆)} ⊆
((0..^(#‘𝑆)) ∪
{(#‘𝑆)})) |
95 | 93, 94 | mpbir 220 |
. . . . . . 7
⊢
(#‘𝑆) ∈
((0..^(#‘𝑆)) ∪
{(#‘𝑆)}) |
96 | 95, 71 | syl5eleqr 2695 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) ∈ (0..^(#‘𝑇))) |
97 | | fnressn 6330 |
. . . . . 6
⊢ ((𝑇 Fn (0..^(#‘𝑇)) ∧ (#‘𝑆) ∈ (0..^(#‘𝑇))) → (𝑇 ↾ {(#‘𝑆)}) = {〈(#‘𝑆), (𝑇‘(#‘𝑆))〉}) |
98 | 92, 96, 97 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ {(#‘𝑆)}) = {〈(#‘𝑆), (𝑇‘(#‘𝑆))〉}) |
99 | 1 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝑇‘(#‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(#‘𝑆)) |
100 | 52 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘𝑆) ∈ ℂ) |
101 | 100 | addid2d 10116 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 + (#‘𝑆)) = (#‘𝑆)) |
102 | 101 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝑆) = (0 + (#‘𝑆))) |
103 | 102 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(#‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆)))) |
104 | 99, 103 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘(#‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆)))) |
105 | | 1nn 10908 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
106 | 105 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ) |
107 | 63, 106 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝜑 →
(#‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
108 | | lbfzo0 12375 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^(#‘〈“(𝐾‘{𝑋})”〉)) ↔
(#‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
109 | 107, 108 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0..^(#‘〈“(𝐾‘{𝑋})”〉))) |
110 | | ccatval3 13216 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶 ∧ 0 ∈
(0..^(#‘〈“(𝐾‘{𝑋})”〉))) → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆))) = (〈“(𝐾‘{𝑋})”〉‘0)) |
111 | 2, 59, 109, 110 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆))) = (〈“(𝐾‘{𝑋})”〉‘0)) |
112 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐾‘{𝑋}) ∈ V |
113 | | s1fv 13243 |
. . . . . . . . 9
⊢ ((𝐾‘{𝑋}) ∈ V → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
114 | 112, 113 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
115 | 104, 111,
114 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘(#‘𝑆)) = (𝐾‘{𝑋})) |
116 | 115 | opeq2d 4347 |
. . . . . 6
⊢ (𝜑 → 〈(#‘𝑆), (𝑇‘(#‘𝑆))〉 = 〈(#‘𝑆), (𝐾‘{𝑋})〉) |
117 | 116 | sneqd 4137 |
. . . . 5
⊢ (𝜑 → {〈(#‘𝑆), (𝑇‘(#‘𝑆))〉} = {〈(#‘𝑆), (𝐾‘{𝑋})〉}) |
118 | 98, 117 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ {(#‘𝑆)}) = {〈(#‘𝑆), (𝐾‘{𝑋})〉}) |
119 | 90, 118 | breqtrrd 4611 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(#‘𝑆)})) |
120 | | pgpfac.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Abel) |
121 | | dprdsubg 18246 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ (0..^(#‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∈ (SubGrp‘𝐺)) |
122 | 86, 121 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∈ (SubGrp‘𝐺)) |
123 | | dprdsubg 18246 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ {(#‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) ∈ (SubGrp‘𝐺)) |
124 | 119, 123 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) ∈ (SubGrp‘𝐺)) |
125 | 72, 120, 122, 124 | ablcntzd 18083 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(#‘𝑆)})))) |
126 | | pgpfac.i |
. . . 4
⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
127 | 85 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) = (𝐺 DProd 𝑆)) |
128 | | pgpfac.5 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) |
129 | 127, 128 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) = 𝑊) |
130 | 118 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) = (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
131 | 89 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋})) |
132 | 130, 131 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) = (𝐾‘{𝑋})) |
133 | 129, 132 | ineq12d 3777 |
. . . . 5
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋}))) |
134 | | incom 3767 |
. . . . 5
⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊) |
135 | 133, 134 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊)) |
136 | 4, 73 | subg0 17423 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
137 | 3, 136 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
138 | | pgpfac.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐻) |
139 | 137, 138 | syl6eqr 2662 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) = 0 ) |
140 | 139 | sneqd 4137 |
. . . 4
⊢ (𝜑 →
{(0g‘𝐺)} =
{ 0
}) |
141 | 126, 135,
140 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = {(0g‘𝐺)}) |
142 | 49, 57, 71, 72, 73, 86, 119, 125, 141 | dmdprdsplit2 18268 |
. 2
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
143 | | eqid 2610 |
. . . . 5
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
144 | 49, 57, 71, 143, 142 | dprdsplit 18270 |
. . . 4
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(#‘𝑆)})))) |
145 | 129, 132 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋}))) |
146 | 129, 122 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
147 | 143 | lsmcom 18084 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
148 | 120, 146,
21, 147 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
149 | 144, 145,
148 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
150 | | pgpfac.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) |
151 | 7 | subgss 17418 |
. . . . . 6
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻)) |
152 | 150, 151 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻)) |
153 | 152, 13 | sseqtr4d 3605 |
. . . 4
⊢ (𝜑 → 𝑊 ⊆ 𝑈) |
154 | | pgpfac.l |
. . . . 5
⊢ ⊕ =
(LSSum‘𝐻) |
155 | 4, 143, 154 | subglsm 17909 |
. . . 4
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
156 | 3, 23, 153, 155 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
157 | | pgpfac.s |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
158 | 149, 156,
157 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈) |
159 | | breq2 4587 |
. . . 4
⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇)) |
160 | | oveq2 6557 |
. . . . 5
⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇)) |
161 | 160 | eqeq1d 2612 |
. . . 4
⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈)) |
162 | 159, 161 | anbi12d 743 |
. . 3
⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈))) |
163 | 162 | rspcev 3282 |
. 2
⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
164 | 43, 142, 158, 163 | syl12anc 1316 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |