![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > shjshseli | Structured version Unicode version |
Description: A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
Ref | Expression |
---|---|
shjshs.1 |
![]() ![]() ![]() ![]() |
shjshs.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
shjshseli |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shjshs.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | shjshs.2 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | 1, 2 | shjshsi 25042 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | ococ 24956 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl5req 2506 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2 | shjcli 24925 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | eleq1 2524 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | mpbiri 233 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 8 | impbii 188 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-inf2 7953 ax-cc 8710 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 ax-pre-sup 9466 ax-addf 9467 ax-mulf 9468 ax-hilex 24548 ax-hfvadd 24549 ax-hvcom 24550 ax-hvass 24551 ax-hv0cl 24552 ax-hvaddid 24553 ax-hfvmul 24554 ax-hvmulid 24555 ax-hvmulass 24556 ax-hvdistr1 24557 ax-hvdistr2 24558 ax-hvmul0 24559 ax-hfi 24628 ax-his1 24631 ax-his2 24632 ax-his3 24633 ax-his4 24634 ax-hcompl 24751 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rmo 2804 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4195 df-int 4232 df-iun 4276 df-iin 4277 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-se 4783 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-isom 5530 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-of 6425 df-om 6582 df-1st 6682 df-2nd 6683 df-supp 6796 df-recs 6937 df-rdg 6971 df-1o 7025 df-2o 7026 df-oadd 7029 df-omul 7030 df-er 7206 df-map 7321 df-pm 7322 df-ixp 7369 df-en 7416 df-dom 7417 df-sdom 7418 df-fin 7419 df-fsupp 7727 df-fi 7767 df-sup 7797 df-oi 7830 df-card 8215 df-acn 8218 df-cda 8443 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-div 10100 df-nn 10429 df-2 10486 df-3 10487 df-4 10488 df-5 10489 df-6 10490 df-7 10491 df-8 10492 df-9 10493 df-10 10494 df-n0 10686 df-z 10753 df-dec 10862 df-uz 10968 df-q 11060 df-rp 11098 df-xneg 11195 df-xadd 11196 df-xmul 11197 df-ioo 11410 df-ico 11412 df-icc 11413 df-fz 11550 df-fzo 11661 df-fl 11754 df-seq 11919 df-exp 11978 df-hash 12216 df-cj 12701 df-re 12702 df-im 12703 df-sqr 12837 df-abs 12838 df-clim 13079 df-rlim 13080 df-sum 13277 df-struct 14289 df-ndx 14290 df-slot 14291 df-base 14292 df-sets 14293 df-ress 14294 df-plusg 14365 df-mulr 14366 df-starv 14367 df-sca 14368 df-vsca 14369 df-ip 14370 df-tset 14371 df-ple 14372 df-ds 14374 df-unif 14375 df-hom 14376 df-cco 14377 df-rest 14475 df-topn 14476 df-0g 14494 df-gsum 14495 df-topgen 14496 df-pt 14497 df-prds 14500 df-xrs 14554 df-qtop 14559 df-imas 14560 df-xps 14562 df-mre 14638 df-mrc 14639 df-acs 14641 df-mnd 15529 df-submnd 15579 df-mulg 15662 df-cntz 15949 df-cmn 16395 df-psmet 17929 df-xmet 17930 df-met 17931 df-bl 17932 df-mopn 17933 df-fbas 17934 df-fg 17935 df-cnfld 17939 df-top 18630 df-bases 18632 df-topon 18633 df-topsp 18634 df-cld 18750 df-ntr 18751 df-cls 18752 df-nei 18829 df-cn 18958 df-cnp 18959 df-lm 18960 df-haus 19046 df-tx 19262 df-hmeo 19455 df-fil 19546 df-fm 19638 df-flim 19639 df-flf 19640 df-xms 20022 df-ms 20023 df-tms 20024 df-cfil 20893 df-cau 20894 df-cmet 20895 df-grpo 23825 df-gid 23826 df-ginv 23827 df-gdiv 23828 df-ablo 23916 df-subgo 23936 df-vc 24071 df-nv 24117 df-va 24120 df-ba 24121 df-sm 24122 df-0v 24123 df-vs 24124 df-nmcv 24125 df-ims 24126 df-dip 24243 df-ssp 24267 df-ph 24360 df-cbn 24411 df-hnorm 24517 df-hba 24518 df-hvsub 24520 df-hlim 24521 df-hcau 24522 df-sh 24756 df-ch 24771 df-oc 24802 df-ch0 24803 df-shs 24858 df-chj 24860 |
This theorem is referenced by: osumi 25192 |
Copyright terms: Public domain | W3C validator |