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 addridd โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( ( 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โ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) ) )