Metamath Proof Explorer


Theorem dip0r

Description: Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dip0r.1 𝑋 = ( BaseSet ‘ 𝑈 )
dip0r.5 𝑍 = ( 0vec𝑈 )
dip0r.7 𝑃 = ( ·𝑖OLD𝑈 )
Assertion dip0r ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 𝑃 𝑍 ) = 0 )

Proof

Step Hyp Ref Expression
1 dip0r.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 dip0r.5 𝑍 = ( 0vec𝑈 )
3 dip0r.7 𝑃 = ( ·𝑖OLD𝑈 )
4 1 2 nvzcl ( 𝑈 ∈ NrmCVec → 𝑍𝑋 )
5 4 adantr ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → 𝑍𝑋 )
6 eqid ( +𝑣𝑈 ) = ( +𝑣𝑈 )
7 eqid ( ·𝑠OLD𝑈 ) = ( ·𝑠OLD𝑈 )
8 eqid ( normCV𝑈 ) = ( normCV𝑈 )
9 1 6 7 8 3 ipval2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑍𝑋 ) → ( 𝐴 𝑃 𝑍 ) = ( ( ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
10 5 9 mpd3an3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 𝑃 𝑍 ) = ( ( ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
11 neg1cn - 1 ∈ ℂ
12 7 2 nvsz ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ) → ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
13 11 12 mpan2 ( 𝑈 ∈ NrmCVec → ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
14 13 adantr ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
15 14 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) = ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) )
16 15 fveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) = ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) )
17 16 oveq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) = ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) )
18 17 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) ) )
19 1 6 7 8 3 ipval2lem3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑍𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) ∈ ℝ )
20 5 19 mpd3an3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) ∈ ℝ )
21 20 recnd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) ∈ ℂ )
22 21 subidd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) ) = 0 )
23 18 22 eqtrd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = 0 )
24 negicn - i ∈ ℂ
25 7 2 nvsz ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ) → ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
26 24 25 mpan2 ( 𝑈 ∈ NrmCVec → ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
27 ax-icn i ∈ ℂ
28 7 2 nvsz ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ) → ( i ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
29 27 28 mpan2 ( 𝑈 ∈ NrmCVec → ( i ( ·𝑠OLD𝑈 ) 𝑍 ) = 𝑍 )
30 26 29 eqtr4d ( 𝑈 ∈ NrmCVec → ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) = ( i ( ·𝑠OLD𝑈 ) 𝑍 ) )
31 30 adantr ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) = ( i ( ·𝑠OLD𝑈 ) 𝑍 ) )
32 31 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) = ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) )
33 32 fveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) = ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) )
34 33 oveq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) = ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) )
35 34 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) )
36 1 6 7 8 3 ipval2lem4 ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑍𝑋 ) ∧ i ∈ ℂ ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ∈ ℂ )
37 27 36 mpan2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑍𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ∈ ℂ )
38 5 37 mpd3an3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ∈ ℂ )
39 38 subidd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = 0 )
40 35 39 eqtrd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = 0 )
41 40 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) = ( i · 0 ) )
42 23 41 oveq12d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) = ( 0 + ( i · 0 ) ) )
43 it0e0 ( i · 0 ) = 0
44 43 oveq2i ( 0 + ( i · 0 ) ) = ( 0 + 0 )
45 00id ( 0 + 0 ) = 0
46 44 45 eqtri ( 0 + ( i · 0 ) ) = 0
47 42 46 eqtrdi ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) = 0 )
48 47 oveq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( 0 / 4 ) )
49 4cn 4 ∈ ℂ
50 4ne0 4 ≠ 0
51 49 50 div0i ( 0 / 4 ) = 0
52 48 51 eqtrdi ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - 1 ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV𝑈 ) ‘ ( 𝐴 ( +𝑣𝑈 ) ( - i ( ·𝑠OLD𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) = 0 )
53 10 52 eqtrd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴 𝑃 𝑍 ) = 0 )