Theorem ho0f 29512

Description: Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
ho0f	⊢ 0hop : ℋ⟶ ℋ

Proof of Theorem ho0f

Step	Hyp	Ref	Expression
1		h0elch 29016	. . 3 ⊢ 0ℋ ∈ Cℋ
2	1	pjfi 29465	. 2 ⊢ (projℎ‘0ℋ): ℋ⟶ ℋ
3		df-h0op 29509	. . 3 ⊢ 0hop = (projℎ‘0ℋ)
4	3	feq1i 6491	. 2 ⊢ ( 0hop : ℋ⟶ ℋ ↔ (projℎ‘0ℋ): ℋ⟶ ℋ)
5	2, 4	mpbir 233	1 ⊢ 0hop : ℋ⟶ ℋ

Syntax hints:  ⟶wf 6337  ‘cfv 6341   ℋchba 28680  0_ℋc0h 28696  proj_ℎcpjh 28698   0_hop ch0o 28704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-inf2 9090  ax-cc 9843  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600  ax-pre-sup 10601  ax-addf 10602  ax-mulf 10603  ax-hilex 28760  ax-hfvadd 28761  ax-hvcom 28762  ax-hvass 28763  ax-hv0cl 28764  ax-hvaddid 28765  ax-hfvmul 28766  ax-hvmulid 28767  ax-hvmulass 28768  ax-hvdistr1 28769  ax-hvdistr2 28770  ax-hvmul0 28771  ax-hfi 28840  ax-his1 28843  ax-his2 28844  ax-his3 28845  ax-his4 28846  ax-hcompl 28963

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-se 5501  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-of 7395  df-om 7567  df-1st 7675  df-2nd 7676  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-omul 8093  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8820  df-fi 8861  df-sup 8892  df-inf 8893  df-oi 8960  df-card 9354  df-acn 9357  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-div 11284  df-nn 11625  df-2 11687  df-3 11688  df-4 11689  df-5 11690  df-6 11691  df-7 11692  df-8 11693  df-9 11694  df-n0 11885  df-z 11969  df-dec 12086  df-uz 12231  df-q 12336  df-rp 12377  df-xneg 12494  df-xadd 12495  df-xmul 12496  df-ioo 12729  df-ico 12731  df-icc 12732  df-fz 12883  df-fzo 13024  df-fl 13152  df-seq 13360  df-exp 13420  df-hash 13681  df-cj 14443  df-re 14444  df-im 14445  df-sqrt 14579  df-abs 14580  df-clim 14830  df-rlim 14831  df-sum 15028  df-struct 16468  df-ndx 16469  df-slot 16470  df-base 16472  df-sets 16473  df-ress 16474  df-plusg 16561  df-mulr 16562  df-starv 16563  df-sca 16564  df-vsca 16565  df-ip 16566  df-tset 16567  df-ple 16568  df-ds 16570  df-unif 16571  df-hom 16572  df-cco 16573  df-rest 16679  df-topn 16680  df-0g 16698  df-gsum 16699  df-topgen 16700  df-pt 16701  df-prds 16704  df-xrs 16758  df-qtop 16763  df-imas 16764  df-xps 16766  df-mre 16840  df-mrc 16841  df-acs 16843  df-mgm 17835  df-sgrp 17884  df-mnd 17895  df-submnd 17940  df-mulg 18208  df-cntz 18430  df-cmn 18891  df-psmet 20520  df-xmet 20521  df-met 20522  df-bl 20523  df-mopn 20524  df-fbas 20525  df-fg 20526  df-cnfld 20529  df-top 21485  df-topon 21502  df-topsp 21524  df-bases 21537  df-cld 21610  df-ntr 21611  df-cls 21612  df-nei 21689  df-cn 21818  df-cnp 21819  df-lm 21820  df-haus 21906  df-tx 22153  df-hmeo 22346  df-fil 22437  df-fm 22529  df-flim 22530  df-flf 22531  df-xms 22913  df-ms 22914  df-tms 22915  df-cfil 23841  df-cau 23842  df-cmet 23843  df-grpo 28254  df-gid 28255  df-ginv 28256  df-gdiv 28257  df-ablo 28306  df-vc 28320  df-nv 28353  df-va 28356  df-ba 28357  df-sm 28358  df-0v 28359  df-vs 28360  df-nmcv 28361  df-ims 28362  df-dip 28462  df-ssp 28483  df-ph 28574  df-cbn 28624  df-hnorm 28729  df-hba 28730  df-hvsub 28732  df-hlim 28733  df-hcau 28734  df-sh 28968  df-ch 28982  df-oc 29013  df-ch0 29014  df-shs 29069  df-pjh 29156  df-h0op 29509

This theorem is referenced by:  df0op2  29513  hosubcl  29534  hoaddcom  29535  hoaddass  29543  hocsubdir  29546  hoaddid1i  29547  hodidi  29548  ho0coi  29549  hoaddid1  29552  hodid  29553  ho0subi  29556  ho0sub  29558  hosubid1  29559  honegsub  29560  hoaddsubass  29576  hosd1i  29583  hosubeq0i  29587  0cnop  29740  0hmop  29744  nmop0  29747  hoddi  29751  adj0  29755  nmlnop0iALT  29756  lnopco0i  29765  pjorthcoi  29930