This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )