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⋅ihB=0→normℎ⁡A≤normℎ⁡A+ℎB

Proof

Step Hyp Ref Expression
1 normcl ⊢A∈ℋ→normℎ⁡A∈ℝ
2 1 resqcld ⊢A∈ℋ→normℎ⁡A2∈ℝ
3 2 recnd ⊢A∈ℋ→normℎ⁡A2∈ℂ
4 3 addridd ⊢A∈ℋ→normℎ⁡A2+0=normℎ⁡A2
5 4 adantr ⊢A∈ℋ∧B∈ℋ→normℎ⁡A2+0=normℎ⁡A2
6 normcl ⊢B∈ℋ→normℎ⁡B∈ℝ
7 6 sqge0d ⊢B∈ℋ→0≤normℎ⁡B2
8 7 adantl ⊢A∈ℋ∧B∈ℋ→0≤normℎ⁡B2
9 6 resqcld ⊢B∈ℋ→normℎ⁡B2∈ℝ
10 0re ⊢0∈ℝ
11 leadd2 ⊢0∈ℝ∧normℎ⁡B2∈ℝ∧normℎ⁡A2∈ℝ→0≤normℎ⁡B2↔normℎ⁡A2+0≤normℎ⁡A2+normℎ⁡B2
12 10 11 mp3an1 ⊢normℎ⁡B2∈ℝ∧normℎ⁡A2∈ℝ→0≤normℎ⁡B2↔normℎ⁡A2+0≤normℎ⁡A2+normℎ⁡B2
13 9 2 12 syl2anr ⊢A∈ℋ∧B∈ℋ→0≤normℎ⁡B2↔normℎ⁡A2+0≤normℎ⁡A2+normℎ⁡B2
14 8 13 mpbid ⊢A∈ℋ∧B∈ℋ→normℎ⁡A2+0≤normℎ⁡A2+normℎ⁡B2
15 5 14 eqbrtrrd ⊢A∈ℋ∧B∈ℋ→normℎ⁡A2≤normℎ⁡A2+normℎ⁡B2
16 15 adantr ⊢A∈ℋ∧B∈ℋ∧A⋅ihB=0→normℎ⁡A2≤normℎ⁡A2+normℎ⁡B2
17 normpyth ⊢A∈ℋ∧B∈ℋ→A⋅ihB=0→normℎ⁡A+ℎB2=normℎ⁡A2+normℎ⁡B2
18 17 imp ⊢A∈ℋ∧B∈ℋ∧A⋅ihB=0→normℎ⁡A+ℎB2=normℎ⁡A2+normℎ⁡B2
19 16 18 breqtrrd ⊢A∈ℋ∧B∈ℋ∧A⋅ihB=0→normℎ⁡A2≤normℎ⁡A+ℎB2
20 19 ex ⊢A∈ℋ∧B∈ℋ→A⋅ihB=0→normℎ⁡A2≤normℎ⁡A+ℎB2
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ℎ⁡A2≤normℎ⁡A+ℎB2
30 20 29 sylibrd ⊢A∈ℋ∧B∈ℋ→A⋅ihB=0→normℎ⁡A≤normℎ⁡A+ℎB