Proof of Theorem pgpfaclem1
Step | Hyp | Ref
| Expression |
1 | | pgpfac.t |
. . 3
⊢ 𝑇 = (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) |
2 | | pgpfac.2 |
. . 3
⊢ (𝜑 → 𝑆 ∈ Word 𝐶) |
3 | | pgpfac.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
4 | | pgpfac.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝐺 ↾s 𝑈) |
5 | 4 | subggrp 18412 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
6 | 3, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ Grp) |
7 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝐻) =
(Base‘𝐻) |
8 | 7 | subgacs 18443 |
. . . . . . . . 9
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
9 | 6, 8 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
10 | 9 | acsmred 17042 |
. . . . . . 7
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(Moore‘(Base‘𝐻))) |
11 | | pgpfac.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
12 | 4 | subgbas 18413 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻)) |
13 | 3, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (Base‘𝐻)) |
14 | 11, 13 | eleqtrd 2836 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) |
15 | | pgpfac.k |
. . . . . . . 8
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐻)) |
16 | 15 | mrcsncl 16998 |
. . . . . . 7
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
17 | 10, 14, 16 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
18 | 4 | subsubg 18432 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
19 | 3, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))) |
20 | 17, 19 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)) |
21 | 20 | simpld 498 |
. . . 4
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) |
22 | 4 | oveq1i 7192 |
. . . . . . 7
⊢ (𝐻 ↾s (𝐾‘{𝑋})) = ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) |
23 | 20 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈) |
24 | | ressabs 16678 |
. . . . . . . 8
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
25 | 3, 23, 24 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ↾s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
26 | 22, 25 | syl5eq 2786 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) = (𝐺 ↾s (𝐾‘{𝑋}))) |
27 | 7, 15 | cycsubgcyg2 19153 |
. . . . . . 7
⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
28 | 6, 14, 27 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐻 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
29 | 26, 28 | eqeltrrd 2835 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp) |
30 | | pgpfac.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
31 | | pgpprm 18848 |
. . . . . . 7
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
33 | | subgpgp 18852 |
. . . . . . 7
⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
34 | 30, 21, 33 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) |
35 | | brelrng 5794 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾s (𝐾‘{𝑋}))) → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
36 | 32, 29, 34, 35 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ ran pGrp ) |
37 | 29, 36 | elind 4094 |
. . . 4
⊢ (𝜑 → (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
)) |
38 | | oveq2 7190 |
. . . . . 6
⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾s 𝑟) = (𝐺 ↾s (𝐾‘{𝑋}))) |
39 | 38 | eleq1d 2818 |
. . . . 5
⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔
(𝐺 ↾s
(𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
40 | | pgpfac.c |
. . . . 5
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
41 | 39, 40 | elrab2 3596 |
. . . 4
⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp
))) |
42 | 21, 37, 41 | sylanbrc 586 |
. . 3
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶) |
43 | 1, 2, 42 | cats1cld 14318 |
. 2
⊢ (𝜑 → 𝑇 ∈ Word 𝐶) |
44 | | wrdf 13972 |
. . . . 5
⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(♯‘𝑇))⟶𝐶) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶𝐶) |
46 | 40 | ssrab3 3981 |
. . . 4
⊢ 𝐶 ⊆ (SubGrp‘𝐺) |
47 | | fss 6531 |
. . . 4
⊢ ((𝑇:(0..^(♯‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺)) |
48 | 45, 46, 47 | sylancl 589 |
. . 3
⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺)) |
49 | | lencl 13986 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈
ℕ0) |
50 | 2, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑆) ∈
ℕ0) |
51 | 50 | nn0zd 12178 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑆) ∈
ℤ) |
52 | | fzosn 13211 |
. . . . . 6
⊢
((♯‘𝑆)
∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)}) |
53 | 51, 52 | syl 17 |
. . . . 5
⊢ (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)}) |
54 | 53 | ineq2d 4113 |
. . . 4
⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) =
((0..^(♯‘𝑆))
∩ {(♯‘𝑆)})) |
55 | | fzodisj 13174 |
. . . 4
⊢
((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅ |
56 | 54, 55 | eqtr3di 2789 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅) |
57 | 1 | fveq2i 6689 |
. . . . . . 7
⊢
(♯‘𝑇) =
(♯‘(𝑆 ++
〈“(𝐾‘{𝑋})”〉)) |
58 | 42 | s1cld 14058 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) |
59 | | ccatlen 14028 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶) → (♯‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉))) |
60 | 2, 58, 59 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝑆 ++ 〈“(𝐾‘{𝑋})”〉)) = ((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉))) |
61 | 57, 60 | syl5eq 2786 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉))) |
62 | | s1len 14061 |
. . . . . . 7
⊢
(♯‘〈“(𝐾‘{𝑋})”〉) = 1 |
63 | 62 | oveq2i 7193 |
. . . . . 6
⊢
((♯‘𝑆) +
(♯‘〈“(𝐾‘{𝑋})”〉)) = ((♯‘𝑆) + 1) |
64 | 61, 63 | eqtrdi 2790 |
. . . . 5
⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1)) |
65 | 64 | oveq2d 7198 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1))) |
66 | | nn0uz 12374 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
67 | 50, 66 | eleqtrdi 2844 |
. . . . 5
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘0)) |
68 | | fzosplitsn 13248 |
. . . . 5
⊢
((♯‘𝑆)
∈ (ℤ≥‘0) → (0..^((♯‘𝑆) + 1)) =
((0..^(♯‘𝑆))
∪ {(♯‘𝑆)})) |
69 | 67, 68 | syl 17 |
. . . 4
⊢ (𝜑 → (0..^((♯‘𝑆) + 1)) =
((0..^(♯‘𝑆))
∪ {(♯‘𝑆)})) |
70 | 65, 69 | eqtrd 2774 |
. . 3
⊢ (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})) |
71 | | eqid 2739 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
72 | | eqid 2739 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
73 | | pgpfac.4 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
74 | | cats1un 14184 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
75 | 2, 42, 74 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
76 | 1, 75 | syl5eq 2786 |
. . . . . 6
⊢ (𝜑 → 𝑇 = (𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
77 | 76 | reseq1d 5834 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(♯‘𝑆)))) |
78 | | wrdfn 13981 |
. . . . . . 7
⊢ (𝑆 ∈ Word 𝐶 → 𝑆 Fn (0..^(♯‘𝑆))) |
79 | 2, 78 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn (0..^(♯‘𝑆))) |
80 | | fzonel 13154 |
. . . . . 6
⊢ ¬
(♯‘𝑆) ∈
(0..^(♯‘𝑆)) |
81 | | fsnunres 6972 |
. . . . . 6
⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬
(♯‘𝑆) ∈
(0..^(♯‘𝑆)))
→ ((𝑆 ∪
{〈(♯‘𝑆),
(𝐾‘{𝑋})〉}) ↾ (0..^(♯‘𝑆))) = 𝑆) |
82 | 79, 80, 81 | sylancl 589 |
. . . . 5
⊢ (𝜑 → ((𝑆 ∪ {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) ↾ (0..^(♯‘𝑆))) = 𝑆) |
83 | 77, 82 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆) |
84 | 73, 83 | breqtrrd 5068 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆)))) |
85 | | fvex 6699 |
. . . . . 6
⊢
(♯‘𝑆)
∈ V |
86 | | dprdsn 19289 |
. . . . . 6
⊢
(((♯‘𝑆)
∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
87 | 85, 21, 86 | sylancr 590 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉} ∧ (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋}))) |
88 | 87 | simpld 498 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) |
89 | | wrdfn 13981 |
. . . . . . 7
⊢ (𝑇 ∈ Word 𝐶 → 𝑇 Fn (0..^(♯‘𝑇))) |
90 | 43, 89 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑇 Fn (0..^(♯‘𝑇))) |
91 | | ssun2 4073 |
. . . . . . . 8
⊢
{(♯‘𝑆)}
⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) |
92 | 85 | snss 4684 |
. . . . . . . 8
⊢
((♯‘𝑆)
∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) ↔ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})) |
93 | 91, 92 | mpbir 234 |
. . . . . . 7
⊢
(♯‘𝑆)
∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) |
94 | 93, 70 | eleqtrrid 2841 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑆) ∈
(0..^(♯‘𝑇))) |
95 | | fnressn 6942 |
. . . . . 6
⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈
(0..^(♯‘𝑇)))
→ (𝑇 ↾
{(♯‘𝑆)}) =
{〈(♯‘𝑆),
(𝑇‘(♯‘𝑆))〉}) |
96 | 90, 94, 95 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {〈(♯‘𝑆), (𝑇‘(♯‘𝑆))〉}) |
97 | 1 | fveq1i 6687 |
. . . . . . . . 9
⊢ (𝑇‘(♯‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(♯‘𝑆)) |
98 | 50 | nn0cnd 12050 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑆) ∈
ℂ) |
99 | 98 | addid2d 10931 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆)) |
100 | 99 | fveq2d 6690 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆))) =
((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(♯‘𝑆))) |
101 | 97, 100 | eqtr4id 2793 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆)))) |
102 | | 1nn 11739 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
103 | 62, 102 | eqeltri 2830 |
. . . . . . . . . . 11
⊢
(♯‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ |
104 | | lbfzo0 13180 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉)) ↔
(♯‘〈“(𝐾‘{𝑋})”〉) ∈
ℕ) |
105 | 103, 104 | mpbir 234 |
. . . . . . . . . 10
⊢ 0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉)) |
106 | 105 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉))) |
107 | | ccatval3 14034 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐶 ∧ 〈“(𝐾‘{𝑋})”〉 ∈ Word 𝐶 ∧ 0 ∈
(0..^(♯‘〈“(𝐾‘{𝑋})”〉))) → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆))) =
(〈“(𝐾‘{𝑋})”〉‘0)) |
108 | 2, 58, 106, 107 | syl3anc 1372 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 ++ 〈“(𝐾‘{𝑋})”〉)‘(0 +
(♯‘𝑆))) =
(〈“(𝐾‘{𝑋})”〉‘0)) |
109 | | fvex 6699 |
. . . . . . . . 9
⊢ (𝐾‘{𝑋}) ∈ V |
110 | | s1fv 14065 |
. . . . . . . . 9
⊢ ((𝐾‘{𝑋}) ∈ V → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
111 | 109, 110 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (〈“(𝐾‘{𝑋})”〉‘0) = (𝐾‘{𝑋})) |
112 | 101, 108,
111 | 3eqtrd 2778 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋})) |
113 | 112 | opeq2d 4778 |
. . . . . 6
⊢ (𝜑 → 〈(♯‘𝑆), (𝑇‘(♯‘𝑆))〉 = 〈(♯‘𝑆), (𝐾‘{𝑋})〉) |
114 | 113 | sneqd 4538 |
. . . . 5
⊢ (𝜑 →
{〈(♯‘𝑆),
(𝑇‘(♯‘𝑆))〉} = {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) |
115 | 96, 114 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) |
116 | 88, 115 | breqtrrd 5068 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)})) |
117 | | pgpfac.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Abel) |
118 | | dprdsubg 19277 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺)) |
119 | 84, 118 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺)) |
120 | | dprdsubg 19277 |
. . . . 5
⊢ (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺)) |
121 | 116, 120 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺)) |
122 | 71, 117, 119, 121 | ablcntzd 19108 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})))) |
123 | | pgpfac.i |
. . . 4
⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
124 | 83 | oveq2d 7198 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆)) |
125 | | pgpfac.5 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) |
126 | 124, 125 | eqtrd 2774 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊) |
127 | 115 | oveq2d 7198 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉})) |
128 | 87 | simprd 499 |
. . . . . . 7
⊢ (𝜑 → (𝐺 DProd {〈(♯‘𝑆), (𝐾‘{𝑋})〉}) = (𝐾‘{𝑋})) |
129 | 127, 128 | eqtrd 2774 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋})) |
130 | 126, 129 | ineq12d 4114 |
. . . . 5
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋}))) |
131 | | incom 4101 |
. . . . 5
⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊) |
132 | 130, 131 | eqtrdi 2790 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊)) |
133 | 4, 72 | subg0 18415 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
134 | 3, 133 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
135 | | pgpfac.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐻) |
136 | 134, 135 | eqtr4di 2792 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) = 0 ) |
137 | 136 | sneqd 4538 |
. . . 4
⊢ (𝜑 →
{(0g‘𝐺)} =
{ 0
}) |
138 | 123, 132,
137 | 3eqtr4d 2784 |
. . 3
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0g‘𝐺)}) |
139 | 48, 56, 70, 71, 72, 84, 116, 122, 138 | dmdprdsplit2 19299 |
. 2
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
140 | | eqid 2739 |
. . . . 5
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
141 | 48, 56, 70, 140, 139 | dprdsplit 19301 |
. . . 4
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})))) |
142 | 126, 129 | oveq12d 7200 |
. . . 4
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋}))) |
143 | 126, 119 | eqeltrrd 2835 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
144 | 140 | lsmcom 19109 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
145 | 117, 143,
21, 144 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
146 | 141, 142,
145 | 3eqtrd 2778 |
. . 3
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊)) |
147 | | pgpfac.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) |
148 | 7 | subgss 18410 |
. . . . . 6
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻)) |
149 | 147, 148 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻)) |
150 | 149, 13 | sseqtrrd 3928 |
. . . 4
⊢ (𝜑 → 𝑊 ⊆ 𝑈) |
151 | | pgpfac.l |
. . . . 5
⊢ ⊕ =
(LSSum‘𝐻) |
152 | 4, 140, 151 | subglsm 18929 |
. . . 4
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
153 | 3, 23, 150, 152 | syl3anc 1372 |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊)) |
154 | | pgpfac.s |
. . 3
⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
155 | 146, 153,
154 | 3eqtrd 2778 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈) |
156 | | breq2 5044 |
. . . 4
⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇)) |
157 | | oveq2 7190 |
. . . . 5
⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇)) |
158 | 157 | eqeq1d 2741 |
. . . 4
⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈)) |
159 | 156, 158 | anbi12d 634 |
. . 3
⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈))) |
160 | 159 | rspcev 3529 |
. 2
⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
161 | 43, 139, 155, 160 | syl12anc 836 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |