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 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = norm ℎ ⁡ A + ℎ B 2 - norm ℎ ⁡ A - ℎ B 2 + i ⁢ norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 4

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih B
2 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B
3 2 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2
4 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
5 4 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2
6 3 5 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 − norm ℎ ⁡ A - ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2
7 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ i ⋅ ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B
8 7 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2
9 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ i ⋅ ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B
10 9 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2
11 8 10 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2
12 11 oveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → i ⁢ norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 = i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2
13 6 12 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 - norm ℎ ⁡ A - ℎ B 2 + i ⁢ norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2
14 13 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 - norm ℎ ⁡ A - ℎ B 2 + i ⁢ norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 4 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 4
15 1 14 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = norm ℎ ⁡ A + ℎ B 2 - norm ℎ ⁡ A - ℎ B 2 + i ⁢ norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 4 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 4
16 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
17 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
18 17 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
19 18 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2
20 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
21 20 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
22 21 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2
23 19 22 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2
24 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → i ⋅ ℎ B = i ⋅ ℎ if B ∈ ℋ B 0 ℎ
25 24 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B = if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
26 25 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
27 26 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2
28 24 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
29 28 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ
30 29 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2
31 27 30 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2
32 31 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 = i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2
33 23 32 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2
34 33 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 4 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 4
35 16 34 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ B 2 4 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 4
36 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
37 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
38 36 37 polidi ⊢ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 - norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ 2 + i ⁢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 − norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ i ⋅ ℎ if B ∈ ℋ B 0 ℎ 2 4
39 15 35 38 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = norm ℎ ⁡ A + ℎ B 2 - norm ℎ ⁡ A - ℎ B 2 + i ⁢ norm ℎ ⁡ A + ℎ i ⋅ ℎ B 2 − norm ℎ ⁡ A - ℎ i ⋅ ℎ B 2 4