| Step | Hyp | Ref
| Expression |
| 1 | | pgpfac.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) |
| 2 | | pgpfac.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
| 3 | | pgpfac.h |
. . . . . . . . 9
⊢ 𝐻 = (𝐺 ↾s 𝑈) |
| 4 | 3 | subsubg 19167 |
. . . . . . . 8
⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈))) |
| 5 | 2, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈))) |
| 6 | 1, 5 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈)) |
| 7 | 6 | simprd 495 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ 𝑈) |
| 8 | | pgpfac.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 9 | | pgpfac.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐺) |
| 10 | 9 | subgss 19145 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵) |
| 11 | 2, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
| 12 | 8, 11 | ssfid 9301 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ Fin) |
| 13 | 12, 7 | ssfid 9301 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Fin) |
| 14 | | hashcl 14395 |
. . . . . . . . 9
⊢ (𝑊 ∈ Fin →
(♯‘𝑊) ∈
ℕ0) |
| 15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
| 16 | 15 | nn0red 12588 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ) |
| 17 | | pgpfac.0 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐻) |
| 18 | 17 | fvexi 6920 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
| 19 | | hashsng 14408 |
. . . . . . . . . . 11
⊢ ( 0 ∈ V
→ (♯‘{ 0 }) = 1) |
| 20 | 18, 19 | ax-mp 5 |
. . . . . . . . . 10
⊢
(♯‘{ 0 }) = 1 |
| 21 | | subgrcl 19149 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp) |
| 22 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 23 | 22 | subgacs 19179 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) |
| 24 | | acsmre 17695 |
. . . . . . . . . . . . . . . 16
⊢
((SubGrp‘𝐻)
∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) |
| 25 | 1, 21, 23, 24 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (SubGrp‘𝐻) ∈
(Moore‘(Base‘𝐻))) |
| 26 | | pgpfac.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐻)) |
| 27 | 25, 26 | mrcssvd 17666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ (Base‘𝐻)) |
| 28 | 3 | subgbas 19148 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻)) |
| 29 | 2, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 = (Base‘𝐻)) |
| 30 | 27, 29 | sseqtrrd 4021 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈) |
| 31 | 12, 30 | ssfid 9301 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ Fin) |
| 32 | | pgpfac.x |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
| 33 | 32, 29 | eleqtrd 2843 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) |
| 34 | 26 | mrcsncl 17655 |
. . . . . . . . . . . . . . . 16
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
| 35 | 25, 33, 34 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻)) |
| 36 | 17 | subg0cl 19152 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) → 0 ∈ (𝐾‘{𝑋})) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ (𝐾‘{𝑋})) |
| 38 | 37 | snssd 4809 |
. . . . . . . . . . . . 13
⊢ (𝜑 → { 0 } ⊆ (𝐾‘{𝑋})) |
| 39 | 33 | snssd 4809 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑋} ⊆ (Base‘𝐻)) |
| 40 | 25, 26, 39 | mrcssidd 17668 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋})) |
| 41 | | snssg 4783 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝑈 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋}))) |
| 42 | 32, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋}))) |
| 43 | 40, 42 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ (𝐾‘{𝑋})) |
| 44 | | pgpfac.oe |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) |
| 45 | | pgpfac.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ≠ 1) |
| 46 | 44, 45 | eqnetrd 3008 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘𝑋) ≠ 1) |
| 47 | | pgpfac.o |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑂 = (od‘𝐻) |
| 48 | 47, 17 | od1 19577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ Grp → (𝑂‘ 0 ) = 1) |
| 49 | 1, 21, 48 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑂‘ 0 ) = 1) |
| 50 | | elsni 4643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ { 0 } → 𝑋 = 0 ) |
| 51 | 50 | fveqeq2d 6914 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ { 0 } → ((𝑂‘𝑋) = 1 ↔ (𝑂‘ 0 ) = 1)) |
| 52 | 49, 51 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∈ { 0 } → (𝑂‘𝑋) = 1)) |
| 53 | 52 | necon3ad 2953 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑂‘𝑋) ≠ 1 → ¬ 𝑋 ∈ { 0 })) |
| 54 | 46, 53 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ { 0 }) |
| 55 | 38, 43, 54 | ssnelpssd 4115 |
. . . . . . . . . . . 12
⊢ (𝜑 → { 0 } ⊊ (𝐾‘{𝑋})) |
| 56 | | php3 9249 |
. . . . . . . . . . . 12
⊢ (((𝐾‘{𝑋}) ∈ Fin ∧ { 0 } ⊊ (𝐾‘{𝑋})) → { 0 } ≺ (𝐾‘{𝑋})) |
| 57 | 31, 55, 56 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → { 0 } ≺ (𝐾‘{𝑋})) |
| 58 | | snfi 9083 |
. . . . . . . . . . . 12
⊢ { 0 } ∈
Fin |
| 59 | | hashsdom 14420 |
. . . . . . . . . . . 12
⊢ (({ 0 } ∈ Fin
∧ (𝐾‘{𝑋}) ∈ Fin) →
((♯‘{ 0 }) <
(♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋}))) |
| 60 | 58, 31, 59 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘{ 0 }) <
(♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋}))) |
| 61 | 57, 60 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘{ 0 }) <
(♯‘(𝐾‘{𝑋}))) |
| 62 | 20, 61 | eqbrtrrid 5179 |
. . . . . . . . 9
⊢ (𝜑 → 1 <
(♯‘(𝐾‘{𝑋}))) |
| 63 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
| 64 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ ((𝐾‘{𝑋}) ∈ Fin → (♯‘(𝐾‘{𝑋})) ∈
ℕ0) |
| 65 | 31, 64 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈
ℕ0) |
| 66 | 65 | nn0red 12588 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℝ) |
| 67 | 17 | subg0cl 19152 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ (SubGrp‘𝐻) → 0 ∈ 𝑊) |
| 68 | | ne0i 4341 |
. . . . . . . . . . . . 13
⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅) |
| 69 | 1, 67, 68 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ≠ ∅) |
| 70 | | hashnncl 14405 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Fin →
((♯‘𝑊) ∈
ℕ ↔ 𝑊 ≠
∅)) |
| 71 | 13, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅)) |
| 72 | 69, 71 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ) |
| 73 | 72 | nngt0d 12315 |
. . . . . . . . . 10
⊢ (𝜑 → 0 <
(♯‘𝑊)) |
| 74 | | ltmul1 12117 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (♯‘(𝐾‘{𝑋})) ∈ ℝ ∧
((♯‘𝑊) ∈
ℝ ∧ 0 < (♯‘𝑊))) → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))) |
| 75 | 63, 66, 16, 73, 74 | syl112anc 1376 |
. . . . . . . . 9
⊢ (𝜑 → (1 <
(♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))) |
| 76 | 62, 75 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (1 ·
(♯‘𝑊)) <
((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))) |
| 77 | 16 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℂ) |
| 78 | 77 | mullidd 11279 |
. . . . . . . 8
⊢ (𝜑 → (1 ·
(♯‘𝑊)) =
(♯‘𝑊)) |
| 79 | | pgpfac.l |
. . . . . . . . . 10
⊢ ⊕ =
(LSSum‘𝐻) |
| 80 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Cntz‘𝐻) =
(Cntz‘𝐻) |
| 81 | | pgpfac.i |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
| 82 | | pgpfac.g |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ Abel) |
| 83 | 3 | subgabl 19854 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) |
| 84 | 82, 2, 83 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ Abel) |
| 85 | 80, 84, 35, 1 | ablcntzd 19875 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ ((Cntz‘𝐻)‘𝑊)) |
| 86 | 79, 17, 80, 35, 1, 81, 85, 31, 13 | lsmhash 19723 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))) |
| 87 | | pgpfac.s |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
| 88 | 87 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = (♯‘𝑈)) |
| 89 | 86, 88 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)) = (♯‘𝑈)) |
| 90 | 76, 78, 89 | 3brtr3d 5174 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) < (♯‘𝑈)) |
| 91 | 16, 90 | ltned 11397 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑊) ≠ (♯‘𝑈)) |
| 92 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑊 = 𝑈 → (♯‘𝑊) = (♯‘𝑈)) |
| 93 | 92 | necon3i 2973 |
. . . . . 6
⊢
((♯‘𝑊)
≠ (♯‘𝑈)
→ 𝑊 ≠ 𝑈) |
| 94 | 91, 93 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ≠ 𝑈) |
| 95 | | df-pss 3971 |
. . . . 5
⊢ (𝑊 ⊊ 𝑈 ↔ (𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈)) |
| 96 | 7, 94, 95 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝑊 ⊊ 𝑈) |
| 97 | | psseq1 4090 |
. . . . . 6
⊢ (𝑡 = 𝑊 → (𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈)) |
| 98 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑡 = 𝑊 → ((𝐺 DProd 𝑠) = 𝑡 ↔ (𝐺 DProd 𝑠) = 𝑊)) |
| 99 | 98 | anbi2d 630 |
. . . . . . 7
⊢ (𝑡 = 𝑊 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))) |
| 100 | 99 | rexbidv 3179 |
. . . . . 6
⊢ (𝑡 = 𝑊 → (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))) |
| 101 | 97, 100 | imbi12d 344 |
. . . . 5
⊢ (𝑡 = 𝑊 → ((𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)) ↔ (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))) |
| 102 | | pgpfac.a |
. . . . 5
⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
| 103 | 6 | simpld 494 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
| 104 | 101, 102,
103 | rspcdva 3623 |
. . . 4
⊢ (𝜑 → (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))) |
| 105 | 96, 104 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)) |
| 106 | | breq2 5147 |
. . . . 5
⊢ (𝑠 = 𝑎 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑎)) |
| 107 | | oveq2 7439 |
. . . . . 6
⊢ (𝑠 = 𝑎 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑎)) |
| 108 | 107 | eqeq1d 2739 |
. . . . 5
⊢ (𝑠 = 𝑎 → ((𝐺 DProd 𝑠) = 𝑊 ↔ (𝐺 DProd 𝑎) = 𝑊)) |
| 109 | 106, 108 | anbi12d 632 |
. . . 4
⊢ (𝑠 = 𝑎 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) |
| 110 | 109 | cbvrexvw 3238 |
. . 3
⊢
(∃𝑠 ∈
Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)) |
| 111 | 105, 110 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)) |
| 112 | | pgpfac.c |
. . 3
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
| 113 | 82 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺 ∈ Abel) |
| 114 | | pgpfac.p |
. . . 4
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
| 115 | 114 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑃 pGrp 𝐺) |
| 116 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐵 ∈ Fin) |
| 117 | 2 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑈 ∈ (SubGrp‘𝐺)) |
| 118 | 102 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
| 119 | | pgpfac.e |
. . 3
⊢ 𝐸 = (gEx‘𝐻) |
| 120 | 45 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐸 ≠ 1) |
| 121 | 32 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑋 ∈ 𝑈) |
| 122 | 44 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝑂‘𝑋) = 𝐸) |
| 123 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑊 ∈ (SubGrp‘𝐻)) |
| 124 | 81 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) |
| 125 | 87 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) |
| 126 | | simprl 771 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑎 ∈ Word 𝐶) |
| 127 | | simprrl 781 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺dom DProd 𝑎) |
| 128 | | simprrr 782 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝐺 DProd 𝑎) = 𝑊) |
| 129 | | eqid 2737 |
. . 3
⊢ (𝑎 ++ 〈“(𝐾‘{𝑋})”〉) = (𝑎 ++ 〈“(𝐾‘{𝑋})”〉) |
| 130 | 9, 112, 113, 115, 116, 117, 118, 3, 26, 47, 119, 17, 79, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129 | pgpfaclem1 20101 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
| 131 | 111, 130 | rexlimddv 3161 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |