Metamath Proof Explorer


Theorem ipidsq

Description: The inner product of a vector with itself is the square of the vector's norm. Equation I4 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipid.1 X=BaseSetU
ipid.6 N=normCVU
ipid.7 P=𝑖OLDU
Assertion ipidsq UNrmCVecAXAPA=NA2

Proof

Step Hyp Ref Expression
1 ipid.1 X=BaseSetU
2 ipid.6 N=normCVU
3 ipid.7 P=𝑖OLDU
4 eqid +vU=+vU
5 eqid 𝑠OLDU=𝑠OLDU
6 1 4 5 2 3 ipval2 UNrmCVecAXAXAPA=NA+vUA2-NA+vU-1𝑠OLDUA2+iNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA24
7 6 3anidm23 UNrmCVecAXAPA=NA+vUA2-NA+vU-1𝑠OLDUA2+iNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA24
8 1 4 5 nv2 UNrmCVecAXA+vUA=2𝑠OLDUA
9 8 fveq2d UNrmCVecAXNA+vUA=N2𝑠OLDUA
10 2re 2
11 0le2 02
12 10 11 pm3.2i 202
13 1 5 2 nvsge0 UNrmCVec202AXN2𝑠OLDUA=2NA
14 12 13 mp3an2 UNrmCVecAXN2𝑠OLDUA=2NA
15 9 14 eqtrd UNrmCVecAXNA+vUA=2NA
16 15 oveq1d UNrmCVecAXNA+vUA2=2NA2
17 1 2 nvcl UNrmCVecAXNA
18 17 recnd UNrmCVecAXNA
19 2cn 2
20 2nn0 20
21 mulexp 2NA202NA2=22NA2
22 19 20 21 mp3an13 NA2NA2=22NA2
23 18 22 syl UNrmCVecAX2NA2=22NA2
24 sq2 22=4
25 24 oveq1i 22NA2=4NA2
26 23 25 eqtrdi UNrmCVecAX2NA2=4NA2
27 16 26 eqtrd UNrmCVecAXNA+vUA2=4NA2
28 eqid 0vecU=0vecU
29 1 4 5 28 nvrinv UNrmCVecAXA+vU-1𝑠OLDUA=0vecU
30 29 fveq2d UNrmCVecAXNA+vU-1𝑠OLDUA=N0vecU
31 28 2 nvz0 UNrmCVecN0vecU=0
32 31 adantr UNrmCVecAXN0vecU=0
33 30 32 eqtrd UNrmCVecAXNA+vU-1𝑠OLDUA=0
34 33 sq0id UNrmCVecAXNA+vU-1𝑠OLDUA2=0
35 27 34 oveq12d UNrmCVecAXNA+vUA2NA+vU-1𝑠OLDUA2=4NA20
36 4cn 4
37 18 sqcld UNrmCVecAXNA2
38 mulcl 4NA24NA2
39 36 37 38 sylancr UNrmCVecAX4NA2
40 39 subid1d UNrmCVecAX4NA20=4NA2
41 35 40 eqtrd UNrmCVecAXNA+vUA2NA+vU-1𝑠OLDUA2=4NA2
42 1re 1
43 neg1rr 1
44 absreim 111+i-1=12+12
45 42 43 44 mp2an 1+i-1=12+12
46 ax-icn i
47 ax-1cn 1
48 46 47 mulneg2i i-1=i1
49 46 mulid1i i1=i
50 49 negeqi i1=i
51 48 50 eqtri i-1=i
52 51 oveq2i 1+i-1=1+i
53 52 fveq2i 1+i-1=1+i
54 sqneg 112=12
55 47 54 ax-mp 12=12
56 55 oveq2i 12+12=12+12
57 56 fveq2i 12+12=12+12
58 45 53 57 3eqtr3i 1+i=12+12
59 absreim 111+i1=12+12
60 42 42 59 mp2an 1+i1=12+12
61 49 oveq2i 1+i1=1+i
62 61 fveq2i 1+i1=1+i
63 58 60 62 3eqtr2i 1+i=1+i
64 63 oveq1i 1+iNA=1+iNA
65 negicn i
66 47 65 addcli 1+i
67 1 5 2 nvs UNrmCVec1+iAXN1+i𝑠OLDUA=1+iNA
68 66 67 mp3an2 UNrmCVecAXN1+i𝑠OLDUA=1+iNA
69 47 46 addcli 1+i
70 1 5 2 nvs UNrmCVec1+iAXN1+i𝑠OLDUA=1+iNA
71 69 70 mp3an2 UNrmCVecAXN1+i𝑠OLDUA=1+iNA
72 64 68 71 3eqtr4a UNrmCVecAXN1+i𝑠OLDUA=N1+i𝑠OLDUA
73 1 4 5 nvdir UNrmCVec1iAX1+i𝑠OLDUA=1𝑠OLDUA+vUi𝑠OLDUA
74 47 73 mp3anr1 UNrmCVeciAX1+i𝑠OLDUA=1𝑠OLDUA+vUi𝑠OLDUA
75 65 74 mpanr1 UNrmCVecAX1+i𝑠OLDUA=1𝑠OLDUA+vUi𝑠OLDUA
76 1 5 nvsid UNrmCVecAX1𝑠OLDUA=A
77 76 oveq1d UNrmCVecAX1𝑠OLDUA+vUi𝑠OLDUA=A+vUi𝑠OLDUA
78 75 77 eqtrd UNrmCVecAX1+i𝑠OLDUA=A+vUi𝑠OLDUA
79 78 fveq2d UNrmCVecAXN1+i𝑠OLDUA=NA+vUi𝑠OLDUA
80 1 4 5 nvdir UNrmCVec1iAX1+i𝑠OLDUA=1𝑠OLDUA+vUi𝑠OLDUA
81 47 80 mp3anr1 UNrmCVeciAX1+i𝑠OLDUA=1𝑠OLDUA+vUi𝑠OLDUA
82 46 81 mpanr1 UNrmCVecAX1+i𝑠OLDUA=1𝑠OLDUA+vUi𝑠OLDUA
83 76 oveq1d UNrmCVecAX1𝑠OLDUA+vUi𝑠OLDUA=A+vUi𝑠OLDUA
84 82 83 eqtrd UNrmCVecAX1+i𝑠OLDUA=A+vUi𝑠OLDUA
85 84 fveq2d UNrmCVecAXN1+i𝑠OLDUA=NA+vUi𝑠OLDUA
86 72 79 85 3eqtr3d UNrmCVecAXNA+vUi𝑠OLDUA=NA+vUi𝑠OLDUA
87 86 oveq1d UNrmCVecAXNA+vUi𝑠OLDUA2=NA+vUi𝑠OLDUA2
88 87 oveq2d UNrmCVecAXNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2=NA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2
89 1 4 5 2 3 ipval2lem4 UNrmCVecAXAXiNA+vUi𝑠OLDUA2
90 46 89 mpan2 UNrmCVecAXAXNA+vUi𝑠OLDUA2
91 90 3anidm23 UNrmCVecAXNA+vUi𝑠OLDUA2
92 91 subidd UNrmCVecAXNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2=0
93 88 92 eqtrd UNrmCVecAXNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2=0
94 93 oveq2d UNrmCVecAXiNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2=i0
95 it0e0 i0=0
96 94 95 eqtrdi UNrmCVecAXiNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2=0
97 41 96 oveq12d UNrmCVecAXNA+vUA2-NA+vU-1𝑠OLDUA2+iNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2=4NA2+0
98 39 addid1d UNrmCVecAX4NA2+0=4NA2
99 97 98 eqtr2d UNrmCVecAX4NA2=NA+vUA2-NA+vU-1𝑠OLDUA2+iNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA2
100 99 oveq1d UNrmCVecAX4NA24=NA+vUA2-NA+vU-1𝑠OLDUA2+iNA+vUi𝑠OLDUA2NA+vUi𝑠OLDUA24
101 4ne0 40
102 divcan3 NA24404NA24=NA2
103 36 101 102 mp3an23 NA24NA24=NA2
104 37 103 syl UNrmCVecAX4NA24=NA2
105 7 100 104 3eqtr2d UNrmCVecAXAPA=NA2