![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lspprcl | Structured version Visualization version GIF version |
Description: The span of a pair is a subspace (frequently used special case of lspcl 19099). (Contributed by NM, 11-Apr-2015.) |
Ref | Expression |
---|---|
lspval.v | ⊢ 𝑉 = (Base‘𝑊) |
lspval.s | ⊢ 𝑆 = (LSubSp‘𝑊) |
lspval.n | ⊢ 𝑁 = (LSpan‘𝑊) |
lspprcl.w | ⊢ (𝜑 → 𝑊 ∈ LMod) |
lspprcl.x | ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
lspprcl.y | ⊢ (𝜑 → 𝑌 ∈ 𝑉) |
Ref | Expression |
---|---|
lspprcl | ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspprcl.w | . 2 ⊢ (𝜑 → 𝑊 ∈ LMod) | |
2 | lspprcl.x | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑉) | |
3 | lspprcl.y | . . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑉) | |
4 | prssi 4461 | . . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉) | |
5 | 2, 3, 4 | syl2anc 696 | . 2 ⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉) |
6 | lspval.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
7 | lspval.s | . . 3 ⊢ 𝑆 = (LSubSp‘𝑊) | |
8 | lspval.n | . . 3 ⊢ 𝑁 = (LSpan‘𝑊) | |
9 | 6, 7, 8 | lspcl 19099 | . 2 ⊢ ((𝑊 ∈ LMod ∧ {𝑋, 𝑌} ⊆ 𝑉) → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆) |
10 | 1, 5, 9 | syl2anc 696 | 1 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1596 ∈ wcel 2103 ⊆ wss 3680 {cpr 4287 ‘cfv 6001 Basecbs 15980 LModclmod 18986 LSubSpclss 19055 LSpanclspn 19094 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-cnex 10105 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 ax-pre-mulgt0 10126 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-int 4584 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-om 7183 df-1st 7285 df-2nd 7286 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-er 7862 df-en 8073 df-dom 8074 df-sdom 8075 df-pnf 10189 df-mnf 10190 df-xr 10191 df-ltxr 10192 df-le 10193 df-sub 10381 df-neg 10382 df-nn 11134 df-2 11192 df-ndx 15983 df-slot 15984 df-base 15986 df-sets 15987 df-plusg 16077 df-0g 16225 df-mgm 17364 df-sgrp 17406 df-mnd 17417 df-grp 17547 df-minusg 17548 df-sbg 17549 df-mgp 18611 df-ur 18623 df-ring 18670 df-lmod 18988 df-lss 19056 df-lsp 19095 |
This theorem is referenced by: lspprid1 19120 lspprvacl 19122 lsmelpr 19214 lspexch 19252 lspindpi 19255 lsppratlem4 19273 lsatfixedN 34716 dvh3dim2 37156 dvh3dim3N 37157 lclkrlem2v 37236 lcfrlem23 37273 lcfrlem25 37275 mapdindp 37379 baerlem3lem1 37415 baerlem5alem1 37416 baerlem5blem1 37417 baerlem5amN 37424 baerlem5bmN 37425 baerlem5abmN 37426 mapdh6aN 37443 mapdh6b0N 37444 mapdh6iN 37452 lspindp5 37478 mapdh8ab 37485 mapdh8ad 37487 mapdh8e 37492 mapdh9a 37498 mapdh9aOLDN 37499 hdmap1l6a 37518 hdmap1l6b0N 37519 hdmap1l6i 37527 hdmap1eulemOLDN 37533 hdmapval0 37544 hdmapval3lemN 37548 hdmap10lem 37550 hdmap11lem1 37552 hdmap11lem2 37553 hdmap14lem11 37589 |
Copyright terms: Public domain | W3C validator |