Proof of Theorem pgpfac1lem1
Step | Hyp | Ref
| Expression |
1 | | pgpfac1.ss |
. . . 4
⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝑆 ⊕ 𝑊) ⊆ 𝑈) |
3 | | pgpfac1.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Abel) |
4 | | ablgrp 18198 |
. . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
5 | | pgpfac1.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
6 | 5 | subgacs 17629 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘𝐵)) |
7 | | acsmre 16313 |
. . . . . 6
⊢
((SubGrp‘𝐺)
∈ (ACS‘𝐵) →
(SubGrp‘𝐺) ∈
(Moore‘𝐵)) |
8 | 3, 4, 6, 7 | 4syl 19 |
. . . . 5
⊢ (𝜑 → (SubGrp‘𝐺) ∈ (Moore‘𝐵)) |
9 | 8 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (SubGrp‘𝐺) ∈ (Moore‘𝐵)) |
10 | | eldifi 3732 |
. . . . . 6
⊢ (𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊)) → 𝐶 ∈ 𝑈) |
11 | 10 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐶 ∈ 𝑈) |
12 | 11 | snssd 4340 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → {𝐶} ⊆ 𝑈) |
13 | | pgpfac1.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
14 | 13 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝑈 ∈ (SubGrp‘𝐺)) |
15 | | pgpfac1.k |
. . . . 5
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
16 | 15 | mrcsscl 16280 |
. . . 4
⊢
(((SubGrp‘𝐺)
∈ (Moore‘𝐵)
∧ {𝐶} ⊆ 𝑈 ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝐾‘{𝐶}) ⊆ 𝑈) |
17 | 9, 12, 14, 16 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝐾‘{𝐶}) ⊆ 𝑈) |
18 | | pgpfac1.s |
. . . . . . 7
⊢ 𝑆 = (𝐾‘{𝐴}) |
19 | 5 | subgss 17595 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵) |
20 | 13, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
21 | | pgpfac1.au |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
22 | 20, 21 | sseldd 3604 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
23 | 15 | mrcsncl 16272 |
. . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘𝐵)
∧ 𝐴 ∈ 𝐵) → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺)) |
24 | 8, 22, 23 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺)) |
25 | 18, 24 | syl5eqel 2705 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
26 | | pgpfac1.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) |
27 | | pgpfac1.l |
. . . . . . 7
⊢ ⊕ =
(LSSum‘𝐺) |
28 | 27 | lsmsubg2 18262 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑊 ∈ (SubGrp‘𝐺)) → (𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺)) |
29 | 3, 25, 26, 28 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺)) |
30 | 29 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺)) |
31 | 20 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑈) → 𝐶 ∈ 𝐵) |
32 | 10, 31 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐶 ∈ 𝐵) |
33 | 15 | mrcsncl 16272 |
. . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘𝐵)
∧ 𝐶 ∈ 𝐵) → (𝐾‘{𝐶}) ∈ (SubGrp‘𝐺)) |
34 | 9, 32, 33 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝐾‘{𝐶}) ∈ (SubGrp‘𝐺)) |
35 | 27 | lsmlub 18078 |
. . . 4
⊢ (((𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝐶}) ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (((𝑆 ⊕ 𝑊) ⊆ 𝑈 ∧ (𝐾‘{𝐶}) ⊆ 𝑈) ↔ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊆ 𝑈)) |
36 | 30, 34, 14, 35 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (((𝑆 ⊕ 𝑊) ⊆ 𝑈 ∧ (𝐾‘{𝐶}) ⊆ 𝑈) ↔ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊆ 𝑈)) |
37 | 2, 17, 36 | mpbi2and 956 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊆ 𝑈) |
38 | 27 | lsmub1 18071 |
. . . . . 6
⊢ (((𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝐶}) ∈ (SubGrp‘𝐺)) → (𝑆 ⊕ 𝑊) ⊆ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
39 | 30, 34, 38 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝑆 ⊕ 𝑊) ⊆ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
40 | 27 | lsmub2 18072 |
. . . . . . 7
⊢ (((𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝐶}) ∈ (SubGrp‘𝐺)) → (𝐾‘{𝐶}) ⊆ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
41 | 30, 34, 40 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝐾‘{𝐶}) ⊆ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
42 | 32 | snssd 4340 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → {𝐶} ⊆ 𝐵) |
43 | 9, 15, 42 | mrcssidd 16285 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → {𝐶} ⊆ (𝐾‘{𝐶})) |
44 | | snssg 4327 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐵 → (𝐶 ∈ (𝐾‘{𝐶}) ↔ {𝐶} ⊆ (𝐾‘{𝐶}))) |
45 | 32, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝐶 ∈ (𝐾‘{𝐶}) ↔ {𝐶} ⊆ (𝐾‘{𝐶}))) |
46 | 43, 45 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐶 ∈ (𝐾‘{𝐶})) |
47 | 41, 46 | sseldd 3604 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐶 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
48 | | eldifn 3733 |
. . . . . 6
⊢ (𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊)) → ¬ 𝐶 ∈ (𝑆 ⊕ 𝑊)) |
49 | 48 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ¬ 𝐶 ∈ (𝑆 ⊕ 𝑊)) |
50 | 39, 47, 49 | ssnelpssd 3719 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
51 | 27 | lsmub1 18071 |
. . . . . . . . 9
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑊 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (𝑆 ⊕ 𝑊)) |
52 | 25, 26, 51 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ (𝑆 ⊕ 𝑊)) |
53 | 22 | snssd 4340 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐴} ⊆ 𝐵) |
54 | 8, 15, 53 | mrcssidd 16285 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐴} ⊆ (𝐾‘{𝐴})) |
55 | 54, 18 | syl6sseqr 3652 |
. . . . . . . . 9
⊢ (𝜑 → {𝐴} ⊆ 𝑆) |
56 | | snssg 4327 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑆 ↔ {𝐴} ⊆ 𝑆)) |
57 | 21, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ 𝑆 ↔ {𝐴} ⊆ 𝑆)) |
58 | 55, 57 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
59 | 52, 58 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝑆 ⊕ 𝑊)) |
60 | 59 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐴 ∈ (𝑆 ⊕ 𝑊)) |
61 | 39, 60 | sseldd 3604 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐴 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) |
62 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → 𝐺 ∈ Abel) |
63 | 27 | lsmsubg2 18262 |
. . . . . . 7
⊢ ((𝐺 ∈ Abel ∧ (𝑆 ⊕ 𝑊) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝐶}) ∈ (SubGrp‘𝐺)) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ∈ (SubGrp‘𝐺)) |
64 | 62, 30, 34, 63 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ∈ (SubGrp‘𝐺)) |
65 | | pgpfac1.2 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) |
66 | 65 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) |
67 | | psseq1 3694 |
. . . . . . . . 9
⊢ (𝑤 = ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) → (𝑤 ⊊ 𝑈 ↔ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈)) |
68 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑤 = ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})))) |
69 | 67, 68 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑤 = ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) → ((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) ↔ (((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈 ∧ 𝐴 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))))) |
70 | | psseq2 3695 |
. . . . . . . . 9
⊢ (𝑤 = ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) → ((𝑆 ⊕ 𝑊) ⊊ 𝑤 ↔ (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})))) |
71 | 70 | notbid 308 |
. . . . . . . 8
⊢ (𝑤 = ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) → (¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤 ↔ ¬ (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})))) |
72 | 69, 71 | imbi12d 334 |
. . . . . . 7
⊢ (𝑤 = ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) → (((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤) ↔ ((((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈 ∧ 𝐴 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) → ¬ (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))))) |
73 | 72 | rspcv 3305 |
. . . . . 6
⊢ (((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ∈ (SubGrp‘𝐺) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤) → ((((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈 ∧ 𝐴 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) → ¬ (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))))) |
74 | 64, 66, 73 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈 ∧ 𝐴 ∈ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶}))) → ¬ (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})))) |
75 | 61, 74 | mpan2d 710 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈 → ¬ (𝑆 ⊕ 𝑊) ⊊ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})))) |
76 | 50, 75 | mt2d 131 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ¬ ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈) |
77 | | npss 3717 |
. . 3
⊢ (¬
((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊊ 𝑈 ↔ (((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊆ 𝑈 → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈)) |
78 | 76, 77 | sylib 208 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → (((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) ⊆ 𝑈 → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈)) |
79 | 37, 78 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈) |