Metamath Proof Explorer


Theorem pjssge0ii

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 𝐻C
pjidm.2 𝐴 ∈ ℋ
pjsslem.1 𝐺C
Assertion pjssge0ii ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → 0 ≤ ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 𝐻C
2 pjidm.2 𝐴 ∈ ℋ
3 pjsslem.1 𝐺C
4 1 choccli ( ⊥ ‘ 𝐻 ) ∈ C
5 3 4 chincli ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ∈ C
6 5 2 pjhclii ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ∈ ℋ
7 6 normcli ( norm ‘ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ∈ ℝ
8 7 sqge0i 0 ≤ ( ( norm ‘ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↑ 2 )
9 oveq1 ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ·ih 𝐴 ) )
10 5 2 pjinormii ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( norm ‘ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↑ 2 )
11 9 10 eqtrdi ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( norm ‘ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) ↑ 2 ) )
12 8 11 breqtrrid ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) → 0 ≤ ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) )