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 = ( normCV ` U )
ipid.7 
|- P = ( .iOLD ` U )
Assertion ipidsq 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( N ` A ) ^ 2 ) )

Proof

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