Theorem polidt 9021

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 8946.

Assertion

Ref	Expression
polidt	|- ((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 of Theorem polidt

Step	Hyp	Ref	Expression
1		opreq1 3974	. . 3 |- (A = if(A e. H~, A, 0h) -> (A .ih B) = (if(A e. H~, A, 0h) .ih B))
2		opreq1 3974	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (A +h B) = (if(A e. H~, A, 0h) +h B))
3	2	fveq2d 3734	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (normh` (A +h B)) = (normh` (if(A e. H~, A, 0h) +h B)))
4	3	opreq1d 3981	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> ((normh` (A +h B))^2) = ((normh` (if(A e. H~, A, 0h) +h B))^2))
5		opreq1 3974	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (A -h B) = (if(A e. H~, A, 0h) -h B))
6	5	fveq2d 3734	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (normh` (A -h B)) = (normh` (if(A e. H~, A, 0h) -h B)))
7	6	opreq1d 3981	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> ((normh` (A -h B))^2) = ((normh` (if(A e. H~, A, 0h) -h B))^2))
8	4, 7	opreq12d 3984	. . . . 5 |- (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)))
9		opreq1 3974	. . . . . . . . 9 |- (A = if(A e. H~, A, 0h) -> (A +h (i .h B)) = (if(A e. H~, A, 0h) +h (i .h B)))
10	9	fveq2d 3734	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (normh` (A +h (i .h B))) = (normh` (if(A e. H~, A, 0h) +h (i .h B))))
11	10	opreq1d 3981	. . . . . . 7 |- (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))
12		opreq1 3974	. . . . . . . . 9 |- (A = if(A e. H~, A, 0h) -> (A -h (i .h B)) = (if(A e. H~, A, 0h) -h (i .h B)))
13	12	fveq2d 3734	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (normh` (A -h (i .h B))) = (normh` (if(A e. H~, A, 0h) -h (i .h B))))
14	13	opreq1d 3981	. . . . . . 7 |- (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))
15	11, 14	opreq12d 3984	. . . . . 6 |- (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)))
16	15	opreq2d 3982	. . . . 5 |- (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))))
17	8, 16	opreq12d 3984	. . . 4 |- (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)))))
18	17	opreq1d 3981	. . 3 |- (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))
19	1, 18	eqeq12d 1492	. 2 |- (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)))
20		opreq2 3975	. . 3 |- (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)))
21		opreq2 3975	. . . . . . . 8 |- (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)))
22	21	fveq2d 3734	. . . . . . 7 |- (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))))
23	22	opreq1d 3981	. . . . . 6 |- (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))
24		opreq2 3975	. . . . . . . 8 |- (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)))
25	24	fveq2d 3734	. . . . . . 7 |- (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))))
26	25	opreq1d 3981	. . . . . 6 |- (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))
27	23, 26	opreq12d 3984	. . . . 5 |- (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~,