Step | Hyp | Ref
| Expression |
1 | | lspindpi.e |
. . 3
β’ (π β Β¬ π β (πβ{π, π})) |
2 | | lspindpi.w |
. . . . . . . . . . 11
β’ (π β π β LVec) |
3 | | lveclmod 20583 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
β’ (π β π β LMod) |
5 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
6 | 5 | lsssssubg 20435 |
. . . . . . . . . 10
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
β’ (π β (LSubSpβπ) β (SubGrpβπ)) |
8 | | lspindpi.y |
. . . . . . . . . 10
β’ (π β π β π) |
9 | | lspindpi.v |
. . . . . . . . . . 11
β’ π = (Baseβπ) |
10 | | lspindpi.n |
. . . . . . . . . . 11
β’ π = (LSpanβπ) |
11 | 9, 5, 10 | lspsncl 20454 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
12 | 4, 8, 11 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβ{π}) β (LSubSpβπ)) |
13 | 7, 12 | sseldd 3950 |
. . . . . . . 8
β’ (π β (πβ{π}) β (SubGrpβπ)) |
14 | | lspindpi.z |
. . . . . . . . . 10
β’ (π β π β π) |
15 | 9, 5, 10 | lspsncl 20454 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
16 | 4, 14, 15 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβ{π}) β (LSubSpβπ)) |
17 | 7, 16 | sseldd 3950 |
. . . . . . . 8
β’ (π β (πβ{π}) β (SubGrpβπ)) |
18 | | eqid 2737 |
. . . . . . . . 9
β’
(LSSumβπ) =
(LSSumβπ) |
19 | 18 | lsmub1 19446 |
. . . . . . . 8
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
20 | 13, 17, 19 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
21 | 9, 10, 18, 4, 8, 14 | lsmpr 20566 |
. . . . . . 7
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
22 | 20, 21 | sseqtrrd 3990 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π, π})) |
23 | | sseq1 3974 |
. . . . . 6
β’ ((πβ{π}) = (πβ{π}) β ((πβ{π}) β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
24 | 22, 23 | syl5ibrcom 247 |
. . . . 5
β’ (π β ((πβ{π}) = (πβ{π}) β (πβ{π}) β (πβ{π, π}))) |
25 | 9, 5, 10, 4, 8, 14 | lspprcl 20455 |
. . . . . 6
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
26 | | lspindpi.x |
. . . . . 6
β’ (π β π β π) |
27 | 9, 5, 10, 4, 25, 26 | lspsnel5 20472 |
. . . . 5
β’ (π β (π β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
28 | 24, 27 | sylibrd 259 |
. . . 4
β’ (π β ((πβ{π}) = (πβ{π}) β π β (πβ{π, π}))) |
29 | 28 | necon3bd 2958 |
. . 3
β’ (π β (Β¬ π β (πβ{π, π}) β (πβ{π}) β (πβ{π}))) |
30 | 1, 29 | mpd 15 |
. 2
β’ (π β (πβ{π}) β (πβ{π})) |
31 | 18 | lsmub2 19447 |
. . . . . . . 8
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
32 | 13, 17, 31 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
33 | 32, 21 | sseqtrrd 3990 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π, π})) |
34 | | sseq1 3974 |
. . . . . 6
β’ ((πβ{π}) = (πβ{π}) β ((πβ{π}) β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
35 | 33, 34 | syl5ibrcom 247 |
. . . . 5
β’ (π β ((πβ{π}) = (πβ{π}) β (πβ{π}) β (πβ{π, π}))) |
36 | 35, 27 | sylibrd 259 |
. . . 4
β’ (π β ((πβ{π}) = (πβ{π}) β π β (πβ{π, π}))) |
37 | 36 | necon3bd 2958 |
. . 3
β’ (π β (Β¬ π β (πβ{π, π}) β (πβ{π}) β (πβ{π}))) |
38 | 1, 37 | mpd 15 |
. 2
β’ (π β (πβ{π}) β (πβ{π})) |
39 | 30, 38 | jca 513 |
1
β’ (π β ((πβ{π}) β (πβ{π}) β§ (πβ{π}) β (πβ{π}))) |