Step | Hyp | Ref
| Expression |
1 | | wrd0 14094 |
. . 3
⊢ ∅
∈ Word 𝐶 |
2 | | pgpfac.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Abel) |
3 | | ablgrp 19175 |
. . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
4 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | 4 | dprd0 19418 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
6 | 2, 3, 5 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
8 | | pgpfac.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
9 | 4 | subg0cl 18551 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑈) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐺) ∈ 𝑈) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) →
(0g‘𝐺)
∈ 𝑈) |
12 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s 𝑈) = (𝐺 ↾s 𝑈) |
13 | 12 | subgbas 18547 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
14 | 8, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
15 | 14 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
16 | 12 | subggrp 18546 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑈) ∈ Grp) |
17 | 8, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾s 𝑈) ∈ Grp) |
18 | | grpmnd 18372 |
. . . . . . . . . 10
⊢ ((𝐺 ↾s 𝑈) ∈ Grp → (𝐺 ↾s 𝑈) ∈ Mnd) |
19 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(𝐺
↾s 𝑈)) =
(Base‘(𝐺
↾s 𝑈)) |
20 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(gEx‘(𝐺
↾s 𝑈)) =
(gEx‘(𝐺
↾s 𝑈)) |
21 | 19, 20 | gex1 18980 |
. . . . . . . . . 10
⊢ ((𝐺 ↾s 𝑈) ∈ Mnd →
((gEx‘(𝐺
↾s 𝑈)) = 1
↔ (Base‘(𝐺
↾s 𝑈))
≈ 1o)) |
22 | 17, 18, 21 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ((gEx‘(𝐺 ↾s 𝑈)) = 1 ↔ (Base‘(𝐺 ↾s 𝑈)) ≈
1o)) |
23 | 22 | biimpa 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) →
(Base‘(𝐺
↾s 𝑈))
≈ 1o) |
24 | 15, 23 | eqbrtrd 5075 |
. . . . . . 7
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → 𝑈 ≈ 1o) |
25 | | en1eqsn 8904 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑈 ∧ 𝑈 ≈ 1o) → 𝑈 = {(0g‘𝐺)}) |
26 | 11, 24, 25 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → 𝑈 = {(0g‘𝐺)}) |
27 | 26 | eqeq2d 2748 |
. . . . 5
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → ((𝐺 DProd ∅) = 𝑈 ↔ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
28 | 27 | anbi2d 632 |
. . . 4
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → ((𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈) ↔ (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)}))) |
29 | 7, 28 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈)) |
30 | | breq2 5057 |
. . . . 5
⊢ (𝑠 = ∅ → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd ∅)) |
31 | | oveq2 7221 |
. . . . . 6
⊢ (𝑠 = ∅ → (𝐺 DProd 𝑠) = (𝐺 DProd ∅)) |
32 | 31 | eqeq1d 2739 |
. . . . 5
⊢ (𝑠 = ∅ → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd ∅) = 𝑈)) |
33 | 30, 32 | anbi12d 634 |
. . . 4
⊢ (𝑠 = ∅ → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈))) |
34 | 33 | rspcev 3537 |
. . 3
⊢ ((∅
∈ Word 𝐶 ∧ (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
35 | 1, 29, 34 | sylancr 590 |
. 2
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
36 | 12 | subgabl 19221 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝐺 ↾s 𝑈) ∈ Abel) |
37 | 2, 8, 36 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s 𝑈) ∈ Abel) |
38 | | pgpfac.f |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Fin) |
39 | | pgpfac.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
40 | 39 | subgss 18544 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵) |
41 | 8, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
42 | 38, 41 | ssfid 8898 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ Fin) |
43 | 14, 42 | eqeltrrd 2839 |
. . . . . 6
⊢ (𝜑 → (Base‘(𝐺 ↾s 𝑈)) ∈ Fin) |
44 | 19, 20 | gexcl2 18978 |
. . . . . 6
⊢ (((𝐺 ↾s 𝑈) ∈ Grp ∧
(Base‘(𝐺
↾s 𝑈))
∈ Fin) → (gEx‘(𝐺 ↾s 𝑈)) ∈ ℕ) |
45 | 17, 43, 44 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (gEx‘(𝐺 ↾s 𝑈)) ∈
ℕ) |
46 | | eqid 2737 |
. . . . . 6
⊢
(od‘(𝐺
↾s 𝑈)) =
(od‘(𝐺
↾s 𝑈)) |
47 | 19, 20, 46 | gexex 19238 |
. . . . 5
⊢ (((𝐺 ↾s 𝑈) ∈ Abel ∧
(gEx‘(𝐺
↾s 𝑈))
∈ ℕ) → ∃𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
48 | 37, 45, 47 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
49 | 48 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) → ∃𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
50 | | eqid 2737 |
. . . . 5
⊢
(mrCls‘(SubGrp‘(𝐺 ↾s 𝑈))) = (mrCls‘(SubGrp‘(𝐺 ↾s 𝑈))) |
51 | | eqid 2737 |
. . . . 5
⊢
((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) = ((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) |
52 | | eqid 2737 |
. . . . 5
⊢
(0g‘(𝐺 ↾s 𝑈)) = (0g‘(𝐺 ↾s 𝑈)) |
53 | | eqid 2737 |
. . . . 5
⊢
(LSSum‘(𝐺
↾s 𝑈)) =
(LSSum‘(𝐺
↾s 𝑈)) |
54 | | pgpfac.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
55 | | subgpgp 18986 |
. . . . . . 7
⊢ ((𝑃 pGrp 𝐺 ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑈)) |
56 | 54, 8, 55 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝑈)) |
57 | 56 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → 𝑃 pGrp (𝐺 ↾s 𝑈)) |
58 | 37 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → (𝐺 ↾s 𝑈) ∈ Abel) |
59 | 43 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → (Base‘(𝐺 ↾s 𝑈)) ∈ Fin) |
60 | | simprr 773 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
61 | | simprl 771 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → 𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))) |
62 | 50, 51, 19, 46, 20, 52, 53, 57, 58, 59, 60, 61 | pgpfac1 19467 |
. . . 4
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → ∃𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈))((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈)))) |
63 | | pgpfac.c |
. . . . 5
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
64 | 2 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝐺 ∈ Abel) |
65 | 54 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑃 pGrp 𝐺) |
66 | 38 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝐵 ∈ Fin) |
67 | 8 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑈 ∈ (SubGrp‘𝐺)) |
68 | | pgpfac.a |
. . . . . 6
⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
69 | 68 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
70 | | simpllr 776 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) |
71 | | simplrl 777 |
. . . . . 6
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))) |
72 | 67, 13 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
73 | 71, 72 | eleqtrrd 2841 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑥 ∈ 𝑈) |
74 | | simplrr 778 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
75 | | simprl 771 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈))) |
76 | | simprrl 781 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) →
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))}) |
77 | | simprrr 782 |
. . . . . 6
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) →
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))) |
78 | 77, 72 | eqtr4d 2780 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) →
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = 𝑈) |
79 | 39, 63, 64, 65, 66, 67, 69, 12, 50, 46, 20, 52, 53, 70, 73, 74, 75, 76, 78 | pgpfaclem2 19469 |
. . . 4
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
80 | 62, 79 | rexlimddv 3210 |
. . 3
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
81 | 49, 80 | rexlimddv 3210 |
. 2
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
82 | 35, 81 | pm2.61dane 3029 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |