| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lspindpi.e |
. . 3
β’ (π β Β¬ π β (πβ{π, π})) |
| 2 | | lspindpi.w |
. . . . . . . . . . 11
β’ (π β π β LVec) |
| 3 | | lveclmod 20954 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . . 10
β’ (π β π β LMod) |
| 5 | | eqid 2726 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 6 | 5 | lsssssubg 20805 |
. . . . . . . . . 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 20824 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 12 | 4, 8, 11 | syl2anc 583 |
. . . . . . . . 9
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 13 | 7, 12 | sseldd 3978 |
. . . . . . . 8
β’ (π β (πβ{π}) β (SubGrpβπ)) |
| 14 | | lspindpi.z |
. . . . . . . . . 10
β’ (π β π β π) |
| 15 | 9, 5, 10 | lspsncl 20824 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 16 | 4, 14, 15 | syl2anc 583 |
. . . . . . . . 9
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 17 | 7, 16 | sseldd 3978 |
. . . . . . . 8
β’ (π β (πβ{π}) β (SubGrpβπ)) |
| 18 | | eqid 2726 |
. . . . . . . . 9
β’
(LSSumβπ) =
(LSSumβπ) |
| 19 | 18 | lsmub1 19577 |
. . . . . . . 8
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 20 | 13, 17, 19 | syl2anc 583 |
. . . . . . 7
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 21 | 9, 10, 18, 4, 8, 14 | lsmpr 20937 |
. . . . . . 7
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 22 | 20, 21 | sseqtrrd 4018 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π, π})) |
| 23 | | sseq1 4002 |
. . . . . 6
β’ ((πβ{π}) = (πβ{π}) β ((πβ{π}) β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
| 24 | 22, 23 | syl5ibrcom 246 |
. . . . 5
β’ (π β ((πβ{π}) = (πβ{π}) β (πβ{π}) β (πβ{π, π}))) |
| 25 | 9, 5, 10, 4, 8, 14 | lspprcl 20825 |
. . . . . 6
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
| 26 | | lspindpi.x |
. . . . . 6
β’ (π β π β π) |
| 27 | 9, 5, 10, 4, 25, 26 | lspsnel5 20842 |
. . . . 5
β’ (π β (π β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
| 28 | 24, 27 | sylibrd 259 |
. . . 4
β’ (π β ((πβ{π}) = (πβ{π}) β π β (πβ{π, π}))) |
| 29 | 28 | necon3bd 2948 |
. . 3
β’ (π β (Β¬ π β (πβ{π, π}) β (πβ{π}) β (πβ{π}))) |
| 30 | 1, 29 | mpd 15 |
. 2
β’ (π β (πβ{π}) β (πβ{π})) |
| 31 | 18 | lsmub2 19578 |
. . . . . . . 8
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 32 | 13, 17, 31 | syl2anc 583 |
. . . . . . 7
β’ (π β (πβ{π}) β ((πβ{π})(LSSumβπ)(πβ{π}))) |
| 33 | 32, 21 | sseqtrrd 4018 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π, π})) |
| 34 | | sseq1 4002 |
. . . . . 6
β’ ((πβ{π}) = (πβ{π}) β ((πβ{π}) β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
| 35 | 33, 34 | syl5ibrcom 246 |
. . . . 5
β’ (π β ((πβ{π}) = (πβ{π}) β (πβ{π}) β (πβ{π, π}))) |
| 36 | 35, 27 | sylibrd 259 |
. . . 4
β’ (π β ((πβ{π}) = (πβ{π}) β π β (πβ{π, π}))) |
| 37 | 36 | necon3bd 2948 |
. . 3
β’ (π β (Β¬ π β (πβ{π, π}) β (πβ{π}) β (πβ{π}))) |
| 38 | 1, 37 | mpd 15 |
. 2
β’ (π β (πβ{π}) β (πβ{π})) |
| 39 | 30, 38 | jca 511 |
1
β’ (π β ((πβ{π}) β (πβ{π}) β§ (πβ{π}) β (πβ{π}))) |
