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 ⊢ 𝐺 ∈ Cℋ
pjco.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjorthcoi ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = 0hop )

Proof

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