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 = BaseSet ⁡ U
ipid.6 ⊢ N = norm CV ⁡ U
ipid.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion ipidsq ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = N ⁡ A 2

Proof

Step Hyp Ref Expression
1 ipid.1 ⊢ X = BaseSet ⁡ U
2 ipid.6 ⊢ N = norm CV ⁡ U
3 ipid.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 eqid ⊢ + v ⁡ U = + v ⁡ U
5 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
6 1 4 5 2 3 ipval2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ∈ X → A P A = N ⁡ A + v ⁡ U A 2 - N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
7 6 3anidm23 ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = N ⁡ A + v ⁡ U A 2 - N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
8 1 4 5 nv2 ⊢ U ∈ NrmCVec ∧ A ∈ X → A + v ⁡ U A = 2 ⋅ 𝑠OLD ⁡ U A
9 8 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A = N ⁡ 2 ⋅ 𝑠OLD ⁡ U A
10 2re ⊢ 2 ∈ ℝ
11 0le2 ⊢ 0 ≤ 2
12 10 11 pm3.2i ⊢ 2 ∈ ℝ ∧ 0 ≤ 2
13 1 5 2 nvsge0 ⊢ U ∈ NrmCVec ∧ 2 ∈ ℝ ∧ 0 ≤ 2 ∧ A ∈ X → N ⁡ 2 ⋅ 𝑠OLD ⁡ U A = 2 ⁢ N ⁡ A
14 12 13 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 2 ⋅ 𝑠OLD ⁡ U A = 2 ⁢ N ⁡ A
15 9 14 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A = 2 ⁢ N ⁡ A
16 15 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A 2 = 2 ⁢ N ⁡ A 2
17 1 2 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℝ
18 17 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℂ
19 2cn ⊢ 2 ∈ ℂ
20 2nn0 ⊢ 2 ∈ ℕ 0
21 mulexp ⊢ 2 ∈ ℂ ∧ N ⁡ A ∈ ℂ ∧ 2 ∈ ℕ 0 → 2 ⁢ N ⁡ A 2 = 2 2 ⁢ N ⁡ A 2
22 19 20 21 mp3an13 ⊢ N ⁡ A ∈ ℂ → 2 ⁢ N ⁡ A 2 = 2 2 ⁢ N ⁡ A 2
23 18 22 syl ⊢ U ∈ NrmCVec ∧ A ∈ X → 2 ⁢ N ⁡ A 2 = 2 2 ⁢ N ⁡ A 2
24 sq2 ⊢ 2 2 = 4
25 24 oveq1i ⊢ 2 2 ⁢ N ⁡ A 2 = 4 ⁢ N ⁡ A 2
26 23 25 eqtrdi ⊢ U ∈ NrmCVec ∧ A ∈ X → 2 ⁢ N ⁡ A 2 = 4 ⁢ N ⁡ A 2
27 16 26 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A 2 = 4 ⁢ N ⁡ A 2
28 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
29 1 4 5 28 nvrinv ⊢ U ∈ NrmCVec ∧ A ∈ X → A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A = 0 vec ⁡ U
30 29 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A = N ⁡ 0 vec ⁡ U
31 28 2 nvz0 ⊢ U ∈ NrmCVec → N ⁡ 0 vec ⁡ U = 0
32 31 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 0 vec ⁡ U = 0
33 30 32 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A = 0
34 33 sq0id ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 = 0
35 27 34 oveq12d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A 2 − N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 = 4 ⁢ N ⁡ A 2 − 0
36 4cn ⊢ 4 ∈ ℂ
37 18 sqcld ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A 2 ∈ ℂ
38 mulcl ⊢ 4 ∈ ℂ ∧ N ⁡ A 2 ∈ ℂ → 4 ⁢ N ⁡ A 2 ∈ ℂ
39 36 37 38 sylancr ⊢ U ∈ NrmCVec ∧ A ∈ X → 4 ⁢ N ⁡ A 2 ∈ ℂ
40 39 subid1d ⊢ U ∈ NrmCVec ∧ A ∈ X → 4 ⁢ N ⁡ A 2 − 0 = 4 ⁢ N ⁡ A 2
41 35 40 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A 2 − N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 = 4 ⁢ N ⁡ A 2
42 1re ⊢ 1 ∈ ℝ
43 neg1rr ⊢ − 1 ∈ ℝ
44 absreim ⊢ 1 ∈ ℝ ∧ − 1 ∈ ℝ → 1 + i ⁢ -1 = 1 2 + − 1 2
45 42 43 44 mp2an ⊢ 1 + i ⁢ -1 = 1 2 + − 1 2
46 ax-icn ⊢ i ∈ ℂ
47 ax-1cn ⊢ 1 ∈ ℂ
48 46 47 mulneg2i ⊢ i ⁢ -1 = − i ⋅ 1
49 46 mulridi ⊢ i ⋅ 1 = i
50 49 negeqi ⊢ − i ⋅ 1 = − 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 ⊢ 1 ∈ ℂ → − 1 2 = 1 2
55 47 54 ax-mp ⊢ − 1 2 = 1 2
56 55 oveq2i ⊢ 1 2 + − 1 2 = 1 2 + 1 2
57 56 fveq2i ⊢ 1 2 + − 1 2 = 1 2 + 1 2
58 45 53 57 3eqtr3i ⊢ 1 + − i = 1 2 + 1 2
59 absreim ⊢ 1 ∈ ℝ ∧ 1 ∈ ℝ → 1 + i ⋅ 1 = 1 2 + 1 2
60 42 42 59 mp2an ⊢ 1 + i ⋅ 1 = 1 2 + 1 2
61 49 oveq2i ⊢ 1 + i ⋅ 1 = 1 + i
62 61 fveq2i ⊢ 1 + i ⋅ 1 = 1 + i
63 58 60 62 3eqtr2i ⊢ 1 + − i = 1 + i
64 63 oveq1i ⊢ 1 + − i ⁢ N ⁡ A = 1 + i ⁢ N ⁡ A
65 negicn ⊢ − i ∈ ℂ
66 47 65 addcli ⊢ 1 + − i ∈ ℂ
67 1 5 2 nvs ⊢ U ∈ NrmCVec ∧ 1 + − i ∈ ℂ ∧ A ∈ X → N ⁡ 1 + − i ⋅ 𝑠OLD ⁡ U A = 1 + − i ⁢ N ⁡ A
68 66 67 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 1 + − i ⋅ 𝑠OLD ⁡ U A = 1 + − i ⁢ N ⁡ A
69 47 46 addcli ⊢ 1 + i ∈ ℂ
70 1 5 2 nvs ⊢ U ∈ NrmCVec ∧ 1 + i ∈ ℂ ∧ A ∈ X → N ⁡ 1 + i ⋅ 𝑠OLD ⁡ U A = 1 + i ⁢ N ⁡ A
71 69 70 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 1 + i ⋅ 𝑠OLD ⁡ U A = 1 + i ⁢ N ⁡ A
72 64 68 71 3eqtr4a ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 1 + − i ⋅ 𝑠OLD ⁡ U A = N ⁡ 1 + i ⋅ 𝑠OLD ⁡ U A
73 1 4 5 nvdir ⊢ U ∈ NrmCVec ∧ 1 ∈ ℂ ∧ − i ∈ ℂ ∧ A ∈ X → 1 + − i ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
74 47 73 mp3anr1 ⊢ U ∈ NrmCVec ∧ − i ∈ ℂ ∧ A ∈ X → 1 + − i ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
75 65 74 mpanr1 ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 + − i ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
76 1 5 nvsid ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⋅ 𝑠OLD ⁡ U A = A
77 76 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A = A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
78 75 77 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 + − i ⋅ 𝑠OLD ⁡ U A = A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
79 78 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 1 + − i ⋅ 𝑠OLD ⁡ U A = N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A
80 1 4 5 nvdir ⊢ U ∈ NrmCVec ∧ 1 ∈ ℂ ∧ i ∈ ℂ ∧ A ∈ X → 1 + i ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
81 47 80 mp3anr1 ⊢ U ∈ NrmCVec ∧ i ∈ ℂ ∧ A ∈ X → 1 + i ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
82 46 81 mpanr1 ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 + i ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
83 76 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A = A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
84 82 83 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 + i ⋅ 𝑠OLD ⁡ U A = A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
85 84 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 1 + i ⋅ 𝑠OLD ⁡ U A = N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
86 72 79 85 3eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A = N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A
87 86 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 = N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2
88 87 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 = N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2
89 1 4 5 2 3 ipval2lem4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ∈ X ∧ i ∈ ℂ → N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 ∈ ℂ
90 46 89 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ∈ X → N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 ∈ ℂ
91 90 3anidm23 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 ∈ ℂ
92 91 subidd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 = 0
93 88 92 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 = 0
94 93 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 = i ⋅ 0
95 it0e0 ⊢ i ⋅ 0 = 0
96 94 95 eqtrdi ⊢ U ∈ NrmCVec ∧ A ∈ X → i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 = 0
97 41 96 oveq12d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U A 2 - N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 = 4 ⁢ N ⁡ A 2 + 0
98 39 addridd ⊢ U ∈ NrmCVec ∧ A ∈ X → 4 ⁢ N ⁡ A 2 + 0 = 4 ⁢ N ⁡ A 2
99 97 98 eqtr2d ⊢ U ∈ NrmCVec ∧ A ∈ X → 4 ⁢ N ⁡ A 2 = N ⁡ A + v ⁡ U A 2 - N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2
100 99 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → 4 ⁢ N ⁡ A 2 4 = N ⁡ A + v ⁡ U A 2 - N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A 2 + i ⁢ N ⁡ A + v ⁡ U i ⋅ 𝑠OLD ⁡ U A 2 − N ⁡ A + v ⁡ U − i ⋅ 𝑠OLD ⁡ U A 2 4
101 4ne0 ⊢ 4 ≠ 0
102 divcan3 ⊢ N ⁡ A 2 ∈ ℂ ∧ 4 ∈ ℂ ∧ 4 ≠ 0 → 4 ⁢ N ⁡ A 2 4 = N ⁡ A 2
103 36 101 102 mp3an23 ⊢ N ⁡ A 2 ∈ ℂ → 4 ⁢ N ⁡ A 2 4 = N ⁡ A 2
104 37 103 syl ⊢ U ∈ NrmCVec ∧ A ∈ X → 4 ⁢ N ⁡ A 2 4 = N ⁡ A 2
105 7 100 104 3eqtr2d ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = N ⁡ A 2