Theorem ho0val 31792

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 31369	. . . . . 6 ⊢ (⊥‘ ℋ) = 0ℋ
2	1	fveq2i 6914	. . . . 5 ⊢ (projℎ‘(⊥‘ ℋ)) = (projℎ‘0ℋ)
3		df-h0op 31790	. . . . 5 ⊢ 0hop = (projℎ‘0ℋ)
4	2, 3	eqtr4i 2767	. . . 4 ⊢ (projℎ‘(⊥‘ ℋ)) = 0hop
5	4	fveq1i 6912	. . 3 ⊢ ((projℎ‘(⊥‘ ℋ))‘𝐴) = ( 0hop ‘𝐴)
6		helch 31285	. . . 4 ⊢ ℋ ∈ Cℋ
7		pjo 31713	. . . 4 ⊢ (( ℋ ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘ ℋ))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)))
8	6, 7	mpan 690	. . 3 ⊢ (𝐴 ∈ ℋ → ((projℎ‘(⊥‘ ℋ))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)))
9	5, 8	eqtr3id 2790	. 2 ⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)))
10	6	pjhcli 31460	. . 3 ⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) ∈ ℋ)
11		hvsubid 31068	. . 3 ⊢ (((projℎ‘ ℋ)‘𝐴) ∈ ℋ → (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)) = 0ℎ)
12	10, 11	syl 17	. 2 ⊢ (𝐴 ∈ ℋ → (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘ ℋ)‘𝐴)) = 0ℎ)
13	9, 12	eqtrd 2776	1 ⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = 0ℎ)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2107  ‘cfv 6566  (class class class)co 7435   ℋchba 30961  0_ℎc0v 30966   −_ℎ cmv 30967   C_ℋ cch 30971  ⊥cort 30972  0_ℋc0h 30977  proj_ℎcpjh 30979   0_hop ch0o 30985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5286  ax-sep 5303  ax-nul 5313  ax-pow 5372  ax-pr 5439  ax-un 7758  ax-inf2 9685  ax-cc 10479  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236  ax-pre-sup 11237  ax-addf 11238  ax-mulf 11239  ax-hilex 31041  ax-hfvadd 31042  ax-hvcom 31043  ax-hvass 31044  ax-hv0cl 31045  ax-hvaddid 31046  ax-hfvmul 31047  ax-hvmulid 31048  ax-hvmulass 31049  ax-hvdistr1 31050  ax-hvdistr2 31051  ax-hvmul0 31052  ax-hfi 31121  ax-his1 31124  ax-his2 31125  ax-his3 31126  ax-his4 31127  ax-hcompl 31244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3435  df-v 3481  df-sbc 3793  df-csb 3910  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-pss 3984  df-nul 4341  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4914  df-int 4953  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5642  df-se 5643  df-we 5644  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-rn 5701  df-res 5702  df-ima 5703  df-pred 6326  df-ord 6392  df-on 6393  df-lim 6394  df-suc 6395  df-iota 6519  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7392  df-ov 7438  df-oprab 7439  df-mpo 7440  df-of 7701  df-om 7892  df-1st 8019  df-2nd 8020  df-supp 8191  df-frecs 8311  df-wrecs 8342  df-recs 8416  df-rdg 8455  df-1o 8511  df-2o 8512  df-oadd 8515  df-omul 8516  df-er 8750  df-map 8873  df-pm 8874  df-ixp 8943  df-en 8991  df-dom 8992  df-sdom 8993  df-fin 8994  df-fsupp 9406  df-fi 9455  df-sup 9486  df-inf 9487  df-oi 9554  df-card 9983  df-acn 9986  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11498  df-neg 11499  df-div 11925  df-nn 12271  df-2 12333  df-3 12334  df-4 12335  df-5 12336  df-6 12337  df-7 12338  df-8 12339  df-9 12340  df-n0 12531  df-z 12618  df-dec 12738  df-uz 12883  df-q 12995  df-rp 13039  df-xneg 13158  df-xadd 13159  df-xmul 13160  df-ioo 13394  df-ico 13396  df-icc 13397  df-fz 13551  df-fzo 13698  df-fl 13835  df-seq 14046  df-exp 14106  df-hash 14373  df-cj 15141  df-re 15142  df-im 15143  df-sqrt 15277  df-abs 15278  df-clim 15527  df-rlim 15528  df-sum 15726  df-struct 17187  df-sets 17204  df-slot 17222  df-ndx 17234  df-base 17252  df-ress 17281  df-plusg 17317  df-mulr 17318  df-starv 17319  df-sca 17320  df-vsca 17321  df-ip 17322  df-tset 17323  df-ple 17324  df-ds 17326  df-unif 17327  df-hom 17328  df-cco 17329  df-rest 17475  df-topn 17476  df-0g 17494  df-gsum 17495  df-topgen 17496  df-pt 17497  df-prds 17500  df-xrs 17555  df-qtop 17560  df-imas 17561  df-xps 17563  df-mre 17637  df-mrc 17638  df-acs 17640  df-mgm 18672  df-sgrp 18751  df-mnd 18767  df-submnd 18816  df-mulg 19105  df-cntz 19354  df-cmn 19821  df-psmet 21380  df-xmet 21381  df-met 21382  df-bl 21383  df-mopn 21384  df-fbas 21385  df-fg 21386  df-cnfld 21389  df-top 22922  df-topon 22939  df-topsp 22961  df-bases 22975  df-cld 23049  df-ntr 23050  df-cls 23051  df-nei 23128  df-cn 23257  df-cnp 23258  df-lm 23259  df-haus 23345  df-tx 23592  df-hmeo 23785  df-fil 23876  df-fm 23968  df-flim 23969  df-flf 23970  df-xms 24352  df-ms 24353  df-tms 24354  df-cfil 25311  df-cau 25312  df-cmet 25313  df-grpo 30535  df-gid 30536  df-ginv 30537  df-gdiv 30538  df-ablo 30587  df-vc 30601  df-nv 30634  df-va 30637  df-ba 30638  df-sm 30639  df-0v 30640  df-vs 30641  df-nmcv 30642  df-ims 30643  df-dip 30743  df-ssp 30764  df-ph 30855  df-cbn 30905  df-hnorm 31010  df-hba 31011  df-hvsub 31013  df-hlim 31014  df-hcau 31015  df-sh 31249  df-ch 31263  df-oc 31294  df-ch0 31295  df-shs 31350  df-pjh 31437  df-h0op 31790

This theorem is referenced by:  df0op2  31794  hoaddridi  31828  ho0coi  31830  0cnop  32021  0hmop  32025  nmop0  32028  adj0  32036  nmlnop0iALT  32037  lnopco0i  32046  lnopeq0i  32049  nmopcoi  32137  leop3  32167  leoprf2  32169  leoprf  32170  idleop  32173  pjorthcoi  32211