Metamath Proof Explorer

Theorem ho0val

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.)

Ref Expression
Assertion ho0val ⊢A∈ℋ→0hop⁡A=0ℎ

Proof

Step Hyp Ref Expression
1 choc1 ⊢⊥⁡ℋ=0ℋ
2 1 fveq2i ⊢projℎ⁡⊥⁡ℋ=projℎ⁡0ℋ
3 df-h0op ⊢0hop=projℎ⁡0ℋ
4 2 3 eqtr4i ⊢projℎ⁡⊥⁡ℋ=0hop
5 4 fveq1i ⊢projℎ⁡⊥⁡ℋ⁡A=0hop⁡A
6 helch ⊢ℋ∈Cℋ
7 pjo ⊢ℋ∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡ℋ⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A
8 6 7 mpan ⊢A∈ℋ→projℎ⁡⊥⁡ℋ⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A
9 5 8 eqtr3id ⊢A∈ℋ→0hop⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A
10 6 pjhcli ⊢A∈ℋ→projℎ⁡ℋ⁡A∈ℋ
11 hvsubid ⊢projℎ⁡ℋ⁡A∈ℋ→projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A=0ℎ
12 10 11 syl ⊢A∈ℋ→projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A=0ℎ
13 9 12 eqtrd ⊢A∈ℋ→0hop⁡A=0ℎ