Step | Hyp | Ref
| Expression |
1 | | wrd0 13185 |
. . 3
⊢ ∅
∈ Word 𝐶 |
2 | | pgpfac.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Abel) |
3 | | ablgrp 18021 |
. . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
4 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | 4 | dprd0 18253 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
6 | 2, 3, 5 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
8 | | pgpfac.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
9 | 4 | subg0cl 17425 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑈) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐺) ∈ 𝑈) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) →
(0g‘𝐺)
∈ 𝑈) |
12 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s 𝑈) = (𝐺 ↾s 𝑈) |
13 | 12 | subgbas 17421 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
14 | 8, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → 𝑈 = (Base‘(𝐺 ↾s 𝑈))) |
16 | 12 | subggrp 17420 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑈) ∈ Grp) |
17 | 8, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾s 𝑈) ∈ Grp) |
18 | | grpmnd 17252 |
. . . . . . . . . 10
⊢ ((𝐺 ↾s 𝑈) ∈ Grp → (𝐺 ↾s 𝑈) ∈ Mnd) |
19 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘(𝐺
↾s 𝑈)) =
(Base‘(𝐺
↾s 𝑈)) |
20 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(gEx‘(𝐺
↾s 𝑈)) =
(gEx‘(𝐺
↾s 𝑈)) |
21 | 19, 20 | gex1 17829 |
. . . . . . . . . 10
⊢ ((𝐺 ↾s 𝑈) ∈ Mnd →
((gEx‘(𝐺
↾s 𝑈)) = 1
↔ (Base‘(𝐺
↾s 𝑈))
≈ 1𝑜)) |
22 | 17, 18, 21 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ((gEx‘(𝐺 ↾s 𝑈)) = 1 ↔ (Base‘(𝐺 ↾s 𝑈)) ≈
1𝑜)) |
23 | 22 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) →
(Base‘(𝐺
↾s 𝑈))
≈ 1𝑜) |
24 | 15, 23 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → 𝑈 ≈
1𝑜) |
25 | | en1eqsn 8075 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑈 ∧ 𝑈 ≈ 1𝑜) → 𝑈 = {(0g‘𝐺)}) |
26 | 11, 24, 25 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → 𝑈 = {(0g‘𝐺)}) |
27 | 26 | eqeq2d 2620 |
. . . . 5
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → ((𝐺 DProd ∅) = 𝑈 ↔ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
28 | 27 | anbi2d 736 |
. . . 4
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → ((𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈) ↔ (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)}))) |
29 | 7, 28 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈)) |
30 | | breq2 4587 |
. . . . 5
⊢ (𝑠 = ∅ → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd ∅)) |
31 | | oveq2 6557 |
. . . . . 6
⊢ (𝑠 = ∅ → (𝐺 DProd 𝑠) = (𝐺 DProd ∅)) |
32 | 31 | eqeq1d 2612 |
. . . . 5
⊢ (𝑠 = ∅ → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd ∅) = 𝑈)) |
33 | 30, 32 | anbi12d 743 |
. . . 4
⊢ (𝑠 = ∅ → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈))) |
34 | 33 | rspcev 3282 |
. . 3
⊢ ((∅
∈ Word 𝐶 ∧ (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
35 | 1, 29, 34 | sylancr 694 |
. 2
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) = 1) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
36 | 12 | subgabl 18064 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝐺 ↾s 𝑈) ∈ Abel) |
37 | 2, 8, 36 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s 𝑈) ∈ Abel) |
38 | | pgpfac.f |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Fin) |
39 | | pgpfac.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
40 | 39 | subgss 17418 |
. . . . . . . . 9
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵) |
41 | 8, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
42 | | ssfi 8065 |
. . . . . . . 8
⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin) |
43 | 38, 41, 42 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ Fin) |
44 | 14, 43 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (Base‘(𝐺 ↾s 𝑈)) ∈ Fin) |
45 | 19, 20 | gexcl2 17827 |
. . . . . 6
⊢ (((𝐺 ↾s 𝑈) ∈ Grp ∧
(Base‘(𝐺
↾s 𝑈))
∈ Fin) → (gEx‘(𝐺 ↾s 𝑈)) ∈ ℕ) |
46 | 17, 44, 45 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (gEx‘(𝐺 ↾s 𝑈)) ∈
ℕ) |
47 | | eqid 2610 |
. . . . . 6
⊢
(od‘(𝐺
↾s 𝑈)) =
(od‘(𝐺
↾s 𝑈)) |
48 | 19, 20, 47 | gexex 18079 |
. . . . 5
⊢ (((𝐺 ↾s 𝑈) ∈ Abel ∧
(gEx‘(𝐺
↾s 𝑈))
∈ ℕ) → ∃𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
49 | 37, 46, 48 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
50 | 49 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) → ∃𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
51 | | eqid 2610 |
. . . . 5
⊢
(mrCls‘(SubGrp‘(𝐺 ↾s 𝑈))) = (mrCls‘(SubGrp‘(𝐺 ↾s 𝑈))) |
52 | | eqid 2610 |
. . . . 5
⊢
((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) = ((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) |
53 | | eqid 2610 |
. . . . 5
⊢
(0g‘(𝐺 ↾s 𝑈)) = (0g‘(𝐺 ↾s 𝑈)) |
54 | | eqid 2610 |
. . . . 5
⊢
(LSSum‘(𝐺
↾s 𝑈)) =
(LSSum‘(𝐺
↾s 𝑈)) |
55 | | pgpfac.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
56 | | subgpgp 17835 |
. . . . . . 7
⊢ ((𝑃 pGrp 𝐺 ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑈)) |
57 | 55, 8, 56 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝑈)) |
58 | 57 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → 𝑃 pGrp (𝐺 ↾s 𝑈)) |
59 | 37 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → (𝐺 ↾s 𝑈) ∈ Abel) |
60 | 44 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → (Base‘(𝐺 ↾s 𝑈)) ∈ Fin) |
61 | | simprr 792 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈))) |
62 | | simprl 790 |
. . . . 5
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → 𝑥 ∈ (Base‘(𝐺 ↾s 𝑈))) |
63 | 51, 52, 19, 47, 20, 53, 54, 58, 59, 60, 61, 62 | pgpfac1 18302 |
. . . 4
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → ∃𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈))((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈)))) |
64 | | pgpfac.c |
. . . . 5
⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp
)} |
65 | 2 | ad3antrrr 762 |
. . . . 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) |
66 | 55 | ad3antrrr 762 |
. . . . 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 𝐺) |
67 | 38 | ad3antrrr 762 |
. . . . 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) |
68 | 8 | ad3antrrr 762 |
. . . . 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‘𝐺)) |
69 | | pgpfac.a |
. . . . . 6
⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) |
70 | 69 | ad3antrrr 762 |
. . . . 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 𝑠) = 𝑡))) |
71 | | simpllr 795 |
. . . . 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) |
72 | | simplrl 796 |
. . . . . 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 | 68, 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 𝑈))) |
74 | 72, 73 | eleqtrrd 2691 |
. . . . 5
⊢ ((((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) ∧ (𝑤 ∈ (SubGrp‘(𝐺 ↾s 𝑈)) ∧
((((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥}) ∩ 𝑤) = {(0g‘(𝐺 ↾s 𝑈))} ∧
(((mrCls‘(SubGrp‘(𝐺 ↾s 𝑈)))‘{𝑥})(LSSum‘(𝐺 ↾s 𝑈))𝑤) = (Base‘(𝐺 ↾s 𝑈))))) → 𝑥 ∈ 𝑈) |
75 | | simplrr 797 |
. . . . 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 𝑈))) |
76 | | simprl 790 |
. . . . 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 𝑈))) |
77 | | simprrl 800 |
. . . . 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 𝑈))}) |
78 | | simprrr 801 |
. . . . . 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 𝑈))) |
79 | 78, 73 | eqtr4d 2647 |
. . . . 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 𝑈))𝑤) = 𝑈) |
80 | 39, 64, 65, 66, 67, 68, 70, 12, 51, 47, 20, 53, 54, 71, 74, 75, 76, 77, 79 | pgpfaclem2 18304 |
. . . 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 𝑠) = 𝑈)) |
81 | 63, 80 | rexlimddv 3017 |
. . 3
⊢ (((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) ∧ (𝑥 ∈ (Base‘(𝐺 ↾s 𝑈)) ∧ ((od‘(𝐺 ↾s 𝑈))‘𝑥) = (gEx‘(𝐺 ↾s 𝑈)))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
82 | 50, 81 | rexlimddv 3017 |
. 2
⊢ ((𝜑 ∧ (gEx‘(𝐺 ↾s 𝑈)) ≠ 1) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |
83 | 35, 82 | pm2.61dane 2869 |
1
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) |