Metamath Proof Explorer

Theorem polid

Description: Polarization identity. Recovers inner product from norm. Exercise 4(a) of ReedSimon p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 . (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 oveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ๐ด ยทih ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) )
2 fvoveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) )
3 2 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) )
4 fvoveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) )
5 4 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) )
6 3 5 oveq12d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) = ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) )
7 fvoveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) )
8 7 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) )
9 fvoveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) )
10 9 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) )
11 8 10 oveq12d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) = ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) )
12 11 oveq2d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( i ยท ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) = ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) )
13 6 12 oveq12d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) = ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) )
14 13 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) = ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )
15 1 14 eqeq12d โŠข ( ๐ด = if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โ†’ ( ( ๐ด ยทih ๐ต ) = ( ( ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) โ†” ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) ) )
16 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
17 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
18 17 fveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) )
19 18 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) )
20 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
21 20 fveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) )
22 21 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) )
23 19 22 oveq12d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) = ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) ) )
24 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( i ยทโ„Ž ๐ต ) = ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) )
25 24 oveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) )
26 25 fveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) )
27 26 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) )
28 24 oveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) = ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) )
29 28 fveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) = ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) )
30 29 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) )
31 27 30 oveq12d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) = ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) ) )
32 31 oveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) = ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) ) ) )
33 23 32 oveq12d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) = ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) ) ) ) )
34 33 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) = ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )
35 16 34 eqeq12d โŠข ( ๐ต = if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โ†’ ( ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih ๐ต ) = ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) โ†” ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) = ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) ) ) ) / 4 ) ) )
36 ifhvhv0 โŠข if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆˆ โ„‹
37 ifhvhv0 โŠข if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) โˆˆ โ„‹
38 36 37 polidi โŠข ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) ยทih if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) = ( ( ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) +โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( if ( ๐ด โˆˆ โ„‹ , ๐ด , 0โ„Ž ) โˆ’โ„Ž ( i ยทโ„Ž if ( ๐ต โˆˆ โ„‹ , ๐ต , 0โ„Ž ) ) ) ) โ†‘ 2 ) ) ) ) / 4 )
39 15 35 38 dedth2h โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทih ๐ต ) = ( ( ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( normโ„Ž โ€˜ ( ๐ด +โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( normโ„Ž โ€˜ ( ๐ด โˆ’โ„Ž ( i ยทโ„Ž ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )