Theorem ho0val 31909

Description: Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
ho0val	⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = 0ℎ)

Proof of Theorem ho0val

Step	Hyp	Ref	Expression
1		choc1 31486	. . . . . 6 ⊢ (⊥‘ ℋ) = 0ℋ
2	1	fveq2i 6864	. . . . 5 ⊢ (projℎ‘(⊥‘ ℋ)) = (projℎ‘0ℋ)
3		df-h0op 31907	. . . . 5 ⊢ 0hop = (projℎ‘0ℋ)
4	2, 3	eqtr4i 2787	. . . 4 ⊢ (projℎ‘(⊥‘ ℋ)) = 0hop
5	4	fveq1i 6862	. . 3 ⊢ ((projℎ‘(⊥‘ ℋ))‘𝐴) = ( 0hop ‘𝐴)
6		helch 31402	. . . 4 ⊢ ℋ ∈ Cℋ
7		pjo 31830	. . . 4 ⊢ (( ℋ ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘ ℋ))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)))
8	6, 7	mpan 700	. . 3 ⊢ (𝐴 ∈ ℋ → ((projℎ‘(⊥‘ ℋ))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)))
9	5, 8	eqtr3id 2810	. 2 ⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)))
10	6	pjhcli 31577	. . 3 ⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) ∈ ℋ)
11		hvsubid 31185	. . 3 ⊢ (((projℎ‘ ℋ)‘𝐴) ∈ ℋ → (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)) = 0ℎ)
12	10, 11	syl 17	. 2 ⊢ (𝐴 ∈ ℋ → (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)) = 0ℎ)
13	9, 12	eqtrd 2796	1 ⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = 0ℎ)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  ‘cfv 6515  (class class class)co 7390   ℋchba 31078  0_ℎc0v 31083   −_ℎ cmv 31084   C_ℋ cch 31088  ⊥cort 31089  0_ℋc0h 31094  proj_ℎcpjh 31096   0_hop ch0o 31102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-inf2 9589  ax-cc 10385  ax-cnex 11122  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142  ax-pre-mulgt0 11143  ax-pre-sup 11144  ax-addf 11145  ax-mulf 11146  ax-hilex 31158  ax-hfvadd 31159  ax-hvcom 31160  ax-hvass 31161  ax-hv0cl 31162  ax-hvaddid 31163  ax-hfvmul 31164  ax-hvmulid 31165  ax-hvmulass 31166  ax-hvdistr1 31167  ax-hvdistr2 31168  ax-hvmul0 31169  ax-hfi 31238  ax-his1 31241  ax-his2 31242  ax-his3 31243  ax-his4 31244  ax-hcompl 31361

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-isom 6524  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7654  df-om 7841  df-1st 7964  df-2nd 7965  df-supp 8134  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-1o 8430  df-2o 8431  df-oadd 8434  df-omul 8435  df-er 8671  df-map 8803  df-pm 8804  df-ixp 8873  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-fsupp 9301  df-fi 9350  df-sup 9381  df-inf 9382  df-oi 9451  df-card 9890  df-acn 9893  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-sub 11409  df-neg 11410  df-div 11838  df-nn 12204  df-2 12273  df-3 12274  df-4 12275  df-5 12276  df-6 12277  df-7 12278  df-8 12279  df-9 12280  df-n0 12475  df-z 12562  df-dec 12682  df-uz 12833  df-q 12943  df-rp 12987  df-xneg 13107  df-xadd 13108  df-xmul 13109  df-ioo 13346  df-ico 13348  df-icc 13349  df-fz 13506  df-fzo 13653  df-fl 13795  df-seq 14008  df-exp 14068  df-hash 14337  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-clim 15505  df-rlim 15506  df-sum 15704  df-struct 17173  df-sets 17190  df-slot 17208  df-ndx 17220  df-base 17236  df-ress 17257  df-plusg 17289  df-mulr 17290  df-starv 17291  df-sca 17292  df-vsca 17293  df-ip 17294  df-tset 17295  df-ple 17296  df-ds 17298  df-unif 17299  df-hom 17300  df-cco 17301  df-rest 17441  df-topn 17442  df-0g 17460  df-gsum 17461  df-topgen 17462  df-pt 17463  df-prds 17466  df-xrs 17522  df-qtop 17527  df-imas 17528  df-xps 17530  df-mre 17604  df-mrc 17605  df-acs 17607  df-mgm 18664  df-sgrp 18743  df-mnd 18759  df-submnd 18808  df-mulg 19100  df-cntz 19347  df-cmn 19812  df-psmet 21403  df-xmet 21404  df-met 21405  df-bl 21406  df-mopn 21407  df-fbas 21408  df-fg 21409  df-cnfld 21412  df-top 22941  df-topon 22958  df-topsp 22980  df-bases 22993  df-cld 23066  df-ntr 23067  df-cls 23068  df-nei 23145  df-cn 23274  df-cnp 23275  df-lm 23276  df-haus 23362  df-tx 23609  df-hmeo 23802  df-fil 23893  df-fm 23985  df-flim 23986  df-flf 23987  df-xms 24367  df-ms 24368  df-tms 24369  df-cfil 25304  df-cau 25305  df-cmet 25306  df-grpo 30652  df-gid 30653  df-ginv 30654  df-gdiv 30655  df-ablo 30704  df-vc 30718  df-nv 30751  df-va 30754  df-ba 30755  df-sm 30756  df-0v 30757  df-vs 30758  df-nmcv 30759  df-ims 30760  df-dip 30860  df-ssp 30881  df-ph 30972  df-cbn 31022  df-hnorm 31127  df-hba 31128  df-hvsub 31130  df-hlim 31131  df-hcau 31132  df-sh 31366  df-ch 31380  df-oc 31411  df-ch0 31412  df-shs 31467  df-pjh 31554  df-h0op 31907

This theorem is referenced by:  df0op2  31911  hoaddridi  31945  ho0coi  31947  0cnop  32138  0hmop  32142  nmop0  32145  adj0  32153  nmlnop0iALT  32154  lnopco0i  32163  lnopeq0i  32166  nmopcoi  32254  leop3  32284  leoprf2  32286  leoprf  32287  idleop  32290  pjorthcoi  32328