Metamath Proof Explorer


Theorem dip0r

Description: Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dip0r.1 X = BaseSet U
dip0r.5 Z = 0 vec U
dip0r.7 P = 𝑖OLD U
Assertion dip0r U NrmCVec A X A P Z = 0

Proof

Step Hyp Ref Expression
1 dip0r.1 X = BaseSet U
2 dip0r.5 Z = 0 vec U
3 dip0r.7 P = 𝑖OLD U
4 1 2 nvzcl U NrmCVec Z X
5 4 adantr U NrmCVec A X Z X
6 eqid + v U = + v U
7 eqid 𝑠OLD U = 𝑠OLD U
8 eqid norm CV U = norm CV U
9 1 6 7 8 3 ipval2 U NrmCVec A X Z X A P Z = norm CV U A + v U Z 2 - norm CV U A + v U -1 𝑠OLD U Z 2 + i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 4
10 5 9 mpd3an3 U NrmCVec A X A P Z = norm CV U A + v U Z 2 - norm CV U A + v U -1 𝑠OLD U Z 2 + i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 4
11 neg1cn 1
12 7 2 nvsz U NrmCVec 1 -1 𝑠OLD U Z = Z
13 11 12 mpan2 U NrmCVec -1 𝑠OLD U Z = Z
14 13 adantr U NrmCVec A X -1 𝑠OLD U Z = Z
15 14 oveq2d U NrmCVec A X A + v U -1 𝑠OLD U Z = A + v U Z
16 15 fveq2d U NrmCVec A X norm CV U A + v U -1 𝑠OLD U Z = norm CV U A + v U Z
17 16 oveq1d U NrmCVec A X norm CV U A + v U -1 𝑠OLD U Z 2 = norm CV U A + v U Z 2
18 17 oveq2d U NrmCVec A X norm CV U A + v U Z 2 norm CV U A + v U -1 𝑠OLD U Z 2 = norm CV U A + v U Z 2 norm CV U A + v U Z 2
19 1 6 7 8 3 ipval2lem3 U NrmCVec A X Z X norm CV U A + v U Z 2
20 5 19 mpd3an3 U NrmCVec A X norm CV U A + v U Z 2
21 20 recnd U NrmCVec A X norm CV U A + v U Z 2
22 21 subidd U NrmCVec A X norm CV U A + v U Z 2 norm CV U A + v U Z 2 = 0
23 18 22 eqtrd U NrmCVec A X norm CV U A + v U Z 2 norm CV U A + v U -1 𝑠OLD U Z 2 = 0
24 negicn i
25 7 2 nvsz U NrmCVec i i 𝑠OLD U Z = Z
26 24 25 mpan2 U NrmCVec i 𝑠OLD U Z = Z
27 ax-icn i
28 7 2 nvsz U NrmCVec i i 𝑠OLD U Z = Z
29 27 28 mpan2 U NrmCVec i 𝑠OLD U Z = Z
30 26 29 eqtr4d U NrmCVec i 𝑠OLD U Z = i 𝑠OLD U Z
31 30 adantr U NrmCVec A X i 𝑠OLD U Z = i 𝑠OLD U Z
32 31 oveq2d U NrmCVec A X A + v U i 𝑠OLD U Z = A + v U i 𝑠OLD U Z
33 32 fveq2d U NrmCVec A X norm CV U A + v U i 𝑠OLD U Z = norm CV U A + v U i 𝑠OLD U Z
34 33 oveq1d U NrmCVec A X norm CV U A + v U i 𝑠OLD U Z 2 = norm CV U A + v U i 𝑠OLD U Z 2
35 34 oveq2d U NrmCVec A X norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 = norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2
36 1 6 7 8 3 ipval2lem4 U NrmCVec A X Z X i norm CV U A + v U i 𝑠OLD U Z 2
37 27 36 mpan2 U NrmCVec A X Z X norm CV U A + v U i 𝑠OLD U Z 2
38 5 37 mpd3an3 U NrmCVec A X norm CV U A + v U i 𝑠OLD U Z 2
39 38 subidd U NrmCVec A X norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 = 0
40 35 39 eqtrd U NrmCVec A X norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 = 0
41 40 oveq2d U NrmCVec A X i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 = i 0
42 23 41 oveq12d U NrmCVec A X norm CV U A + v U Z 2 - norm CV U A + v U -1 𝑠OLD U Z 2 + i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 = 0 + i 0
43 it0e0 i 0 = 0
44 43 oveq2i 0 + i 0 = 0 + 0
45 00id 0 + 0 = 0
46 44 45 eqtri 0 + i 0 = 0
47 42 46 eqtrdi U NrmCVec A X norm CV U A + v U Z 2 - norm CV U A + v U -1 𝑠OLD U Z 2 + i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 = 0
48 47 oveq1d U NrmCVec A X norm CV U A + v U Z 2 - norm CV U A + v U -1 𝑠OLD U Z 2 + i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 4 = 0 4
49 4cn 4
50 4ne0 4 0
51 49 50 div0i 0 4 = 0
52 48 51 eqtrdi U NrmCVec A X norm CV U A + v U Z 2 - norm CV U A + v U -1 𝑠OLD U Z 2 + i norm CV U A + v U i 𝑠OLD U Z 2 norm CV U A + v U i 𝑠OLD U Z 2 4 = 0
53 10 52 eqtrd U NrmCVec A X A P Z = 0