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 eqtrid ⊢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ℎ