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⋅ihB=A+ℎC⋅ihD+ℎB-A-ℎC⋅ihD-ℎB+i⁢A+ℎi⋅ℎC⋅ihD+ℎi⋅ℎB−A-ℎi⋅ℎC⋅ihD-ℎi⋅ℎB4

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