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