Metamath Proof Explorer

Theorem polid2i

Description: Generalized polarization identity. Generalization of Exercise 4(a) of ReedSimon p. 63. (Contributed by NM, 30-Jun-2005) (New usage is discouraged.)

Ref Expression
Hypotheses polid2.1 ⊢ A ∈ ℋ
polid2.2 ⊢ B ∈ ℋ
polid2.3 ⊢ C ∈ ℋ
polid2.4 ⊢ D ∈ ℋ
Assertion polid2i ⊢ A ⋅ ih B = A + ℎ C ⋅ ih D + ℎ B - A - ℎ C ⋅ ih D - ℎ B + i ⁢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B 4

Proof

Step Hyp Ref Expression
1 polid2.1 ⊢ A ∈ ℋ
2 polid2.2 ⊢ B ∈ ℋ
3 polid2.3 ⊢ C ∈ ℋ
4 polid2.4 ⊢ D ∈ ℋ
5 4cn ⊢ 4 ∈ ℂ
6 1 2 hicli ⊢ A ⋅ ih B ∈ ℂ
7 4ne0 ⊢ 4 ≠ 0
8 2cn ⊢ 2 ∈ ℂ
9 3 4 hicli ⊢ C ⋅ ih D ∈ ℂ
10 6 9 addcli ⊢ A ⋅ ih B + C ⋅ ih D ∈ ℂ
11 6 9 subcli ⊢ A ⋅ ih B − C ⋅ ih D ∈ ℂ
12 8 10 11 adddii ⊢ 2 ⁢ A ⋅ ih B + C ⋅ ih D + A ⋅ ih B − C ⋅ ih D = 2 ⁢ A ⋅ ih B + C ⋅ ih D + 2 ⁢ A ⋅ ih B − C ⋅ ih D
13 ppncan ⊢ A ⋅ ih B ∈ ℂ ∧ C ⋅ ih D ∈ ℂ ∧ A ⋅ ih B ∈ ℂ → A ⋅ ih B + C ⋅ ih D + A ⋅ ih B − C ⋅ ih D = A ⋅ ih B + A ⋅ ih B
14 6 9 6 13 mp3an ⊢ A ⋅ ih B + C ⋅ ih D + A ⋅ ih B − C ⋅ ih D = A ⋅ ih B + A ⋅ ih B
15 6 2timesi ⊢ 2 ⁢ A ⋅ ih B = A ⋅ ih B + A ⋅ ih B
16 14 15 eqtr4i ⊢ A ⋅ ih B + C ⋅ ih D + A ⋅ ih B − C ⋅ ih D = 2 ⁢ A ⋅ ih B
17 16 oveq2i ⊢ 2 ⁢ A ⋅ ih B + C ⋅ ih D + A ⋅ ih B − C ⋅ ih D = 2 ⁢ 2 ⁢ A ⋅ ih B
18 8 8 6 mulassi ⊢ 2 ⋅ 2 ⁢ A ⋅ ih B = 2 ⁢ 2 ⁢ A ⋅ ih B
19 2t2e4 ⊢ 2 ⋅ 2 = 4
20 19 oveq1i ⊢ 2 ⋅ 2 ⁢ A ⋅ ih B = 4 ⁢ A ⋅ ih B
21 17 18 20 3eqtr2ri ⊢ 4 ⁢ A ⋅ ih B = 2 ⁢ A ⋅ ih B + C ⋅ ih D + A ⋅ ih B − C ⋅ ih D
22 1 4 hicli ⊢ A ⋅ ih D ∈ ℂ
23 3 2 hicli ⊢ C ⋅ ih B ∈ ℂ
24 22 23 addcli ⊢ A ⋅ ih D + C ⋅ ih B ∈ ℂ
25 24 10 10 pnncani ⊢ A ⋅ ih D + C ⋅ ih B + A ⋅ ih B + C ⋅ ih D - A ⋅ ih D + C ⋅ ih B - A ⋅ ih B + C ⋅ ih D = A ⋅ ih B + C ⋅ ih D + A ⋅ ih B + C ⋅ ih D
26 1 3 4 2 normlem8 ⊢ A + ℎ C ⋅ ih D + ℎ B = A ⋅ ih D + C ⋅ ih B + A ⋅ ih B + C ⋅ ih D
27 1 3 4 2 normlem9 ⊢ A - ℎ C ⋅ ih D - ℎ B = A ⋅ ih D + C ⋅ ih B - A ⋅ ih B + C ⋅ ih D
28 26 27 oveq12i ⊢ A + ℎ C ⋅ ih D + ℎ B − A - ℎ C ⋅ ih D - ℎ B = A ⋅ ih D + C ⋅ ih B + A ⋅ ih B + C ⋅ ih D - A ⋅ ih D + C ⋅ ih B - A ⋅ ih B + C ⋅ ih D
29 10 2timesi ⊢ 2 ⁢ A ⋅ ih B + C ⋅ ih D = A ⋅ ih B + C ⋅ ih D + A ⋅ ih B + C ⋅ ih D
30 25 28 29 3eqtr4i ⊢ A + ℎ C ⋅ ih D + ℎ B − A - ℎ C ⋅ ih D - ℎ B = 2 ⁢ A ⋅ ih B + C ⋅ ih D
31 ax-icn ⊢ i ∈ ℂ
32 31 3 hvmulcli ⊢ i ⋅ ℎ C ∈ ℋ
33 31 2 hvmulcli ⊢ i ⋅ ℎ B ∈ ℋ
34 1 32 4 33 normlem8 ⊢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B = A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B + A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D
35 1 32 4 33 normlem9 ⊢ A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B = A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B - A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D
36 34 35 oveq12i ⊢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B = A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B + A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D - A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B - A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D
37 32 33 hicli ⊢ i ⋅ ℎ C ⋅ ih i ⋅ ℎ B ∈ ℂ
38 22 37 addcli ⊢ A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B ∈ ℂ
39 1 33 hicli ⊢ A ⋅ ih i ⋅ ℎ B ∈ ℂ
40 32 4 hicli ⊢ i ⋅ ℎ C ⋅ ih D ∈ ℂ
41 39 40 addcli ⊢ A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D ∈ ℂ
42 38 41 41 pnncani ⊢ A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B + A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D - A ⋅ ih D + i ⋅ ℎ C ⋅ ih i ⋅ ℎ B - A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D = A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D + A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D
43 41 2timesi ⊢ 2 ⁢ A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D = A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D + A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D
44 his5 ⊢ i ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih i ⋅ ℎ B = i ‾ ⁢ A ⋅ ih B
45 31 1 2 44 mp3an ⊢ A ⋅ ih i ⋅ ℎ B = i ‾ ⁢ A ⋅ ih B
46 cji ⊢ i ‾ = − i
47 46 oveq1i ⊢ i ‾ ⁢ A ⋅ ih B = − i ⁢ A ⋅ ih B
48 45 47 eqtri ⊢ A ⋅ ih i ⋅ ℎ B = − i ⁢ A ⋅ ih B
49 ax-his3 ⊢ i ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → i ⋅ ℎ C ⋅ ih D = i ⁢ C ⋅ ih D
50 31 3 4 49 mp3an ⊢ i ⋅ ℎ C ⋅ ih D = i ⁢ C ⋅ ih D
51 48 50 oveq12i ⊢ A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D = − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D
52 51 oveq2i ⊢ 2 ⁢ A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D = 2 ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D
53 43 52 eqtr3i ⊢ A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D + A ⋅ ih i ⋅ ℎ B + i ⋅ ℎ C ⋅ ih D = 2 ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D
54 36 42 53 3eqtri ⊢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B = 2 ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D
55 54 oveq2i ⊢ i ⁢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B = i ⁢ 2 ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D
56 negicn ⊢ − i ∈ ℂ
57 56 6 mulcli ⊢ − i ⁢ A ⋅ ih B ∈ ℂ
58 31 9 mulcli ⊢ i ⁢ C ⋅ ih D ∈ ℂ
59 57 58 addcli ⊢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D ∈ ℂ
60 8 31 59 mul12i ⊢ 2 ⁢ i ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D = i ⁢ 2 ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D
61 31 57 58 adddii ⊢ i ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D = i ⁢ − i ⁢ A ⋅ ih B + i ⁢ i ⁢ C ⋅ ih D
62 31 31 mulneg2i ⊢ i ⁢ − i = − i ⁢ i
63 ixi ⊢ i ⁢ i = − 1
64 63 negeqi ⊢ − i ⁢ i = − -1
65 negneg1e1 ⊢ − -1 = 1
66 62 64 65 3eqtri ⊢ i ⁢ − i = 1
67 66 oveq1i ⊢ i ⁢ − i ⁢ A ⋅ ih B = 1 ⁢ A ⋅ ih B
68 31 56 6 mulassi ⊢ i ⁢ − i ⁢ A ⋅ ih B = i ⁢ − i ⁢ A ⋅ ih B
69 6 mulid2i ⊢ 1 ⁢ A ⋅ ih B = A ⋅ ih B
70 67 68 69 3eqtr3i ⊢ i ⁢ − i ⁢ A ⋅ ih B = A ⋅ ih B
71 63 oveq1i ⊢ i ⁢ i ⁢ C ⋅ ih D = -1 ⁢ C ⋅ ih D
72 31 31 9 mulassi ⊢ i ⁢ i ⁢ C ⋅ ih D = i ⁢ i ⁢ C ⋅ ih D
73 9 mulm1i ⊢ -1 ⁢ C ⋅ ih D = − C ⋅ ih D
74 71 72 73 3eqtr3i ⊢ i ⁢ i ⁢ C ⋅ ih D = − C ⋅ ih D
75 70 74 oveq12i ⊢ i ⁢ − i ⁢ A ⋅ ih B + i ⁢ i ⁢ C ⋅ ih D = A ⋅ ih B + − C ⋅ ih D
76 6 9 negsubi ⊢ A ⋅ ih B + − C ⋅ ih D = A ⋅ ih B − C ⋅ ih D
77 61 75 76 3eqtri ⊢ i ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D = A ⋅ ih B − C ⋅ ih D
78 77 oveq2i ⊢ 2 ⁢ i ⁢ − i ⁢ A ⋅ ih B + i ⁢ C ⋅ ih D = 2 ⁢ A ⋅ ih B − C ⋅ ih D
79 55 60 78 3eqtr2i ⊢ i ⁢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B = 2 ⁢ A ⋅ ih B − C ⋅ ih D
80 30 79 oveq12i ⊢ A + ℎ C ⋅ ih D + ℎ B - A - ℎ C ⋅ ih D - ℎ B + i ⁢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B = 2 ⁢ A ⋅ ih B + C ⋅ ih D + 2 ⁢ A ⋅ ih B − C ⋅ ih D
81 12 21 80 3eqtr4i ⊢ 4 ⁢ A ⋅ ih B = A + ℎ C ⋅ ih D + ℎ B - A - ℎ C ⋅ ih D - ℎ B + i ⁢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B
82 5 6 7 81 mvllmuli ⊢ A ⋅ ih B = A + ℎ C ⋅ ih D + ℎ B - A - ℎ C ⋅ ih D - ℎ B + i ⁢ A + ℎ i ⋅ ℎ C ⋅ ih D + ℎ i ⋅ ℎ B − A - ℎ i ⋅ ℎ C ⋅ ih D - ℎ i ⋅ ℎ B 4