Metamath Proof Explorer


Theorem pjige0

Description: The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion pjige0 H C A 0 proj H A ih A

Proof

Step Hyp Ref Expression
1 fveq2 H = if H C H 0 proj H = proj if H C H 0
2 1 fveq1d H = if H C H 0 proj H A = proj if H C H 0 A
3 2 oveq1d H = if H C H 0 proj H A ih A = proj if H C H 0 A ih A
4 3 breq2d H = if H C H 0 0 proj H A ih A 0 proj if H C H 0 A ih A
5 4 imbi2d H = if H C H 0 A 0 proj H A ih A A 0 proj if H C H 0 A ih A
6 h0elch 0 C
7 6 elimel if H C H 0 C
8 7 pjige0i A 0 proj if H C H 0 A ih A
9 5 8 dedth H C A 0 proj H A ih A
10 9 imp H C A 0 proj H A ih A