Metamath Proof Explorer

Theorem normpyth

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

Ref Expression
Assertion normpyth ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทih ๐ต ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ๐ด ยทih ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) )
2 1 eqeq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ๐ด ยทih ๐ต ) = 0 โ†” ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = 0 ) )
3 fvoveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) )
4 3 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) )
5 fveq2 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ๐ด ) = ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) )
6 5 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) )
7 6 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) )
8 4 7 eqeq12d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) โ†” ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) ) )
9 2 8 imbi12d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( ๐ด ยทih ๐ต ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) ) โ†” ( ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) ) ) )
10 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
11 10 eqeq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = 0 โ†” ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) = 0 ) )
12 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
13 12 fveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) )
14 13 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) )
15 fveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ๐ต ) = ( normโ„Ž โ€˜ if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
16 15 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) โ†‘ 2 ) )
17 16 oveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) โ†‘ 2 ) ) )
18 14 17 eqeq12d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) โ†” ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) โ†‘ 2 ) ) ) )
19 11 18 imbi12d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) ) โ†” ( ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) โ†‘ 2 ) ) ) ) )
20 ifhvhv0 โŠข if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆˆ โ„‹
21 ifhvhv0 โŠข if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โˆˆ โ„‹
22 20 21 normpythi โŠข ( ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) โ†‘ 2 ) ) )
23 9 19 22 dedth2h โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทih ๐ต ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ๐ต ) โ†‘ 2 ) ) ) )