![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > spansnss2 | Structured version Visualization version Unicode version |
Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
Ref | Expression |
---|---|
spansnss2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spansnss 27224 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 436 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | spansnid 27216 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | ssel 3426 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | syl5com 31 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | adantl 468 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | impbid 194 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cc 8865 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619 ax-hilex 26652 ax-hfvadd 26653 ax-hvcom 26654 ax-hvass 26655 ax-hv0cl 26656 ax-hvaddid 26657 ax-hfvmul 26658 ax-hvmulid 26659 ax-hvmulass 26660 ax-hvdistr1 26661 ax-hvdistr2 26662 ax-hvmul0 26663 ax-hfi 26732 ax-his1 26735 ax-his2 26736 ax-his3 26737 ax-his4 26738 ax-hcompl 26855 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-omul 7187 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-acn 8376 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-rlim 13553 df-sum 13753 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cld 20034 df-ntr 20035 df-cls 20036 df-nei 20114 df-cn 20243 df-cnp 20244 df-lm 20245 df-haus 20331 df-tx 20577 df-hmeo 20770 df-fil 20861 df-fm 20953 df-flim 20954 df-flf 20955 df-xms 21335 df-ms 21336 df-tms 21337 df-cfil 22225 df-cau 22226 df-cmet 22227 df-grpo 25919 df-gid 25920 df-ginv 25921 df-gdiv 25922 df-ablo 26010 df-subgo 26030 df-vc 26165 df-nv 26211 df-va 26214 df-ba 26215 df-sm 26216 df-0v 26217 df-vs 26218 df-nmcv 26219 df-ims 26220 df-dip 26337 df-ssp 26361 df-ph 26454 df-cbn 26505 df-hnorm 26621 df-hba 26622 df-hvsub 26624 df-hlim 26625 df-hcau 26626 df-sh 26860 df-ch 26874 df-oc 26905 df-ch0 26906 df-span 26962 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |