Step | Hyp | Ref
| Expression |
1 | | pgpfac.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) |
2 | | pgpfac.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
3 | | pgpfac.h |
. . . . . . . 8
⊢ 𝐻 = (𝐺 ↾s 𝑈) |
4 | 3 | subsubg 17440 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈))) |
5 | 2, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈))) |
6 | 1, 5 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈)) |
7 | 6 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
8 | | pgpfac.a |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
9 | 6 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ 𝑈) |
10 | | pgpfac.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ Fin) |
11 | | pgpfac.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐺) |
12 | 11 | subgss 17418 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵) |
13 | 2, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
14 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin) |
15 | 10, 13, 14 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ Fin) |
16 | | ssfi 8065 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Fin ∧ 𝑊 ⊆ 𝑈) → 𝑊 ∈ Fin) |
17 | 15, 9, 16 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Fin) |
18 | | hashcl 13009 |
. . . . . . . . 9
⊢ (𝑊 ∈ Fin →
(#‘𝑊) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑊) ∈
ℕ0) |
20 | 19 | nn0red 11229 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑊) ∈ ℝ) |
21 | | pgpfac.0 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐻) |
22 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘𝐻) ∈ V |
23 | 21, 22 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
24 | | hashsng 13020 |
. . . . . . . . . . 11
⊢ ( 0 ∈ V
→ (#‘{ 0 }) = 1) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . 10
⊢
(#‘{ 0 }) = 1 |
26 | | subgrcl 17422 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp) |
27 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐻) =
(Base‘𝐻) |
28 | 27 | subgacs 17452 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
29 | | acsmre 16136 |
. . . . . . . . . . . . . . . 16
⊢
((SubGrp‘𝐻)
∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) |
30 | 1, 26, 28, 29 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(Moore‘(Base‘𝐻))) |
31 | | pgpfac.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐻)) |
32 | 30, 31 | mrcssvd 16106 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ (Base‘𝐻)) |
33 | 3 | subgbas 17421 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻)) |
34 | 2, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 = (Base‘𝐻)) |
35 | 32, 34 | sseqtr4d 3605 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈) |
36 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Fin ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → (𝐾‘{𝑋}) ∈ Fin) |
37 | 15, 35, 36 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ Fin) |
38 | | pgpfac.x |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
39 | 38, 34 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) |
40 | 31 | mrcsncl 16095 |
. . . . . . . . . . . . . . . 16
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
41 | 30, 39, 40 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
42 | 21 | subg0cl 17425 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) → 0 ∈ (𝐾‘{𝑋})) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ (𝐾‘{𝑋})) |
44 | 43 | snssd 4281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → { 0 } ⊆ (𝐾‘{𝑋})) |
45 | 39 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑋} ⊆ (Base‘𝐻)) |
46 | 30, 31, 45 | mrcssidd 16108 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋})) |
47 | | snssg 4268 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝑈 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋}))) |
48 | 38, 47 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋}))) |
49 | 46, 48 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ (𝐾‘{𝑋})) |
50 | | pgpfac.oe |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) |
51 | | pgpfac.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ≠ 1) |
52 | 50, 51 | eqnetrd 2849 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘𝑋) ≠ 1) |
53 | | pgpfac.o |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑂 = (od‘𝐻) |
54 | 53, 21 | od1 17799 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ Grp → (𝑂‘ 0 ) = 1) |
55 | 1, 26, 54 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑂‘ 0 ) = 1) |
56 | | elsni 4142 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ { 0 } → 𝑋 = 0 ) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ { 0 } → (𝑂‘𝑋) = (𝑂‘ 0 )) |
58 | 57 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ { 0 } → ((𝑂‘𝑋) = 1 ↔ (𝑂‘ 0 ) = 1)) |
59 | 55, 58 | syl5ibrcom 236 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∈ { 0 } → (𝑂‘𝑋) = 1)) |
60 | 59 | necon3ad 2795 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑂‘𝑋) ≠ 1 → ¬ 𝑋 ∈ { 0 })) |
61 | 52, 60 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ { 0 }) |
62 | 44, 49, 61 | ssnelpssd 3681 |
. . . . . . . . . . . 12
⊢ (𝜑 → { 0 } ⊊ (𝐾‘{𝑋})) |
63 | | php3 8031 |
. . . . . . . . . . . 12
⊢ (((𝐾‘{𝑋}) ∈ Fin ∧ { 0 } ⊊ (𝐾‘{𝑋})) → { 0 } ≺ (𝐾‘{𝑋})) |
64 | 37, 62, 63 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → { 0 } ≺ (𝐾‘{𝑋})) |
65 | | snfi 7923 |
. . . . . . . . . . . 12
⊢ { 0 } ∈
Fin |
66 | | hashsdom 13031 |
. . . . . . . . . . . 12
⊢ (({ 0 } ∈ Fin
∧ (𝐾‘{𝑋}) ∈ Fin) →
((#‘{ 0 }) < (#‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋}))) |
67 | 65, 37, 66 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘{ 0 }) <
(#‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋}))) |
68 | 64, 67 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘{ 0 }) <
(#‘(𝐾‘{𝑋}))) |
69 | 25, 68 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ (𝜑 → 1 < (#‘(𝐾‘{𝑋}))) |
70 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
71 | | hashcl 13009 |
. . . . . . . . . . . 12
⊢ ((𝐾‘{𝑋}) ∈ Fin → (#‘(𝐾‘{𝑋})) ∈
ℕ0) |
72 | 37, 71 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐾‘{𝑋})) ∈
ℕ0) |
73 | 72 | nn0red 11229 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝐾‘{𝑋})) ∈ ℝ) |
74 | 21 | subg0cl 17425 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 0 ∈ 𝑊) |
75 | | ne0i 3880 |
. . . . . . . . . . . . 13
⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅) |
76 | 1, 74, 75 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ≠ ∅) |
77 | | hashnncl 13018 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Fin →
((#‘𝑊) ∈ ℕ
↔ 𝑊 ≠
∅)) |
78 | 17, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅)) |
79 | 76, 78 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝑊) ∈ ℕ) |
80 | 79 | nngt0d 10941 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (#‘𝑊)) |
81 | | ltmul1 10752 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (#‘(𝐾‘{𝑋})) ∈ ℝ ∧ ((#‘𝑊) ∈ ℝ ∧ 0 <
(#‘𝑊))) → (1
< (#‘(𝐾‘{𝑋})) ↔ (1 · (#‘𝑊)) < ((#‘(𝐾‘{𝑋})) · (#‘𝑊)))) |
82 | 70, 73, 20, 80, 81 | syl112anc 1322 |
. . . . . . . . 9
⊢ (𝜑 → (1 < (#‘(𝐾‘{𝑋})) ↔ (1 · (#‘𝑊)) < ((#‘(𝐾‘{𝑋})) · (#‘𝑊)))) |
83 | 69, 82 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (1 · (#‘𝑊)) < ((#‘(𝐾‘{𝑋})) · (#‘𝑊))) |
84 | 20 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑊) ∈ ℂ) |
85 | 84 | mulid2d 9937 |
. . . . . . . 8
⊢ (𝜑 → (1 · (#‘𝑊)) = (#‘𝑊)) |
86 | | pgpfac.l |
. . . . . . . . . 10
⊢ ⊕ =
(LSSum‘𝐻) |
87 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Cntz‘𝐻) =
(Cntz‘𝐻) |
88 | | pgpfac.i |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
89 | | pgpfac.g |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ Abel) |
90 | 3 | subgabl 18064 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) |
91 | 89, 2, 90 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ Abel) |
92 | 87, 91, 41, 1 | ablcntzd 18083 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ ((Cntz‘𝐻)‘𝑊)) |
93 | 86, 21, 87, 41, 1, 88, 92, 37, 17 | lsmhash 17941 |
. . . . . . . . 9
⊢ (𝜑 → (#‘((𝐾‘{𝑋}) ⊕ 𝑊)) = ((#‘(𝐾‘{𝑋})) · (#‘𝑊))) |
94 | | pgpfac.s |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
95 | 94 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (#‘((𝐾‘{𝑋}) ⊕ 𝑊)) = (#‘𝑈)) |
96 | 93, 95 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → ((#‘(𝐾‘{𝑋})) · (#‘𝑊)) = (#‘𝑈)) |
97 | 83, 85, 96 | 3brtr3d 4614 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑊) < (#‘𝑈)) |
98 | 20, 97 | ltned 10052 |
. . . . . 6
⊢ (𝜑 → (#‘𝑊) ≠ (#‘𝑈)) |
99 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑊 = 𝑈 → (#‘𝑊) = (#‘𝑈)) |
100 | 99 | necon3i 2814 |
. . . . . 6
⊢
((#‘𝑊) ≠
(#‘𝑈) → 𝑊 ≠ 𝑈) |
101 | 98, 100 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ≠ 𝑈) |
102 | | df-pss 3556 |
. . . . 5
⊢ (𝑊 ⊊ 𝑈 ↔ (𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈)) |
103 | 9, 101, 102 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 𝑊 ⊊ 𝑈) |
104 | | psseq1 3656 |
. . . . . 6
⊢ (𝑡 = 𝑊 → (𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈)) |
105 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑡 = 𝑊 → ((𝐺 DProd 𝑠) = 𝑡 ↔ (𝐺 DProd 𝑠) = 𝑊)) |
106 | 105 | anbi2d 736 |
. . . . . . 7
⊢ (𝑡 = 𝑊 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))) |
107 | 106 | rexbidv 3034 |
. . . . . 6
⊢ (𝑡 = 𝑊 → (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))) |
108 | 104, 107 | imbi12d 333 |
. . . . 5
⊢ (𝑡 = 𝑊 → ((𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)) ↔ (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))) |
109 | 108 | rspcv 3278 |
. . . 4
⊢ (𝑊 ∈ (SubGrp‘𝐺) → (∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)) → (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))) |
110 | 7, 8, 103, 109 | syl3c 64 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)) |
111 | | breq2 4587 |
. . . . 5
⊢ (𝑠 = 𝑎 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑎)) |
112 | | oveq2 6557 |
. . . . . 6
⊢ (𝑠 = 𝑎 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑎)) |
113 | 112 | eqeq1d 2612 |
. . . . 5
⊢ (𝑠 = 𝑎 → ((𝐺 DProd 𝑠) = 𝑊 ↔ (𝐺 DProd 𝑎) = 𝑊)) |
114 | 111, 113 | anbi12d 743 |
. . . 4
⊢ (𝑠 = 𝑎 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) |
115 | 114 | cbvrexv 3148 |
. . 3
⊢
(∃𝑠 ∈
Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)) |
116 | 110, 115 | sylib 207 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)) |
117 | | pgpfac.c |
. . 3
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
118 | 89 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺 ∈ Abel) |
119 | | pgpfac.p |
. . . 4
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
120 | 119 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑃 pGrp 𝐺) |
121 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐵 ∈ Fin) |
122 | 2 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑈 ∈ (SubGrp‘𝐺)) |
123 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
124 | | pgpfac.e |
. . 3
⊢ 𝐸 = (gEx‘𝐻) |
125 | 51 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐸 ≠ 1) |
126 | 38 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑋 ∈ 𝑈) |
127 | 50 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝑂‘𝑋) = 𝐸) |
128 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑊 ∈ (SubGrp‘𝐻)) |
129 | 88 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
130 | 94 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
131 | | simprl 790 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑎 ∈ Word 𝐶) |
132 | | simprrl 800 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺dom DProd 𝑎) |
133 | | simprrr 801 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝐺 DProd 𝑎) = 𝑊) |
134 | | eqid 2610 |
. . 3
⊢ (𝑎 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑎 ++ 〈“(𝐾‘{𝑋})”〉) |
135 | 11, 117, 118, 120, 121, 122, 123, 3, 31, 53, 124, 21, 86, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134 | pgpfaclem1 18303 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
136 | 116, 135 | rexlimddv 3017 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |