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 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 ⊢ ( 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 addridd ⊢ ( ( 𝑈 ∈ 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 ) )