Metamath Proof Explorer


Theorem cphipval2

Description: Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007) (Revised by AV, 18-Oct-2021)

Ref Expression
Hypotheses cphipfval.x X = Base W
cphipfval.p + ˙ = + W
cphipfval.s · ˙ = W
cphipfval.n N = norm W
cphipfval.i , ˙ = 𝑖 W
cphipval2.m - ˙ = - W
cphipval2.f F = Scalar W
cphipval2.k K = Base F
Assertion cphipval2 W CPreHil i K A X B X A , ˙ B = N A + ˙ B 2 - N A - ˙ B 2 + i N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 4

Proof

Step Hyp Ref Expression
1 cphipfval.x X = Base W
2 cphipfval.p + ˙ = + W
3 cphipfval.s · ˙ = W
4 cphipfval.n N = norm W
5 cphipfval.i , ˙ = 𝑖 W
6 cphipval2.m - ˙ = - W
7 cphipval2.f F = Scalar W
8 cphipval2.k K = Base F
9 simpl W CPreHil i K W CPreHil
10 9 3ad2ant1 W CPreHil i K A X B X W CPreHil
11 cphngp W CPreHil W NrmGrp
12 11 adantr W CPreHil i K W NrmGrp
13 ngpgrp W NrmGrp W Grp
14 12 13 syl W CPreHil i K W Grp
15 1 2 grpcl W Grp A X B X A + ˙ B X
16 14 15 syl3an1 W CPreHil i K A X B X A + ˙ B X
17 1 5 4 nmsq W CPreHil A + ˙ B X N A + ˙ B 2 = A + ˙ B , ˙ A + ˙ B
18 10 16 17 syl2anc W CPreHil i K A X B X N A + ˙ B 2 = A + ˙ B , ˙ A + ˙ B
19 simp2 W CPreHil i K A X B X A X
20 simp3 W CPreHil i K A X B X B X
21 5 1 2 10 19 20 19 20 cph2di W CPreHil i K A X B X A + ˙ B , ˙ A + ˙ B = A , ˙ A + B , ˙ B + A , ˙ B + B , ˙ A
22 18 21 eqtrd W CPreHil i K A X B X N A + ˙ B 2 = A , ˙ A + B , ˙ B + A , ˙ B + B , ˙ A
23 1 6 grpsubcl W Grp A X B X A - ˙ B X
24 14 23 syl3an1 W CPreHil i K A X B X A - ˙ B X
25 1 5 4 nmsq W CPreHil A - ˙ B X N A - ˙ B 2 = A - ˙ B , ˙ A - ˙ B
26 10 24 25 syl2anc W CPreHil i K A X B X N A - ˙ B 2 = A - ˙ B , ˙ A - ˙ B
27 5 1 6 10 19 20 19 20 cph2subdi W CPreHil i K A X B X A - ˙ B , ˙ A - ˙ B = A , ˙ A + B , ˙ B - A , ˙ B + B , ˙ A
28 26 27 eqtrd W CPreHil i K A X B X N A - ˙ B 2 = A , ˙ A + B , ˙ B - A , ˙ B + B , ˙ A
29 22 28 oveq12d W CPreHil i K A X B X N A + ˙ B 2 N A - ˙ B 2 = A , ˙ A + B , ˙ B + A , ˙ B + B , ˙ A - A , ˙ A + B , ˙ B - A , ˙ B + B , ˙ A
30 1 5 reipcl W CPreHil A X A , ˙ A
31 30 adantlr W CPreHil i K A X A , ˙ A
32 31 recnd W CPreHil i K A X A , ˙ A
33 32 3adant3 W CPreHil i K A X B X A , ˙ A
34 1 5 reipcl W CPreHil B X B , ˙ B
35 34 adantlr W CPreHil i K B X B , ˙ B
36 35 recnd W CPreHil i K B X B , ˙ B
37 36 3adant2 W CPreHil i K A X B X B , ˙ B
38 33 37 addcld W CPreHil i K A X B X A , ˙ A + B , ˙ B
39 1 5 cphipcl W CPreHil A X B X A , ˙ B
40 9 39 syl3an1 W CPreHil i K A X B X A , ˙ B
41 1 5 cphipcl W CPreHil B X A X B , ˙ A
42 9 41 syl3an1 W CPreHil i K B X A X B , ˙ A
43 42 3com23 W CPreHil i K A X B X B , ˙ A
44 40 43 addcld W CPreHil i K A X B X A , ˙ B + B , ˙ A
45 38 44 44 pnncand W CPreHil i K A X B X A , ˙ A + B , ˙ B + A , ˙ B + B , ˙ A - A , ˙ A + B , ˙ B - A , ˙ B + B , ˙ A = A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A
46 29 45 eqtrd W CPreHil i K A X B X N A + ˙ B 2 N A - ˙ B 2 = A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A
47 14 3ad2ant1 W CPreHil i K A X B X W Grp
48 cphlmod W CPreHil W LMod
49 48 adantr W CPreHil i K W LMod
50 49 adantr W CPreHil i K B X W LMod
51 simplr W CPreHil i K B X i K
52 simpr W CPreHil i K B X B X
53 1 7 3 8 lmodvscl W LMod i K B X i · ˙ B X
54 50 51 52 53 syl3anc W CPreHil i K B X i · ˙ B X
55 54 3adant2 W CPreHil i K A X B X i · ˙ B X
56 1 2 grpcl W Grp A X i · ˙ B X A + ˙ i · ˙ B X
57 47 19 55 56 syl3anc W CPreHil i K A X B X A + ˙ i · ˙ B X
58 1 5 4 nmsq W CPreHil A + ˙ i · ˙ B X N A + ˙ i · ˙ B 2 = A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
59 10 57 58 syl2anc W CPreHil i K A X B X N A + ˙ i · ˙ B 2 = A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
60 5 1 2 10 19 55 19 55 cph2di W CPreHil i K A X B X A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B = A , ˙ A + i · ˙ B , ˙ i · ˙ B + A , ˙ i · ˙ B + i · ˙ B , ˙ A
61 59 60 eqtrd W CPreHil i K A X B X N A + ˙ i · ˙ B 2 = A , ˙ A + i · ˙ B , ˙ i · ˙ B + A , ˙ i · ˙ B + i · ˙ B , ˙ A
62 1 6 grpsubcl W Grp A X i · ˙ B X A - ˙ i · ˙ B X
63 47 19 55 62 syl3anc W CPreHil i K A X B X A - ˙ i · ˙ B X
64 1 5 4 nmsq W CPreHil A - ˙ i · ˙ B X N A - ˙ i · ˙ B 2 = A - ˙ i · ˙ B , ˙ A - ˙ i · ˙ B
65 10 63 64 syl2anc W CPreHil i K A X B X N A - ˙ i · ˙ B 2 = A - ˙ i · ˙ B , ˙ A - ˙ i · ˙ B
66 5 1 6 10 19 55 19 55 cph2subdi W CPreHil i K A X B X A - ˙ i · ˙ B , ˙ A - ˙ i · ˙ B = A , ˙ A + i · ˙ B , ˙ i · ˙ B - A , ˙ i · ˙ B + i · ˙ B , ˙ A
67 65 66 eqtrd W CPreHil i K A X B X N A - ˙ i · ˙ B 2 = A , ˙ A + i · ˙ B , ˙ i · ˙ B - A , ˙ i · ˙ B + i · ˙ B , ˙ A
68 61 67 oveq12d W CPreHil i K A X B X N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 = A , ˙ A + i · ˙ B , ˙ i · ˙ B + A , ˙ i · ˙ B + i · ˙ B , ˙ A - A , ˙ A + i · ˙ B , ˙ i · ˙ B - A , ˙ i · ˙ B + i · ˙ B , ˙ A
69 68 oveq2d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 = i A , ˙ A + i · ˙ B , ˙ i · ˙ B + A , ˙ i · ˙ B + i · ˙ B , ˙ A - A , ˙ A + i · ˙ B , ˙ i · ˙ B - A , ˙ i · ˙ B + i · ˙ B , ˙ A
70 1 5 cphipcl W CPreHil i · ˙ B X i · ˙ B X i · ˙ B , ˙ i · ˙ B
71 10 55 55 70 syl3anc W CPreHil i K A X B X i · ˙ B , ˙ i · ˙ B
72 33 71 addcld W CPreHil i K A X B X A , ˙ A + i · ˙ B , ˙ i · ˙ B
73 1 5 cphipcl W CPreHil A X i · ˙ B X A , ˙ i · ˙ B
74 10 19 55 73 syl3anc W CPreHil i K A X B X A , ˙ i · ˙ B
75 1 5 cphipcl W CPreHil i · ˙ B X A X i · ˙ B , ˙ A
76 10 55 19 75 syl3anc W CPreHil i K A X B X i · ˙ B , ˙ A
77 74 76 addcld W CPreHil i K A X B X A , ˙ i · ˙ B + i · ˙ B , ˙ A
78 72 77 77 pnncand W CPreHil i K A X B X A , ˙ A + i · ˙ B , ˙ i · ˙ B + A , ˙ i · ˙ B + i · ˙ B , ˙ A - A , ˙ A + i · ˙ B , ˙ i · ˙ B - A , ˙ i · ˙ B + i · ˙ B , ˙ A = A , ˙ i · ˙ B + i · ˙ B , ˙ A + A , ˙ i · ˙ B + i · ˙ B , ˙ A
79 78 oveq2d W CPreHil i K A X B X i A , ˙ A + i · ˙ B , ˙ i · ˙ B + A , ˙ i · ˙ B + i · ˙ B , ˙ A - A , ˙ A + i · ˙ B , ˙ i · ˙ B - A , ˙ i · ˙ B + i · ˙ B , ˙ A = i A , ˙ i · ˙ B + i · ˙ B , ˙ A + A , ˙ i · ˙ B + i · ˙ B , ˙ A
80 1 3 5 7 8 cphassir W CPreHil i K A X B X A , ˙ i · ˙ B = i A , ˙ B
81 1 3 5 7 8 cphassi W CPreHil i K A X B X i · ˙ B , ˙ A = i B , ˙ A
82 80 81 oveq12d W CPreHil i K A X B X A , ˙ i · ˙ B + i · ˙ B , ˙ A = i A , ˙ B + i B , ˙ A
83 82 82 oveq12d W CPreHil i K A X B X A , ˙ i · ˙ B + i · ˙ B , ˙ A + A , ˙ i · ˙ B + i · ˙ B , ˙ A = i A , ˙ B + i B , ˙ A + i A , ˙ B + i B , ˙ A
84 83 oveq2d W CPreHil i K A X B X i A , ˙ i · ˙ B + i · ˙ B , ˙ A + A , ˙ i · ˙ B + i · ˙ B , ˙ A = i i A , ˙ B + i B , ˙ A + i A , ˙ B + i B , ˙ A
85 ax-icn i
86 85 a1i W CPreHil i K A X B X i
87 negicn i
88 87 a1i W CPreHil i K A X B X i
89 88 40 mulcld W CPreHil i K A X B X i A , ˙ B
90 86 43 mulcld W CPreHil i K A X B X i B , ˙ A
91 89 90 addcld W CPreHil i K A X B X i A , ˙ B + i B , ˙ A
92 86 91 91 adddid W CPreHil i K A X B X i i A , ˙ B + i B , ˙ A + i A , ˙ B + i B , ˙ A = i i A , ˙ B + i B , ˙ A + i i A , ˙ B + i B , ˙ A
93 86 89 90 adddid W CPreHil i K A X B X i i A , ˙ B + i B , ˙ A = i i A , ˙ B + i i B , ˙ A
94 86 88 40 mulassd W CPreHil i K A X B X i i A , ˙ B = i i A , ˙ B
95 85 85 mulneg2i i i = i i
96 ixi i i = 1
97 96 negeqi i i = -1
98 negneg1e1 -1 = 1
99 95 97 98 3eqtri i i = 1
100 99 oveq1i i i A , ˙ B = 1 A , ˙ B
101 94 100 eqtr3di W CPreHil i K A X B X i i A , ˙ B = 1 A , ˙ B
102 86 86 43 mulassd W CPreHil i K A X B X i i B , ˙ A = i i B , ˙ A
103 96 oveq1i i i B , ˙ A = -1 B , ˙ A
104 102 103 eqtr3di W CPreHil i K A X B X i i B , ˙ A = -1 B , ˙ A
105 101 104 oveq12d W CPreHil i K A X B X i i A , ˙ B + i i B , ˙ A = 1 A , ˙ B + -1 B , ˙ A
106 93 105 eqtrd W CPreHil i K A X B X i i A , ˙ B + i B , ˙ A = 1 A , ˙ B + -1 B , ˙ A
107 106 106 oveq12d W CPreHil i K A X B X i i A , ˙ B + i B , ˙ A + i i A , ˙ B + i B , ˙ A = 1 A , ˙ B + -1 B , ˙ A + 1 A , ˙ B + -1 B , ˙ A
108 40 mulid2d W CPreHil i K A X B X 1 A , ˙ B = A , ˙ B
109 108 oveq1d W CPreHil i K A X B X 1 A , ˙ B + -1 B , ˙ A = A , ˙ B + -1 B , ˙ A
110 addneg1mul A , ˙ B B , ˙ A A , ˙ B + -1 B , ˙ A = A , ˙ B B , ˙ A
111 40 43 110 syl2anc W CPreHil i K A X B X A , ˙ B + -1 B , ˙ A = A , ˙ B B , ˙ A
112 109 111 eqtrd W CPreHil i K A X B X 1 A , ˙ B + -1 B , ˙ A = A , ˙ B B , ˙ A
113 112 112 oveq12d W CPreHil i K A X B X 1 A , ˙ B + -1 B , ˙ A + 1 A , ˙ B + -1 B , ˙ A = A , ˙ B B , ˙ A + A , ˙ B - B , ˙ A
114 107 113 eqtrd W CPreHil i K A X B X i i A , ˙ B + i B , ˙ A + i i A , ˙ B + i B , ˙ A = A , ˙ B B , ˙ A + A , ˙ B - B , ˙ A
115 84 92 114 3eqtrd W CPreHil i K A X B X i A , ˙ i · ˙ B + i · ˙ B , ˙ A + A , ˙ i · ˙ B + i · ˙ B , ˙ A = A , ˙ B B , ˙ A + A , ˙ B - B , ˙ A
116 69 79 115 3eqtrd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 = A , ˙ B B , ˙ A + A , ˙ B - B , ˙ A
117 46 116 oveq12d W CPreHil i K A X B X N A + ˙ B 2 - N A - ˙ B 2 + i N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 = A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B B , ˙ A
118 117 oveq1d W CPreHil i K A X B X N A + ˙ B 2 - N A - ˙ B 2 + i N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 4 = A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B B , ˙ A 4
119 40 43 subcld W CPreHil i K A X B X A , ˙ B B , ˙ A
120 44 44 119 119 add4d W CPreHil i K A X B X A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B B , ˙ A = A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A
121 40 43 40 ppncand W CPreHil i K A X B X A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A = A , ˙ B + A , ˙ B
122 121 121 oveq12d W CPreHil i K A X B X A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A = A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B
123 120 122 eqtrd W CPreHil i K A X B X A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B B , ˙ A = A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B
124 123 oveq1d W CPreHil i K A X B X A , ˙ B + B , ˙ A + A , ˙ B + B , ˙ A + A , ˙ B B , ˙ A + A , ˙ B B , ˙ A 4 = A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B 4
125 40 2timesd W CPreHil i K A X B X 2 A , ˙ B = A , ˙ B + A , ˙ B
126 125 eqcomd W CPreHil i K A X B X A , ˙ B + A , ˙ B = 2 A , ˙ B
127 126 126 oveq12d W CPreHil i K A X B X A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B = 2 A , ˙ B + 2 A , ˙ B
128 2cnd W CPreHil i K A X B X 2
129 128 128 40 adddird W CPreHil i K A X B X 2 + 2 A , ˙ B = 2 A , ˙ B + 2 A , ˙ B
130 2p2e4 2 + 2 = 4
131 130 a1i W CPreHil i K A X B X 2 + 2 = 4
132 131 oveq1d W CPreHil i K A X B X 2 + 2 A , ˙ B = 4 A , ˙ B
133 127 129 132 3eqtr2d W CPreHil i K A X B X A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B = 4 A , ˙ B
134 133 oveq1d W CPreHil i K A X B X A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B 4 = 4 A , ˙ B 4
135 4cn 4
136 135 a1i W CPreHil i K A X B X 4
137 4ne0 4 0
138 137 a1i W CPreHil i K A X B X 4 0
139 40 136 138 divcan3d W CPreHil i K A X B X 4 A , ˙ B 4 = A , ˙ B
140 134 139 eqtrd W CPreHil i K A X B X A , ˙ B + A , ˙ B + A , ˙ B + A , ˙ B 4 = A , ˙ B
141 118 124 140 3eqtrrd W CPreHil i K A X B X A , ˙ B = N A + ˙ B 2 - N A - ˙ B 2 + i N A + ˙ i · ˙ B 2 N A - ˙ i · ˙ B 2 4