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 0 hop A = 0

Proof

Step Hyp Ref Expression
1 choc1 = 0
2 1 fveq2i proj = proj 0
3 df-h0op 0 hop = proj 0
4 2 3 eqtr4i proj = 0 hop
5 4 fveq1i proj A = 0 hop 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 0 hop 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 0 hop A = 0