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 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 → norm ℎ ⁡ A ≤ norm ℎ ⁡ A + ℎ B

Proof

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