Metamath Proof Explorer

Theorem pjorthcoi

Description: Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of Halmos p. 45. (Contributed by NM, 6-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ⊢G∈Cℋ
pjco.2 ⊢H∈Cℋ
Assertion pjorthcoi ⊢G⊆⊥⁡H→projℎ⁡G∘projℎ⁡H=0hop

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢G∈Cℋ
2 pjco.2 ⊢H∈Cℋ
3 2 pjcli ⊢x∈ℋ→projℎ⁡H⁡x∈H
4 1 2 chsscon2i ⊢G⊆⊥⁡H↔H⊆⊥⁡G
5 ssel ⊢H⊆⊥⁡G→projℎ⁡H⁡x∈H→projℎ⁡H⁡x∈⊥⁡G
6 4 5 sylbi ⊢G⊆⊥⁡H→projℎ⁡H⁡x∈H→projℎ⁡H⁡x∈⊥⁡G
7 3 6 syl5com ⊢x∈ℋ→G⊆⊥⁡H→projℎ⁡H⁡x∈⊥⁡G
8 2 pjhcli ⊢x∈ℋ→projℎ⁡H⁡x∈ℋ
9 pjoc2 ⊢G∈Cℋ∧projℎ⁡H⁡x∈ℋ→projℎ⁡H⁡x∈⊥⁡G↔projℎ⁡G⁡projℎ⁡H⁡x=0ℎ
10 1 8 9 sylancr ⊢x∈ℋ→projℎ⁡H⁡x∈⊥⁡G↔projℎ⁡G⁡projℎ⁡H⁡x=0ℎ
11 7 10 sylibd ⊢x∈ℋ→G⊆⊥⁡H→projℎ⁡G⁡projℎ⁡H⁡x=0ℎ
12 11 impcom ⊢G⊆⊥⁡H∧x∈ℋ→projℎ⁡G⁡projℎ⁡H⁡x=0ℎ
13 1 2 pjcoi ⊢x∈ℋ→projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡projℎ⁡H⁡x
14 13 adantl ⊢G⊆⊥⁡H∧x∈ℋ→projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡projℎ⁡H⁡x
15 ho0val ⊢x∈ℋ→0hop⁡x=0ℎ
16 15 adantl ⊢G⊆⊥⁡H∧x∈ℋ→0hop⁡x=0ℎ
17 12 14 16 3eqtr4d ⊢G⊆⊥⁡H∧x∈ℋ→projℎ⁡G∘projℎ⁡H⁡x=0hop⁡x
18 17 ralrimiva ⊢G⊆⊥⁡H→∀x∈ℋprojℎ⁡G∘projℎ⁡H⁡x=0hop⁡x
19 1 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
20 2 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
21 19 20 hocofi ⊢projℎ⁡G∘projℎ⁡H:ℋ⟶ℋ
22 ho0f ⊢0hop:ℋ⟶ℋ
23 21 22 hoeqi ⊢∀x∈ℋprojℎ⁡G∘projℎ⁡H⁡x=0hop⁡x↔projℎ⁡G∘projℎ⁡H=0hop
24 18 23 sylib ⊢G⊆⊥⁡H→projℎ⁡G∘projℎ⁡H=0hop