Metamath Proof Explorer

Theorem pjssdif1i

Description: A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 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 pjssdif1i ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ )

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢ 𝐺 ∈ Cℋ
2 pjco.2 ⊢ 𝐻 ∈ Cℋ
3 1 2 pjssdif2i ⊢ ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) )
4 pjmfn ⊢ projℎ Fn Cℋ
5 1 choccli ⊢ ( ⊥ ‘ 𝐺 ) ∈ Cℋ
6 2 5 chincli ⊢ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ∈ Cℋ
7 fnfvelrn ⊢ ( ( projℎ Fn Cℋ ∧ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ∈ Cℋ ) → ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ∈ ran projℎ )
8 4 6 7 mp2an ⊢ ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ∈ ran projℎ
9 eleq1 ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ ↔ ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ∈ ran projℎ ) )
10 8 9 mpbiri ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) → ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ )
11 fvelrnb ⊢ ( projℎ Fn Cℋ → ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ ↔ ∃ 𝑥 ∈ Cℋ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ) )
12 4 11 ax-mp ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ ↔ ∃ 𝑥 ∈ Cℋ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) )
13 pjige0 ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ ℋ ) → 0 ≤ ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑦 ) ·ih 𝑦 ) )
14 13 adantlr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ ℋ ) → 0 ≤ ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑦 ) ·ih 𝑦 ) )
15 fveq1 ⊢ ( ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝑥 ) ‘ 𝑦 ) = ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) )
16 15 oveq1d ⊢ ( ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) → ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑦 ) ·ih 𝑦 ) = ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) )
17 16 breq2d ⊢ ( ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) → ( 0 ≤ ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑦 ) ·ih 𝑦 ) ↔ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) ) )
18 17 ad2antlr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ ℋ ) → ( 0 ≤ ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑦 ) ·ih 𝑦 ) ↔ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) ) )
19 14 18 mpbid ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ ℋ ) → 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) )
20 19 ralrimiva ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ) → ∀ 𝑦 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) )
21 20 rexlimiva ⊢ ( ∃ 𝑥 ∈ Cℋ ( projℎ ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) → ∀ 𝑦 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) )
22 12 21 sylbi ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ → ∀ 𝑦 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) )
23 1 2 pjssposi ⊢ ( ∀ 𝑦 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) ↔ 𝐺 ⊆ 𝐻 )
24 23 3 bitri ⊢ ( ∀ 𝑦 ∈ ℋ 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ‘ 𝑦 ) ·ih 𝑦 ) ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) )
25 22 24 sylib ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ → ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) )
26 10 25 impbii ⊢ ( ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ )
27 3 26 bitri ⊢ ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) −op ( projℎ ‘ 𝐺 ) ) ∈ ran projℎ )