Metamath Proof Explorer

Theorem pjo

Description: The orthogonal projection. Lemma 4.4(i) of Beran p. 111. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion pjo ⊢H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A

Proof

Step Hyp Ref Expression
1 pjch1 ⊢A∈ℋ→projℎ⁡ℋ⁡A=A
2 1 adantl ⊢H∈Cℋ∧A∈ℋ→projℎ⁡ℋ⁡A=A
3 axpjpj ⊢H∈Cℋ∧A∈ℋ→A=projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A
4 2 3 eqtr2d ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A
5 helch ⊢ℋ∈Cℋ
6 5 pjcli ⊢A∈ℋ→projℎ⁡ℋ⁡A∈ℋ
7 6 adantl ⊢H∈Cℋ∧A∈ℋ→projℎ⁡ℋ⁡A∈ℋ
8 pjhcl ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A∈ℋ
9 choccl ⊢H∈Cℋ→⊥⁡H∈Cℋ
10 pjhcl ⊢⊥⁡H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A∈ℋ
11 9 10 sylan ⊢H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A∈ℋ
12 hvsubadd ⊢projℎ⁡ℋ⁡A∈ℋ∧projℎ⁡H⁡A∈ℋ∧projℎ⁡⊥⁡H⁡A∈ℋ→projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡H⁡A↔projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A
13 7 8 11 12 syl3anc ⊢H∈Cℋ∧A∈ℋ→projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡H⁡A↔projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A
14 4 13 mpbird ⊢H∈Cℋ∧A∈ℋ→projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡H⁡A
15 14 eqcomd ⊢H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A