Metamath Proof Explorer

Theorem pjssposi

Description: Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of Halmos p. 48. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ⊢ 𝐺 ∈ Cℋ
pjco.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjssposi ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝐺 ⊆ 𝐻 )

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢ 𝐺 ∈ Cℋ
2 pjco.2 ⊢ 𝐻 ∈ Cℋ
3 2 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ ℋ )
4 normcl ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ∈ ℝ )
5 3 4 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ∈ ℝ )
6 5 resqcld ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) ∈ ℝ )
7 1 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ )
8 normcl ⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ )
9 7 8 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ )
10 9 resqcld ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ∈ ℝ )
11 6 10 subge0d ⊢ ( 𝑥 ∈ ℋ → ( 0 ≤ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) ) )
12 2 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
13 1 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
14 hodval ⊢ ( ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ ∧ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
15 12 13 14 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
16 15 oveq1d ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ·ih 𝑥 ) )
17 id ⊢ ( 𝑥 ∈ ℋ → 𝑥 ∈ ℋ )
18 his2sub ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑥 ) − ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
19 3 7 17 18 syl3anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑥 ) − ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
20 2 pjinormi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) )
21 1 pjinormi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) )
22 20 21 oveq12d ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑥 ) − ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ·ih 𝑥 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ) )
23 16 19 22 3eqtrd ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ) )
24 23 breq2d ⊢ ( 𝑥 ∈ ℋ → ( 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) − ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ) ) )
25 normge0 ⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
26 7 25 syl ⊢ ( 𝑥 ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
27 normge0 ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
28 3 27 syl ⊢ ( 𝑥 ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
29 9 5 26 28 le2sqd ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↑ 2 ) ) )
30 11 24 29 3bitr4d ⊢ ( 𝑥 ∈ ℋ → ( 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
31 30 ralbiia ⊢ ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
32 1 2 pjnormssi ⊢ ( 𝐺 ⊆ 𝐻 ↔ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
33 31 32 bitr4i ⊢ ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝐺 ⊆ 𝐻 )