Metamath Proof Explorer

Theorem pjssdif2i

Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of Halmos p. 48 (shortened with pjssposi ). (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ⊢ 𝐺 ∈ Cℋ
pjco.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjssdif2i ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢ 𝐺 ∈ Cℋ
2 pjco.2 ⊢ 𝐻 ∈ Cℋ
3 2 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
4 1 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
5 hodval ⊢ ( ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ ∧ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
6 3 4 5 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
7 6 adantl ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
8 2 1 pjssmi ⊢ ( 𝑥 ∈ ℋ → ( 𝐺 ⊆ 𝐻 → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ) )
9 8 impcom ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) )
10 7 9 eqtrd ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) )
11 10 ralrimiva ⊢ ( 𝐺 ⊆ 𝐻 → ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) )
12 3 4 hosubfni ⊢ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) Fn ℋ
13 1 choccli ⊢ ( ⊥ ‘ 𝐺 ) ∈ Cℋ
14 2 13 chincli ⊢ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ∈ Cℋ
15 14 pjfni ⊢ ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) Fn ℋ
16 eqfnfv ⊢ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) Fn ℋ ∧ ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) Fn ℋ ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ) )
17 12 15 16 mp2an ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) )
18 11 17 sylibr ⊢ ( 𝐺 ⊆ 𝐻 → ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) )
19 14 pjige0i ⊢ ( 𝑥 ∈ ℋ → 0 ≤ ( ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ·ih 𝑥 ) )
20 19 adantl ⊢ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ∧ 𝑥 ∈ ℋ ) → 0 ≤ ( ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ·ih 𝑥 ) )
21 fveq1 ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) )
22 21 oveq1d ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) → ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ·ih 𝑥 ) )
23 22 adantr ⊢ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ·ih 𝑥 ) )
24 20 23 breqtrrd ⊢ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ∧ 𝑥 ∈ ℋ ) → 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) )
25 24 ralrimiva ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) → ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) )
26 1 2 pjssposi ⊢ ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝐺 ⊆ 𝐻 )
27 25 26 sylib ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) → 𝐺 ⊆ 𝐻 )
28 18 27 impbii ⊢ ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) )