Metamath Proof Explorer


Theorem pjdifnormii

Description: Theorem 4.5(v)<->(vi) 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 pjdifnormii ( 0 ≤ ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ↔ ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 𝐻C
2 pjidm.2 𝐴 ∈ ℋ
3 pjsslem.1 𝐺C
4 3 2 pjhclii ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ℋ
5 4 normcli ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ∈ ℝ
6 5 resqcli ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ
7 1 2 pjhclii ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ℋ
8 7 normcli ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ℝ
9 8 resqcli ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ
10 6 9 subge0i ( 0 ≤ ( ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) ↔ ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ≤ ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) )
11 his2sub ( ( ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) − ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) ) )
12 4 7 2 11 mp3an ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) − ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) )
13 3 2 pjinormii ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 )
14 1 2 pjinormii ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 )
15 13 14 oveq12i ( ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih 𝐴 ) − ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) ) = ( ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) )
16 12 15 eqtri ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) = ( ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) )
17 16 breq2i ( 0 ≤ ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ↔ 0 ≤ ( ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) − ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) )
18 normge0 ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) )
19 7 18 ax-mp 0 ≤ ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) )
20 normge0 ( ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) )
21 4 20 ax-mp 0 ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) )
22 8 5 le2sqi ( ( 0 ≤ ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ∧ 0 ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ) → ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↔ ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ≤ ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) )
23 19 21 22 mp2an ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↔ ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ≤ ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) )
24 10 17 23 3bitr4i ( 0 ≤ ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ·ih 𝐴 ) ↔ ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ≤ ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) )