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 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( ( ( ( ( normh ` ( A +h B ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A .ih B ) = ( if ( A e. ~H , A , 0h ) .ih B ) )
2 fvoveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A +h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) )
3 2 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) )
4 fvoveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A -h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) )
5 4 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) )
6 3 5 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( normh ` ( A +h B ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) = ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) )
7 fvoveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A +h ( _i .h B ) ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) )
8 7 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) )
9 fvoveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A -h ( _i .h B ) ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) )
10 9 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) )
11 8 10 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) = ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) )
12 11 oveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( _i x. ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) ) = ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) )
13 6 12 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( normh ` ( A +h B ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) ) )
14 13 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( ( normh ` ( A +h B ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) = ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) )
15 1 14 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A .ih B ) = ( ( ( ( ( normh ` ( A +h B ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) <-> ( if ( A e. ~H , A , 0h ) .ih B ) = ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) ) )
16 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) .ih B ) = ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) )
17 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) +h B ) = ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) )
18 17 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) )
19 18 oveq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) )
20 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) -h B ) = ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) )
21 20 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) )
22 21 oveq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) )
23 19 22 oveq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) = ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) ) )
24 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( _i .h B ) = ( _i .h if ( B e. ~H , B , 0h ) ) )
25 24 oveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) = ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) )
26 25 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) )
27 26 oveq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) )
28 24 oveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) = ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) )
29 28 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) )
30 29 oveq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) )
31 27 30 oveq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) = ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) ) )
32 31 oveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) = ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) ) ) )
33 23 32 oveq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) ) ) ) )
34 33 oveq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) = ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) ) ) ) / 4 ) )
35 16 34 eqeq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) .ih B ) = ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h B ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) ) ) ) / 4 ) ) )
36 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
37 ifhvhv0 
 |-  if ( B e. ~H , B , 0h ) e. ~H
38 36 37 polidi 
 |-  ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = ( ( ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( if ( A e. ~H , A , 0h ) +h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) - ( ( normh ` ( if ( A e. ~H , A , 0h ) -h ( _i .h if ( B e. ~H , B , 0h ) ) ) ) ^ 2 ) ) ) ) / 4 )
39 15 35 38 dedth2h 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( ( ( ( ( normh ` ( A +h B ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( A +h ( _i .h B ) ) ) ^ 2 ) - ( ( normh ` ( A -h ( _i .h B ) ) ) ^ 2 ) ) ) ) / 4 ) )