| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ellspsn5 | Structured version Visualization version GIF version | ||
| Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.) |
| Ref | Expression |
|---|---|
| ellspsn5.s | ⊢ 𝑆 = (LSubSp‘𝑊) |
| ellspsn5.n | ⊢ 𝑁 = (LSpan‘𝑊) |
| ellspsn5.w | ⊢ (𝜑 → 𝑊 ∈ LMod) |
| ellspsn5.a | ⊢ (𝜑 → 𝑈 ∈ 𝑆) |
| ellspsn5.x | ⊢ (𝜑 → 𝑋 ∈ 𝑈) |
| Ref | Expression |
|---|---|
| ellspsn5 | ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ellspsn5.x | . 2 ⊢ (𝜑 → 𝑋 ∈ 𝑈) | |
| 2 | eqid 2736 | . . 3 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
| 3 | ellspsn5.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
| 4 | ellspsn5.n | . . 3 ⊢ 𝑁 = (LSpan‘𝑊) | |
| 5 | ellspsn5.w | . . 3 ⊢ (𝜑 → 𝑊 ∈ LMod) | |
| 6 | ellspsn5.a | . . 3 ⊢ (𝜑 → 𝑈 ∈ 𝑆) | |
| 7 | 2, 3 | lssel 20888 | . . . 4 ⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑊)) |
| 8 | 6, 1, 7 | syl2anc 584 | . . 3 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑊)) |
| 9 | 2, 3, 4, 5, 6, 8 | ellspsn5b 20946 | . 2 ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑁‘{𝑋}) ⊆ 𝑈)) |
| 10 | 1, 9 | mpbid 232 | 1 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 ⊆ wss 3901 {csn 4580 ‘cfv 6492 Basecbs 17136 LModclmod 20811 LSubSpclss 20882 LSpanclspn 20922 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-0g 17361 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-grp 18866 df-lmod 20813 df-lss 20883 df-lsp 20923 |
| This theorem is referenced by: lssats2 20951 lspsn 20953 lspsnvsi 20955 lsmelval2 21037 lspprabs 21047 lspvadd 21048 lspabs3 21076 lsmcv 21096 lspsnat 21100 lsppratlem6 21107 issubassa2 21848 lshpnel 39243 lsatel 39265 lsmsat 39268 lssatomic 39271 lssats 39272 lsat0cv 39293 dia2dimlem10 41333 dochsatshpb 41712 lclkrlem2f 41772 lcfrlem25 41827 lcfrlem35 41837 mapdval2N 41890 mapdrvallem2 41905 mapdpglem8 41939 mapdpglem13 41944 mapdindp0 41979 mapdh6aN 41995 mapdh8e 42044 mapdh9a 42049 hdmap1l6a 42069 hdmapval0 42093 hdmapval3lemN 42097 hdmap10lem 42099 hdmap11lem1 42101 hdmap11lem2 42102 hdmaprnlem4N 42113 hdmaprnlem3eN 42118 |
| Copyright terms: Public domain | W3C validator |