Metamath Proof Explorer

Theorem pjop

Description: Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axpjpj ⊢H∈Cℋ∧A∈ℋ→A=projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A
2 1 eqcomd ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A=A
3 simpr ⊢H∈Cℋ∧A∈ℋ→A∈ℋ
4 pjhcl ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A∈ℋ
5 choccl ⊢H∈Cℋ→⊥⁡H∈Cℋ
6 pjhcl ⊢⊥⁡H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A∈ℋ
7 5 6 sylan ⊢H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A∈ℋ
8 hvsubadd ⊢A∈ℋ∧projℎ⁡H⁡A∈ℋ∧projℎ⁡⊥⁡H⁡A∈ℋ→A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡H⁡A↔projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A=A
9 3 4 7 8 syl3anc ⊢H∈Cℋ∧A∈ℋ→A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡H⁡A↔projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A=A
10 2 9 mpbird ⊢H∈Cℋ∧A∈ℋ→A-ℎprojℎ⁡H⁡A=projℎ⁡⊥⁡H⁡A
11 10 eqcomd ⊢H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A=A-ℎprojℎ⁡H⁡A