Metamath Proof Explorer


Theorem pjoc1i

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

Ref Expression
Hypotheses pjop.1 H C
pjop.2 A
Assertion pjoc1i A H proj H A = 0

Proof

Step Hyp Ref Expression
1 pjop.1 H C
2 pjop.2 A
3 1 2 pjopi proj H A = A - proj H A
4 1 chshii H S
5 1 2 pjclii proj H A H
6 shsubcl H S A H proj H A H A - proj H A H
7 4 5 6 mp3an13 A H A - proj H A H
8 3 7 eqeltrid A H proj H A H
9 1 choccli H C
10 9 2 pjclii proj H A H
11 8 10 jctir A H proj H A H proj H A H
12 elin proj H A H H proj H A H proj H A H
13 11 12 sylibr A H proj H A H H
14 ocin H S H H = 0
15 4 14 ax-mp H H = 0
16 13 15 eleqtrdi A H proj H A 0
17 elch0 proj H A 0 proj H A = 0
18 16 17 sylib A H proj H A = 0
19 1 2 pjpji A = proj H A + proj H A
20 oveq2 proj H A = 0 proj H A + proj H A = proj H A + 0
21 19 20 syl5eq proj H A = 0 A = proj H A + 0
22 1 2 pjhclii proj H A
23 ax-hvaddid proj H A proj H A + 0 = proj H A
24 22 23 ax-mp proj H A + 0 = proj H A
25 21 24 eqtrdi proj H A = 0 A = proj H A
26 25 5 eqeltrdi proj H A = 0 A H
27 18 26 impbii A H proj H A = 0