Step | Hyp | Ref
| Expression |
1 | | lspindp5.m |
. . 3
β’ (π β Β¬ π β (πβ{π, π})) |
2 | | lspindp5.e |
. . . 4
β’ (π β π β (πβ{π, π})) |
3 | | ssel 3942 |
. . . 4
β’ ((πβ{π, π}) β (πβ{π, π}) β (π β (πβ{π, π}) β π β (πβ{π, π}))) |
4 | 2, 3 | syl5com 31 |
. . 3
β’ (π β ((πβ{π, π}) β (πβ{π, π}) β π β (πβ{π, π}))) |
5 | 1, 4 | mtod 197 |
. 2
β’ (π β Β¬ (πβ{π, π}) β (πβ{π, π})) |
6 | | lspindp5.w |
. . . . . . 7
β’ (π β π β LVec) |
7 | | lveclmod 20583 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
9 | | lspindp5.y |
. . . . . . 7
β’ (π β π β π) |
10 | | lspindp5.x |
. . . . . . 7
β’ (π β π β π) |
11 | | prssi 4786 |
. . . . . . 7
β’ ((π β π β§ π β π) β {π, π} β π) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . 6
β’ (π β {π, π} β π) |
13 | | snsspr1 4779 |
. . . . . . 7
β’ {π} β {π, π} |
14 | 13 | a1i 11 |
. . . . . 6
β’ (π β {π} β {π, π}) |
15 | | lspindp5.v |
. . . . . . 7
β’ π = (Baseβπ) |
16 | | lspindp5.n |
. . . . . . 7
β’ π = (LSpanβπ) |
17 | 15, 16 | lspss 20461 |
. . . . . 6
β’ ((π β LMod β§ {π, π} β π β§ {π} β {π, π}) β (πβ{π}) β (πβ{π, π})) |
18 | 8, 12, 14, 17 | syl3anc 1372 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π, π})) |
19 | 18 | biantrurd 534 |
. . . 4
β’ (π β ((πβ{π}) β (πβ{π, π}) β ((πβ{π}) β (πβ{π, π}) β§ (πβ{π}) β (πβ{π, π})))) |
20 | | eqid 2737 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
21 | 20 | lsssssubg 20435 |
. . . . . . 7
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
22 | 8, 21 | syl 17 |
. . . . . 6
β’ (π β (LSubSpβπ) β (SubGrpβπ)) |
23 | 15, 20, 16 | lspsncl 20454 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
24 | 8, 9, 23 | syl2anc 585 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
25 | 22, 24 | sseldd 3950 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
26 | | lspindp5.u |
. . . . . . 7
β’ (π β π β π) |
27 | 15, 20, 16 | lspsncl 20454 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
28 | 8, 26, 27 | syl2anc 585 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
29 | 22, 28 | sseldd 3950 |
. . . . 5
β’ (π β (πβ{π}) β (SubGrpβπ)) |
30 | 15, 20, 16, 8, 9, 10 | lspprcl 20455 |
. . . . . 6
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
31 | 22, 30 | sseldd 3950 |
. . . . 5
β’ (π β (πβ{π, π}) β (SubGrpβπ)) |
32 | | eqid 2737 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
33 | 32 | lsmlub 19453 |
. . . . 5
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ) β§ (πβ{π, π}) β (SubGrpβπ)) β (((πβ{π}) β (πβ{π, π}) β§ (πβ{π}) β (πβ{π, π})) β ((πβ{π})(LSSumβπ)(πβ{π})) β (πβ{π, π}))) |
34 | 25, 29, 31, 33 | syl3anc 1372 |
. . . 4
β’ (π β (((πβ{π}) β (πβ{π, π}) β§ (πβ{π}) β (πβ{π, π})) β ((πβ{π})(LSSumβπ)(πβ{π})) β (πβ{π, π}))) |
35 | 19, 34 | bitrd 279 |
. . 3
β’ (π β ((πβ{π}) β (πβ{π, π}) β ((πβ{π})(LSSumβπ)(πβ{π})) β (πβ{π, π}))) |
36 | 15, 20, 16, 8, 30, 26 | lspsnel5 20472 |
. . 3
β’ (π β (π β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
37 | 15, 16, 32, 8, 9, 26 | lsmpr 20566 |
. . . 4
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
38 | 37 | sseq1d 3980 |
. . 3
β’ (π β ((πβ{π, π}) β (πβ{π, π}) β ((πβ{π})(LSSumβπ)(πβ{π})) β (πβ{π, π}))) |
39 | 35, 36, 38 | 3bitr4d 311 |
. 2
β’ (π β (π β (πβ{π, π}) β (πβ{π, π}) β (πβ{π, π}))) |
40 | 5, 39 | mtbird 325 |
1
β’ (π β Β¬ π β (πβ{π, π})) |