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 𝑋 = ( BaseSet ‘ 𝑈 )
ipid.6 𝑁 = ( normCV𝑈 )
ipid.7 𝑃 = ( ·𝑖OLD𝑈 )
Assertion ipidsq ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 𝑃 𝐴 ) = ( ( 𝑁𝐴 ) ↑ 2 ) )

Proof

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