![]() |
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 2734 | . . 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 20952 | . . . 4 ⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑊)) |
8 | 6, 1, 7 | syl2anc 584 | . . 3 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑊)) |
9 | 2, 3, 4, 5, 6, 8 | ellspsn5b 21010 | . 2 ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑁‘{𝑋}) ⊆ 𝑈)) |
10 | 1, 9 | mpbid 232 | 1 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 ⊆ wss 3962 {csn 4630 ‘cfv 6562 Basecbs 17244 LModclmod 20874 LSubSpclss 20946 LSpanclspn 20986 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-0g 17487 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-grp 18966 df-lmod 20876 df-lss 20947 df-lsp 20987 |
This theorem is referenced by: lssats2 21015 lspsn 21017 lspsnvsi 21019 lsmelval2 21101 lspprabs 21111 lspvadd 21112 lspabs3 21140 lsmcv 21160 lspsnat 21164 lsppratlem6 21171 issubassa2 21929 lshpnel 38964 lsatel 38986 lsmsat 38989 lssatomic 38992 lssats 38993 lsat0cv 39014 dia2dimlem10 41055 dochsatshpb 41434 lclkrlem2f 41494 lcfrlem25 41549 lcfrlem35 41559 mapdval2N 41612 mapdrvallem2 41627 mapdpglem8 41661 mapdpglem13 41666 mapdindp0 41701 mapdh6aN 41717 mapdh8e 41766 mapdh9a 41771 hdmap1l6a 41791 hdmapval0 41815 hdmapval3lemN 41819 hdmap10lem 41821 hdmap11lem1 41823 hdmap11lem2 41824 hdmaprnlem4N 41835 hdmaprnlem3eN 41840 |
Copyright terms: Public domain | W3C validator |