Metamath Proof Explorer

Theorem polidi

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, 30-Jun-2005) (New usage is discouraged.)

Ref Expression
Hypotheses polid.1 ⊢ 𝐴 ∈ ℋ
polid.2 ⊢ 𝐵 ∈ ℋ
Assertion polidi ( 𝐴 ·ih 𝐵 ) = ( ( ( ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 )

Proof

Step Hyp Ref Expression
1 polid.1 ⊢ 𝐴 ∈ ℋ
2 polid.2 ⊢ 𝐵 ∈ ℋ
3 1 2 2 1 polid2i ⊢ ( 𝐴 ·ih 𝐵 ) = ( ( ( ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )
4 1 2 hvaddcli ⊢ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ
5 4 normsqi ⊢ ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) )
6 1 2 hvsubcli ⊢ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ
7 6 normsqi ⊢ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) )
8 5 7 oveq12i ⊢ ( ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) )
9 ax-icn ⊢ i ∈ ℂ
10 9 2 hvmulcli ⊢ ( i ·ℎ 𝐵 ) ∈ ℋ
11 1 10 hvaddcli ⊢ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ∈ ℋ
12 11 normsqi ⊢ ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) )
13 1 10 hvsubcli ⊢ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ∈ ℋ
14 13 normsqi ⊢ ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) )
15 12 14 oveq12i ⊢ ( ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) )
16 15 oveq2i ⊢ ( i · ( ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) ) ) = ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) )
17 8 16 oveq12i ⊢ ( ( ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) )
18 17 oveq1i ⊢ ( ( ( ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( ( ( ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ·ih ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )
19 3 18 eqtr4i ⊢ ( 𝐴 ·ih 𝐵 ) = ( ( ( ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝐴 +ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ ( i ·ℎ 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 )