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 )