Metamath Proof Explorer


Theorem pjoc1

Description: Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 6-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjoc1 H C A A H proj H A = 0

Proof

Step Hyp Ref Expression
1 eleq2 H = if H C H A H A if H C H
2 2fveq3 H = if H C H proj H = proj if H C H
3 2 fveq1d H = if H C H proj H A = proj if H C H A
4 3 eqeq1d H = if H C H proj H A = 0 proj if H C H A = 0
5 1 4 bibi12d H = if H C H A H proj H A = 0 A if H C H proj if H C H A = 0
6 eleq1 A = if A A 0 A if H C H if A A 0 if H C H
7 fveqeq2 A = if A A 0 proj if H C H A = 0 proj if H C H if A A 0 = 0
8 6 7 bibi12d A = if A A 0 A if H C H proj if H C H A = 0 if A A 0 if H C H proj if H C H if A A 0 = 0
9 ifchhv if H C H C
10 ifhvhv0 if A A 0
11 9 10 pjoc1i if A A 0 if H C H proj if H C H if A A 0 = 0
12 5 8 11 dedth2h H C A A H proj H A = 0