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 17644 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Grp) |
7 | | eqid 2651 |
. . . . . . . . 9
⊢
(Base‘𝐻) =
(Base‘𝐻) |
8 | 7 | subgacs 17676 |
. . . . . . . 8
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
9 | | acsmre 16360 |
. . . . . . . 8
⊢
((SubGrp‘𝐻)
∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) |
10 | 6, 8, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(Moore‘(Base‘𝐻))) |
11 | | pgpfac.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
12 | 4 | subgbas 17645 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻)) |
13 | 3, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (Base‘𝐻)) |
14 | 11, 13 | eleqtrd 2732 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) |
15 | | pgpfac.k |
. . . . . . . 8
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐻)) |
16 | 15 | mrcsncl 16319 |
. . . . . . 7
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
17 | 10, 14, 16 | syl2anc 694 |
. . . . . 6
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
18 | 4 | subsubg 17664 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
19 | 3, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
20 | 17, 19 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)) |
21 | 20 | simpld 474 |
. . . 4
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) |
22 | 4 | oveq1i 6700 |
. . . . . . 7
⊢ (𝐻 ↾s (𝐾‘{𝑋})) = ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) |
23 | 20 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈) |
24 | | ressabs 15986 |
. . . . . . . 8
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
25 | 3, 23, 24 | syl2anc 694 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
26 | 22, 25 | syl5eq 2697 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
27 | 7, 15 | cycsubgcyg2 18349 |
. . . . . . 7
⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
28 | 6, 14, 27 | syl2anc 694 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
29 | 26, 28 | eqeltrrd 2731 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
30 | | pgpfac.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
31 | | pgpprm 18054 |
. . . . . . 7
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
33 | | subgpgp 18058 |
. . . . . . 7
⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
34 | 30, 21, 33 | syl2anc 694 |
. . . . . 6
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
35 | | brelrng 5387 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
36 | 32, 29, 34, 35 | syl3anc 1366 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
37 | 29, 36 | elind 3831 |
. . . 4
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
)) |
38 | | oveq2 6698 |
. . . . . 6
⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾s 𝑟) = (𝐺 ↾s (𝐾‘{𝑋}))) |
39 | 38 | eleq1d 2715 |
. . . . 5
⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔
(𝐺 ↾s
(𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
40 | | pgpfac.c |
. . . . 5
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
41 | 39, 40 | elrab2 3399 |
. . . 4
⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
42 | 21, 37, 41 | sylanbrc 699 |
. . 3
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶) |
43 | 1, 2, 42 | cats1cld 13646 |
. 2
⊢ (𝜑 → 𝑇 ∈ Word 𝐶) |
44 | | wrdf 13342 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(#‘𝑇))⟶𝐶) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇:(0..^(#‘𝑇))⟶𝐶) |
46 | | ssrab2 3720 |
. . . . 5
⊢ {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆
(SubGrp‘𝐺) |
47 | 40, 46 | eqsstri 3668 |
. . . 4
⊢ 𝐶 ⊆ (SubGrp‘𝐺) |
48 | | fss 6094 |
. . . 4
⊢ ((𝑇:(0..^(#‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(#‘𝑇))⟶(SubGrp‘𝐺)) |
49 | 45, 47, 48 | sylancl 695 |
. . 3
⊢ (𝜑 → 𝑇:(0..^(#‘𝑇))⟶(SubGrp‘𝐺)) |
50 | | fzodisj 12541 |
. . . 4
⊢
((0..^(#‘𝑆))
∩ ((#‘𝑆)..^((#‘𝑆) + 1))) = ∅ |
51 | | lencl 13356 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐶 → (#‘𝑆) ∈
ℕ0) |
52 | 2, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑆) ∈
ℕ0) |
53 | 52 | nn0zd 11518 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) ∈ ℤ) |
54 | | fzosn 12578 |
. . . . . 6
⊢
((#‘𝑆) ∈
ℤ → ((#‘𝑆)..^((#‘𝑆) + 1)) = {(#‘𝑆)}) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ((#‘𝑆)..^((#‘𝑆) + 1)) = {(#‘𝑆)}) |
56 | 55 | ineq2d 3847 |
. . . 4
⊢ (𝜑 → ((0..^(#‘𝑆)) ∩ ((#‘𝑆)..^((#‘𝑆) + 1))) = ((0..^(#‘𝑆)) ∩ {(#‘𝑆)})) |
57 | 50, 56 | syl5reqr 2700 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝑆)) ∩ {(#‘𝑆)}) = ∅) |
58 | 1 | fveq2i 6232 |
. . . . . . 7
⊢
(#‘𝑇) =
(#‘(𝑆 ++
〈“(𝐾‘{𝑋})”〉)) |
59 | 42 | s1cld 13419 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) |
60 | | ccatlen 13393 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) → (#‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((#‘𝑆) + (#‘〈“(𝐾‘{𝑋})”〉))) |
61 | 2, 59, 60 | syl2anc 694 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((#‘𝑆) + (#‘〈“(𝐾‘{𝑋})”〉))) |
62 | 58, 61 | syl5eq 2697 |
. . . . . 6
⊢ (𝜑 → (#‘𝑇) = ((#‘𝑆) + (#‘〈“(𝐾‘{𝑋})”〉))) |
63 | | s1len 13422 |
. . . . . . 7
⊢
(#‘〈“(𝐾‘{𝑋})”〉) = 1 |
64 | 63 | oveq2i 6701 |
. . . . . 6
⊢
((#‘𝑆) +
(#‘〈“(𝐾‘{𝑋})”〉)) = ((#‘𝑆) + 1) |
65 | 62, 64 | syl6eq 2701 |
. . . . 5
⊢ (𝜑 → (#‘𝑇) = ((#‘𝑆) + 1)) |
66 | 65 | oveq2d 6706 |
. . . 4
⊢ (𝜑 → (0..^(#‘𝑇)) = (0..^((#‘𝑆) + 1))) |
67 | | nn0uz 11760 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
68 | 52, 67 | syl6eleq 2740 |
. . . . 5
⊢ (𝜑 → (#‘𝑆) ∈
(ℤ≥‘0)) |
69 | | fzosplitsn 12616 |
. . . . 5
⊢
((#‘𝑆) ∈
(ℤ≥‘0) → (0..^((#‘𝑆) + 1)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})) |
70 | 68, 69 | syl 17 |
. . . 4
⊢ (𝜑 → (0..^((#‘𝑆) + 1)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})) |
71 | 66, 70 | eqtrd 2685 |
. . 3
⊢ (𝜑 → (0..^(#‘𝑇)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})) |
72 | | eqid 2651 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
73 | | eqid 2651 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
74 | | pgpfac.4 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
75 | | cats1un 13521 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
76 | 2, 42, 75 | syl2anc 694 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
77 | 1, 76 | syl5eq 2697 |
. . . . . 6
⊢ (𝜑 → 𝑇 = (𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
78 | 77 | reseq1d 5427 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ (0..^(#‘𝑆))) = ((𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(#‘𝑆)))) |
79 | | wrdf 13342 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐶 → 𝑆:(0..^(#‘𝑆))⟶𝐶) |
80 | | ffn 6083 |
. . . . . . 7
⊢ (𝑆:(0..^(#‘𝑆))⟶𝐶 → 𝑆 Fn (0..^(#‘𝑆))) |
81 | 2, 79, 80 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn (0..^(#‘𝑆))) |
82 | | fzonel 12522 |
. . . . . 6
⊢ ¬
(#‘𝑆) ∈
(0..^(#‘𝑆)) |
83 | | fsnunres 6495 |
. . . . . 6
⊢ ((𝑆 Fn (0..^(#‘𝑆)) ∧ ¬ (#‘𝑆) ∈ (0..^(#‘𝑆))) → ((𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(#‘𝑆))) = 𝑆) |
84 | 81, 82, 83 | sylancl 695 |
. . . . 5
⊢ (𝜑 → ((𝑆 ∪ {〈(#‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(#‘𝑆))) = 𝑆) |
85 | 78, 84 | eqtrd 2685 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ (0..^(#‘𝑆))) = 𝑆) |
86 | 74, 85 | breqtrrd 4713 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(#‘𝑆)))) |
87 | | fvex 6239 |
. . . . . 6
⊢
(#‘𝑆) ∈
V |
88 | | dprdsn 18481 |
. . . . . 6
⊢
(((#‘𝑆) ∈
V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
89 | 87, 21, 88 | sylancr 696 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
90 | 89 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) |
91 | | ffn 6083 |
. . . . . . 7
⊢ (𝑇:(0..^(#‘𝑇))⟶𝐶 → 𝑇 Fn (0..^(#‘𝑇))) |
92 | 43, 44, 91 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑇 Fn (0..^(#‘𝑇))) |
93 | | ssun2 3810 |
. . . . . . . 8
⊢
{(#‘𝑆)}
⊆ ((0..^(#‘𝑆))
∪ {(#‘𝑆)}) |
94 | 87 | snss 4348 |
. . . . . . . 8
⊢
((#‘𝑆) ∈
((0..^(#‘𝑆)) ∪
{(#‘𝑆)}) ↔
{(#‘𝑆)} ⊆
((0..^(#‘𝑆)) ∪
{(#‘𝑆)})) |
95 | 93, 94 | mpbir 221 |
. . . . . . 7
⊢
(#‘𝑆) ∈
((0..^(#‘𝑆)) ∪
{(#‘𝑆)}) |
96 | 95, 71 | syl5eleqr 2737 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) ∈ (0..^(#‘𝑇))) |
97 | | fnressn 6465 |
. . . . . 6
⊢ ((𝑇 Fn (0..^(#‘𝑇)) ∧ (#‘𝑆) ∈ (0..^(#‘𝑇))) → (𝑇 ↾ {(#‘𝑆)}) = {〈(#‘𝑆), (𝑇‘(#‘𝑆))〉}) |
98 | 92, 96, 97 | syl2anc 694 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ {(#‘𝑆)}) = {〈(#‘𝑆), (𝑇‘(#‘𝑆))〉}) |
99 | 1 | fveq1i 6230 |
. . . . . . . . 9
⊢ (𝑇‘(#‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(#‘𝑆)) |
100 | 52 | nn0cnd 11391 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘𝑆) ∈ ℂ) |
101 | 100 | addid2d 10275 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 + (#‘𝑆)) = (#‘𝑆)) |
102 | 101 | eqcomd 2657 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝑆) = (0 + (#‘𝑆))) |
103 | 102 | fveq2d 6233 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(#‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆)))) |
104 | 99, 103 | syl5eq 2697 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘(#‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆)))) |
105 | | 1nn 11069 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
106 | 105 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ) |
107 | 63, 106 | syl5eqel 2734 |
. . . . . . . . . 10
⊢ (𝜑 →
(#‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
108 | | lbfzo0 12547 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^(#‘〈“(𝐾‘{𝑋})”〉)) ↔
(#‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
109 | 107, 108 | sylibr 224 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0..^(#‘〈“(𝐾‘{𝑋})”〉))) |
110 | | ccatval3 13397 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶 ∧ 0 ∈
(0..^(#‘〈“(𝐾‘{𝑋})”〉))) → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆))) = (〈“(𝐾‘{𝑋})”〉‘0)) |
111 | 2, 59, 109, 110 | syl3anc 1366 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 + (#‘𝑆))) = (〈“(𝐾‘{𝑋})”〉‘0)) |
112 | | fvex 6239 |
. . . . . . . . 9
⊢ (𝐾‘{𝑋}) ∈ V |
113 | | s1fv 13427 |
. . . . . . . . 9
⊢ ((𝐾‘{𝑋}) ∈ V → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
114 | 112, 113 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
115 | 104, 111,
114 | 3eqtrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘(#‘𝑆)) = (𝐾‘{𝑋})) |
116 | 115 | opeq2d 4440 |
. . . . . 6
⊢ (𝜑 → 〈(#‘𝑆), (𝑇‘(#‘𝑆))〉 = 〈(#‘𝑆), (𝐾‘{𝑋})〉) |
117 | 116 | sneqd 4222 |
. . . . 5
⊢ (𝜑 → {〈(#‘𝑆), (𝑇‘(#‘𝑆))〉} = {〈(#‘𝑆), (𝐾‘{𝑋})〉}) |
118 | 98, 117 | eqtrd 2685 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ {(#‘𝑆)}) = {〈(#‘𝑆), (𝐾‘{𝑋})〉}) |
119 | 90, 118 | breqtrrd 4713 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(#‘𝑆)})) |
120 | | pgpfac.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Abel) |
121 | | dprdsubg 18469 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ (0..^(#‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∈ (SubGrp‘𝐺)) |
122 | 86, 121 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∈ (SubGrp‘𝐺)) |
123 | | dprdsubg 18469 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ {(#‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) ∈ (SubGrp‘𝐺)) |
124 | 119, 123 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) ∈ (SubGrp‘𝐺)) |
125 | 72, 120, 122, 124 | ablcntzd 18306 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(#‘𝑆)})))) |
126 | | pgpfac.i |
. . . 4
⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
127 | 85 | oveq2d 6706 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) = (𝐺 DProd 𝑆)) |
128 | | pgpfac.5 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) |
129 | 127, 128 | eqtrd 2685 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) = 𝑊) |
130 | 118 | oveq2d 6706 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) = (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉})) |
131 | 89 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd {〈(#‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋})) |
132 | 130, 131 | eqtrd 2685 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) = (𝐾‘{𝑋})) |
133 | 129, 132 | ineq12d 3848 |
. . . . 5
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋}))) |
134 | | incom 3838 |
. . . . 5
⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊) |
135 | 133, 134 | syl6eq 2701 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊)) |
136 | 4, 73 | subg0 17647 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
137 | 3, 136 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
138 | | pgpfac.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐻) |
139 | 137, 138 | syl6eqr 2703 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) = 0 ) |
140 | 139 | sneqd 4222 |
. . . 4
⊢ (𝜑 →
{(0g‘𝐺)} =
{ 0
}) |
141 | 126, 135,
140 | 3eqtr4d 2695 |
. . 3
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = {(0g‘𝐺)}) |
142 | 49, 57, 71, 72, 73, 86, 119, 125, 141 | dmdprdsplit2 18491 |
. 2
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
143 | | eqid 2651 |
. . . . 5
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
144 | 49, 57, 71, 143, 142 | dprdsplit 18493 |
. . . 4
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(#‘𝑆)})))) |
145 | 129, 132 | oveq12d 6708 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋}))) |
146 | 129, 122 | eqeltrrd 2731 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
147 | 143 | lsmcom 18307 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
148 | 120, 146,
21, 147 | syl3anc 1366 |
. . . 4
⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
149 | 144, 145,
148 | 3eqtrd 2689 |
. . 3
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
150 | | pgpfac.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) |
151 | 7 | subgss 17642 |
. . . . . 6
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻)) |
152 | 150, 151 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻)) |
153 | 152, 13 | sseqtr4d 3675 |
. . . 4
⊢ (𝜑 → 𝑊 ⊆ 𝑈) |
154 | | pgpfac.l |
. . . . 5
⊢ ⊕ =
(LSSum‘𝐻) |
155 | 4, 143, 154 | subglsm 18132 |
. . . 4
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
156 | 3, 23, 153, 155 | syl3anc 1366 |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
157 | | pgpfac.s |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
158 | 149, 156,
157 | 3eqtrd 2689 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈) |
159 | | breq2 4689 |
. . . 4
⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇)) |
160 | | oveq2 6698 |
. . . . 5
⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇)) |
161 | 160 | eqeq1d 2653 |
. . . 4
⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈)) |
162 | 159, 161 | anbi12d 747 |
. . 3
⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈))) |
163 | 162 | rspcev 3340 |
. 2
⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
164 | 43, 142, 158, 163 | syl12anc 1364 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |