![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > chj0i | Structured version Visualization version Unicode version |
Description: Join with lattice zero in
![]() |
Ref | Expression |
---|---|
ch0le.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
chj0i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ch0le.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | h0elch 26901 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | chjvali 26999 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | ch0lei 27097 |
. . . . 5
![]() ![]() ![]() ![]() |
5 | ssequn2 3606 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | mpbi 212 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | fveq2i 5866 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | fveq2i 5866 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 1 | pjococi 27083 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 3, 8, 9 | 3eqtri 2476 |
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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cc 8862 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614 ax-addf 9615 ax-mulf 9616 ax-hilex 26645 ax-hfvadd 26646 ax-hvcom 26647 ax-hvass 26648 ax-hv0cl 26649 ax-hvaddid 26650 ax-hfvmul 26651 ax-hvmulid 26652 ax-hvmulass 26653 ax-hvdistr1 26654 ax-hvdistr2 26655 ax-hvmul0 26656 ax-hfi 26725 ax-his1 26728 ax-his2 26729 ax-his3 26730 ax-his4 26731 ax-hcompl 26848 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-iin 4280 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-omul 7184 df-er 7360 df-map 7471 df-pm 7472 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-fi 7922 df-sup 7953 df-inf 7954 df-oi 8022 df-card 8370 df-acn 8373 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-n0 10867 df-z 10935 df-uz 11157 df-q 11262 df-rp 11300 df-xneg 11406 df-xadd 11407 df-xmul 11408 df-ico 11638 df-icc 11639 df-fz 11782 df-fl 12025 df-seq 12211 df-exp 12270 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-rlim 13546 df-rest 15314 df-topgen 15335 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-mopn 18959 df-fbas 18960 df-fg 18961 df-top 19914 df-bases 19915 df-topon 19916 df-cld 20027 df-ntr 20028 df-cls 20029 df-nei 20107 df-lm 20238 df-haus 20324 df-fil 20854 df-fm 20946 df-flim 20947 df-flf 20948 df-cfil 22218 df-cau 22219 df-cmet 22220 df-grpo 25912 df-gid 25913 df-ginv 25914 df-gdiv 25915 df-ablo 26003 df-subgo 26023 df-vc 26158 df-nv 26204 df-va 26207 df-ba 26208 df-sm 26209 df-0v 26210 df-vs 26211 df-nmcv 26212 df-ims 26213 df-ssp 26354 df-ph 26447 df-cbn 26498 df-hnorm 26614 df-hba 26615 df-hvsub 26617 df-hlim 26618 df-hcau 26619 df-sh 26853 df-ch 26867 df-oc 26898 df-ch0 26899 df-chj 26956 |
This theorem is referenced by: chj00i 27133 chj0 27143 nonbooli 27297 atoml2i 28029 atabsi 28047 |
Copyright terms: Public domain | W3C validator |