Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lspsnel5 | Structured version Visualization version GIF version |
Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) |
Ref | Expression |
---|---|
lspsnel5.v | β’ π = (Baseβπ) |
lspsnel5.s | β’ π = (LSubSpβπ) |
lspsnel5.n | β’ π = (LSpanβπ) |
lspsnel5.w | β’ (π β π β LMod) |
lspsnel5.a | β’ (π β π β π) |
lspsnel5.x | β’ (π β π β π) |
Ref | Expression |
---|---|
lspsnel5 | β’ (π β (π β π β (πβ{π}) β π)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspsnel5.x | . 2 β’ (π β π β π) | |
2 | lspsnel5.v | . . 3 β’ π = (Baseβπ) | |
3 | lspsnel5.s | . . 3 β’ π = (LSubSpβπ) | |
4 | lspsnel5.n | . . 3 β’ π = (LSpanβπ) | |
5 | lspsnel5.w | . . 3 β’ (π β π β LMod) | |
6 | lspsnel5.a | . . 3 β’ (π β π β π) | |
7 | 2, 3, 4, 5, 6 | lspsnel6 20378 | . 2 β’ (π β (π β π β (π β π β§ (πβ{π}) β π))) |
8 | 1, 7 | mpbirand 705 | 1 β’ (π β (π β π β (πβ{π}) β π)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wb 205 = wceq 1541 β wcel 2106 β wss 3908 {csn 4584 βcfv 6491 Basecbs 17017 LModclmod 20245 LSubSpclss 20315 LSpanclspn 20355 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5240 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-int 4906 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5528 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-riota 7305 df-ov 7352 df-0g 17257 df-mgm 18431 df-sgrp 18480 df-mnd 18491 df-grp 18685 df-lmod 20247 df-lss 20316 df-lsp 20356 |
This theorem is referenced by: lspsnel5a 20380 lspprid1 20381 lspsnss2 20389 lsmelpr 20475 lspsncmp 20500 lspsnne1 20501 lspsnne2 20502 lspsneq 20506 lspindpi 20516 islbs2 20538 lindsadd 35966 lindsenlbs 35968 lsatelbN 37363 lsmsat 37365 lsatfixedN 37366 l1cvpat 37411 dia2dimlem5 39426 dochsncom 39740 dihjat1lem 39786 dvh4dimlem 39801 lclkrlem2a 39865 lcfrlem6 39905 lcfrlem20 39920 lcfrlem26 39926 lcfrlem36 39936 mapdval2N 39988 mapdrvallem2 40003 mapdindp 40029 mapdh6aN 40093 lspindp5 40128 mapdh8ab 40135 mapdh8e 40142 hdmap1l6a 40167 hdmaprnlem3eN 40216 hdmapoc 40289 |
Copyright terms: Public domain | W3C validator |