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 e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 -> ( normh ` A ) <_ ( normh ` ( A +h B ) ) ) )

Proof

Step Hyp Ref Expression
1 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
2 1 resqcld 
 |-  ( A e. ~H -> ( ( normh ` A ) ^ 2 ) e. RR )
3 2 recnd 
 |-  ( A e. ~H -> ( ( normh ` A ) ^ 2 ) e. CC )
4 3 addid1d 
 |-  ( A e. ~H -> ( ( ( normh ` A ) ^ 2 ) + 0 ) = ( ( normh ` A ) ^ 2 ) )
5 4 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( normh ` A ) ^ 2 ) + 0 ) = ( ( normh ` A ) ^ 2 ) )
6 normcl 
 |-  ( B e. ~H -> ( normh ` B ) e. RR )
7 6 sqge0d 
 |-  ( B e. ~H -> 0 <_ ( ( normh ` B ) ^ 2 ) )
8 7 adantl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> 0 <_ ( ( normh ` B ) ^ 2 ) )
9 6 resqcld 
 |-  ( B e. ~H -> ( ( normh ` B ) ^ 2 ) e. RR )
10 0re 
 |-  0 e. RR
11 leadd2 
 |-  ( ( 0 e. RR /\ ( ( normh ` B ) ^ 2 ) e. RR /\ ( ( normh ` A ) ^ 2 ) e. RR ) -> ( 0 <_ ( ( normh ` B ) ^ 2 ) <-> ( ( ( normh ` A ) ^ 2 ) + 0 ) <_ ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) ) )
12 10 11 mp3an1 
 |-  ( ( ( ( normh ` B ) ^ 2 ) e. RR /\ ( ( normh ` A ) ^ 2 ) e. RR ) -> ( 0 <_ ( ( normh ` B ) ^ 2 ) <-> ( ( ( normh ` A ) ^ 2 ) + 0 ) <_ ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) ) )
13 9 2 12 syl2anr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( 0 <_ ( ( normh ` B ) ^ 2 ) <-> ( ( ( normh ` A ) ^ 2 ) + 0 ) <_ ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) ) )
14 8 13 mpbid 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( normh ` A ) ^ 2 ) + 0 ) <_ ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )
15 5 14 eqbrtrrd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( normh ` A ) ^ 2 ) <_ ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )
16 15 adantr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( A .ih B ) = 0 ) -> ( ( normh ` A ) ^ 2 ) <_ ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )
17 normpyth 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) ) )
18 17 imp 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( A .ih B ) = 0 ) -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )
19 16 18 breqtrrd 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( A .ih B ) = 0 ) -> ( ( normh ` A ) ^ 2 ) <_ ( ( normh ` ( A +h B ) ) ^ 2 ) )
20 19 ex 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 -> ( ( normh ` A ) ^ 2 ) <_ ( ( normh ` ( A +h B ) ) ^ 2 ) ) )
21 1 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( normh ` A ) e. RR )
22 hvaddcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ~H )
23 normcl 
 |-  ( ( A +h B ) e. ~H -> ( normh ` ( A +h B ) ) e. RR )
24 22 23 syl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( normh ` ( A +h B ) ) e. RR )
25 normge0 
 |-  ( A e. ~H -> 0 <_ ( normh ` A ) )
26 25 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> 0 <_ ( normh ` A ) )
27 normge0 
 |-  ( ( A +h B ) e. ~H -> 0 <_ ( normh ` ( A +h B ) ) )
28 22 27 syl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> 0 <_ ( normh ` ( A +h B ) ) )
29 21 24 26 28 le2sqd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( normh ` A ) <_ ( normh ` ( A +h B ) ) <-> ( ( normh ` A ) ^ 2 ) <_ ( ( normh ` ( A +h B ) ) ^ 2 ) ) )
30 20 29 sylibrd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 -> ( normh ` A ) <_ ( normh ` ( A +h B ) ) ) )