Metamath Proof Explorer

Theorem pjtoi

Description: Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjidmco.1 ⊢H∈Cℋ
Assertion pjtoi ⊢projℎ⁡H+opprojℎ⁡⊥⁡H=projℎ⁡ℋ

Proof

Step Hyp Ref Expression
1 pjidmco.1 ⊢H∈Cℋ
2 axpjpj ⊢H∈Cℋ∧x∈ℋ→x=projℎ⁡H⁡x+ℎprojℎ⁡⊥⁡H⁡x
3 1 2 mpan ⊢x∈ℋ→x=projℎ⁡H⁡x+ℎprojℎ⁡⊥⁡H⁡x
4 pjch1 ⊢x∈ℋ→projℎ⁡ℋ⁡x=x
5 1 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
6 1 choccli ⊢⊥⁡H∈Cℋ
7 6 pjfi ⊢projℎ⁡⊥⁡H:ℋ⟶ℋ
8 hosval ⊢projℎ⁡H:ℋ⟶ℋ∧projℎ⁡⊥⁡H:ℋ⟶ℋ∧x∈ℋ→projℎ⁡H+opprojℎ⁡⊥⁡H⁡x=projℎ⁡H⁡x+ℎprojℎ⁡⊥⁡H⁡x
9 5 7 8 mp3an12 ⊢x∈ℋ→projℎ⁡H+opprojℎ⁡⊥⁡H⁡x=projℎ⁡H⁡x+ℎprojℎ⁡⊥⁡H⁡x
10 3 4 9 3eqtr4rd ⊢x∈ℋ→projℎ⁡H+opprojℎ⁡⊥⁡H⁡x=projℎ⁡ℋ⁡x
11 10 rgen ⊢∀x∈ℋprojℎ⁡H+opprojℎ⁡⊥⁡H⁡x=projℎ⁡ℋ⁡x
12 5 7 hoaddcli ⊢projℎ⁡H+opprojℎ⁡⊥⁡H:ℋ⟶ℋ
13 helch ⊢ℋ∈Cℋ
14 13 pjfi ⊢projℎ⁡ℋ:ℋ⟶ℋ
15 12 14 hoeqi ⊢∀x∈ℋprojℎ⁡H+opprojℎ⁡⊥⁡H⁡x=projℎ⁡ℋ⁡x↔projℎ⁡H+opprojℎ⁡⊥⁡H=projℎ⁡ℋ
16 11 15 mpbi ⊢projℎ⁡H+opprojℎ⁡⊥⁡H=projℎ⁡ℋ