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 )