Metamath Proof Explorer

Theorem normpyc

Description: Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of Beran p. 98. (Contributed by NM, 26-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion normpyc ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 → ( normℎ ‘ 𝐴 ) ≤ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 normcl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
2 1 resqcld ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
3 2 recnd ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
4 3 addid1d ⊢ ( 𝐴 ∈ ℋ → ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + 0 ) = ( ( normℎ ‘ 𝐴 ) ↑ 2 ) )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + 0 ) = ( ( normℎ ‘ 𝐴 ) ↑ 2 ) )
6 normcl ⊢ ( 𝐵 ∈ ℋ → ( normℎ ‘ 𝐵 ) ∈ ℝ )
7 6 sqge0d ⊢ ( 𝐵 ∈ ℋ → 0 ≤ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) )
8 7 adantl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → 0 ≤ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) )
9 6 resqcld ⊢ ( 𝐵 ∈ ℋ → ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ∈ ℝ )
10 0re ⊢ 0 ∈ ℝ
11 leadd2 ⊢ ( ( 0 ∈ ℝ ∧ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ∈ ℝ ) → ( 0 ≤ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ↔ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + 0 ) ≤ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ) )
12 10 11 mp3an1 ⊢ ( ( ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ∈ ℝ ) → ( 0 ≤ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ↔ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + 0 ) ≤ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ) )
13 9 2 12 syl2anr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 0 ≤ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ↔ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + 0 ) ≤ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ) )
14 8 13 mpbid ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + 0 ) ≤ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )
15 5 14 eqbrtrrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ≤ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )
16 15 adantr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐴 ·ih 𝐵 ) = 0 ) → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ≤ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )
17 normpyth ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) = ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ) )
18 17 imp ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐴 ·ih 𝐵 ) = 0 ) → ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) = ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )
19 16 18 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐴 ·ih 𝐵 ) = 0 ) → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ≤ ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) )
20 19 ex ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ≤ ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) ) )
21 1 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( normℎ ‘ 𝐴 ) ∈ ℝ )
22 hvaddcl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ )
23 normcl ⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ → ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ ℝ )
24 22 23 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ ℝ )
25 normge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
26 25 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → 0 ≤ ( normℎ ‘ 𝐴 ) )
27 normge0 ⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) )
28 22 27 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → 0 ≤ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) )
29 21 24 26 28 le2sqd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( normℎ ‘ 𝐴 ) ≤ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↔ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) ≤ ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) ) )
30 20 29 sylibrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 → ( normℎ ‘ 𝐴 ) ≤ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ) )