Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > spansnmul | Structured version Visualization version GIF version |
Description: A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Ref | Expression |
---|---|
spansnmul | ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spansnsh 29671 | . . . 4 ⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Sℋ ) | |
2 | spansnid 29673 | . . . 4 ⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴})) | |
3 | 1, 2 | jca 515 | . . 3 ⊢ (𝐴 ∈ ℋ → ((span‘{𝐴}) ∈ Sℋ ∧ 𝐴 ∈ (span‘{𝐴}))) |
4 | shmulcl 29328 | . . . . 5 ⊢ (((span‘{𝐴}) ∈ Sℋ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ (span‘{𝐴})) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) | |
5 | 4 | 3com12 1125 | . . . 4 ⊢ ((𝐵 ∈ ℂ ∧ (span‘{𝐴}) ∈ Sℋ ∧ 𝐴 ∈ (span‘{𝐴})) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) |
6 | 5 | 3expb 1122 | . . 3 ⊢ ((𝐵 ∈ ℂ ∧ ((span‘{𝐴}) ∈ Sℋ ∧ 𝐴 ∈ (span‘{𝐴}))) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) |
7 | 3, 6 | sylan2 596 | . 2 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) |
8 | 7 | ancoms 462 | 1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2112 {csn 4557 ‘cfv 6400 (class class class)co 7234 ℂcc 10754 ℋchba 29029 ·ℎ csm 29031 Sℋ csh 29038 spancspn 29042 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5195 ax-sep 5208 ax-nul 5215 ax-pow 5274 ax-pr 5338 ax-un 7544 ax-inf2 9283 ax-cc 10076 ax-cnex 10812 ax-resscn 10813 ax-1cn 10814 ax-icn 10815 ax-addcl 10816 ax-addrcl 10817 ax-mulcl 10818 ax-mulrcl 10819 ax-mulcom 10820 ax-addass 10821 ax-mulass 10822 ax-distr 10823 ax-i2m1 10824 ax-1ne0 10825 ax-1rid 10826 ax-rnegex 10827 ax-rrecex 10828 ax-cnre 10829 ax-pre-lttri 10830 ax-pre-lttrn 10831 ax-pre-ltadd 10832 ax-pre-mulgt0 10833 ax-pre-sup 10834 ax-addf 10835 ax-mulf 10836 ax-hilex 29109 ax-hfvadd 29110 ax-hvcom 29111 ax-hvass 29112 ax-hv0cl 29113 ax-hvaddid 29114 ax-hfvmul 29115 ax-hvmulid 29116 ax-hvmulass 29117 ax-hvdistr1 29118 ax-hvdistr2 29119 ax-hvmul0 29120 ax-hfi 29189 ax-his1 29192 ax-his2 29193 ax-his3 29194 ax-his4 29195 ax-hcompl 29312 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3711 df-csb 3828 df-dif 3885 df-un 3887 df-in 3889 df-ss 3899 df-pss 3901 df-nul 4254 df-if 4456 df-pw 4531 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4836 df-int 4876 df-iun 4922 df-iin 4923 df-br 5070 df-opab 5132 df-mpt 5152 df-tr 5178 df-id 5471 df-eprel 5477 df-po 5485 df-so 5486 df-fr 5526 df-se 5527 df-we 5528 df-xp 5574 df-rel 5575 df-cnv 5576 df-co 5577 df-dm 5578 df-rn 5579 df-res 5580 df-ima 5581 df-pred 6178 df-ord 6236 df-on 6237 df-lim 6238 df-suc 6239 df-iota 6358 df-fun 6402 df-fn 6403 df-f 6404 df-f1 6405 df-fo 6406 df-f1o 6407 df-fv 6408 df-isom 6409 df-riota 7191 df-ov 7237 df-oprab 7238 df-mpo 7239 df-of 7490 df-om 7666 df-1st 7782 df-2nd 7783 df-supp 7927 df-wrecs 8070 df-recs 8131 df-rdg 8169 df-1o 8225 df-2o 8226 df-oadd 8229 df-omul 8230 df-er 8414 df-map 8533 df-pm 8534 df-ixp 8602 df-en 8650 df-dom 8651 df-sdom 8652 df-fin 8653 df-fsupp 9013 df-fi 9054 df-sup 9085 df-inf 9086 df-oi 9153 df-card 9582 df-acn 9585 df-pnf 10896 df-mnf 10897 df-xr 10898 df-ltxr 10899 df-le 10900 df-sub 11091 df-neg 11092 df-div 11517 df-nn 11858 df-2 11920 df-3 11921 df-4 11922 df-5 11923 df-6 11924 df-7 11925 df-8 11926 df-9 11927 df-n0 12118 df-z 12204 df-dec 12321 df-uz 12466 df-q 12572 df-rp 12614 df-xneg 12731 df-xadd 12732 df-xmul 12733 df-ioo 12966 df-ico 12968 df-icc 12969 df-fz 13123 df-fzo 13266 df-fl 13394 df-seq 13604 df-exp 13665 df-hash 13927 df-cj 14692 df-re 14693 df-im 14694 df-sqrt 14828 df-abs 14829 df-clim 15079 df-rlim 15080 df-sum 15280 df-struct 16730 df-sets 16747 df-slot 16765 df-ndx 16775 df-base 16791 df-ress 16815 df-plusg 16845 df-mulr 16846 df-starv 16847 df-sca 16848 df-vsca 16849 df-ip 16850 df-tset 16851 df-ple 16852 df-ds 16854 df-unif 16855 df-hom 16856 df-cco 16857 df-rest 16957 df-topn 16958 df-0g 16976 df-gsum 16977 df-topgen 16978 df-pt 16979 df-prds 16982 df-xrs 17037 df-qtop 17042 df-imas 17043 df-xps 17045 df-mre 17119 df-mrc 17120 df-acs 17122 df-mgm 18144 df-sgrp 18193 df-mnd 18204 df-submnd 18249 df-mulg 18519 df-cntz 18741 df-cmn 19202 df-psmet 20385 df-xmet 20386 df-met 20387 df-bl 20388 df-mopn 20389 df-fbas 20390 df-fg 20391 df-cnfld 20394 df-top 21820 df-topon 21837 df-topsp 21859 df-bases 21872 df-cld 21945 df-ntr 21946 df-cls 21947 df-nei 22024 df-cn 22153 df-cnp 22154 df-lm 22155 df-haus 22241 df-tx 22488 df-hmeo 22681 df-fil 22772 df-fm 22864 df-flim 22865 df-flf 22866 df-xms 23247 df-ms 23248 df-tms 23249 df-cfil 24181 df-cau 24182 df-cmet 24183 df-grpo 28603 df-gid 28604 df-ginv 28605 df-gdiv 28606 df-ablo 28655 df-vc 28669 df-nv 28702 df-va 28705 df-ba 28706 df-sm 28707 df-0v 28708 df-vs 28709 df-nmcv 28710 df-ims 28711 df-dip 28811 df-ssp 28832 df-ph 28923 df-cbn 28973 df-hnorm 29078 df-hba 29079 df-hvsub 29081 df-hlim 29082 df-hcau 29083 df-sh 29317 df-ch 29331 df-oc 29362 df-ch0 29363 df-span 29419 |
This theorem is referenced by: spanunsni 29689 |
Copyright terms: Public domain | W3C validator |