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 ⊢X=BaseSet⁡U
dip0r.5 ⊢Z=0vec⁡U
dip0r.7 ⊢P=⋅𝑖OLD⁡U
Assertion dip0r ⊢U∈NrmCVec∧A∈X→APZ=0

Proof

Step Hyp Ref Expression
1 dip0r.1 ⊢X=BaseSet⁡U
2 dip0r.5 ⊢Z=0vec⁡U
3 dip0r.7 ⊢P=⋅𝑖OLD⁡U
4 1 2 nvzcl ⊢U∈NrmCVec→Z∈X
5 4 adantr ⊢U∈NrmCVec∧A∈X→Z∈X
6 eqid ⊢+v⁡U=+v⁡U
7 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
8 eqid ⊢normCV⁡U=normCV⁡U
9 1 6 7 8 3 ipval2 ⊢U∈NrmCVec∧A∈X∧Z∈X→APZ=normCV⁡U⁡A+v⁡UZ2-normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2+i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ24
10 5 9 mpd3an3 ⊢U∈NrmCVec∧A∈X→APZ=normCV⁡U⁡A+v⁡UZ2-normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2+i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ24
11 neg1cn ⊢−1∈ℂ
12 7 2 nvsz ⊢U∈NrmCVec∧−1∈ℂ→-1⋅𝑠OLD⁡UZ=Z
13 11 12 mpan2 ⊢U∈NrmCVec→-1⋅𝑠OLD⁡UZ=Z
14 13 adantr ⊢U∈NrmCVec∧A∈X→-1⋅𝑠OLD⁡UZ=Z
15 14 oveq2d ⊢U∈NrmCVec∧A∈X→A+v⁡U-1⋅𝑠OLD⁡UZ=A+v⁡UZ
16 15 fveq2d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ=normCV⁡U⁡A+v⁡UZ
17 16 oveq1d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2=normCV⁡U⁡A+v⁡UZ2
18 17 oveq2d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2−normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2=normCV⁡U⁡A+v⁡UZ2−normCV⁡U⁡A+v⁡UZ2
19 1 6 7 8 3 ipval2lem3 ⊢U∈NrmCVec∧A∈X∧Z∈X→normCV⁡U⁡A+v⁡UZ2∈ℝ
20 5 19 mpd3an3 ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2∈ℝ
21 20 recnd ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2∈ℂ
22 21 subidd ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2−normCV⁡U⁡A+v⁡UZ2=0
23 18 22 eqtrd ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2−normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2=0
24 negicn ⊢−i∈ℂ
25 7 2 nvsz ⊢U∈NrmCVec∧−i∈ℂ→−i⋅𝑠OLD⁡UZ=Z
26 24 25 mpan2 ⊢U∈NrmCVec→−i⋅𝑠OLD⁡UZ=Z
27 ax-icn ⊢i∈ℂ
28 7 2 nvsz ⊢U∈NrmCVec∧i∈ℂ→i⋅𝑠OLD⁡UZ=Z
29 27 28 mpan2 ⊢U∈NrmCVec→i⋅𝑠OLD⁡UZ=Z
30 26 29 eqtr4d ⊢U∈NrmCVec→−i⋅𝑠OLD⁡UZ=i⋅𝑠OLD⁡UZ
31 30 adantr ⊢U∈NrmCVec∧A∈X→−i⋅𝑠OLD⁡UZ=i⋅𝑠OLD⁡UZ
32 31 oveq2d ⊢U∈NrmCVec∧A∈X→A+v⁡U−i⋅𝑠OLD⁡UZ=A+v⁡Ui⋅𝑠OLD⁡UZ
33 32 fveq2d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ=normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ
34 33 oveq1d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ2=normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2
35 34 oveq2d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ2=normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2
36 1 6 7 8 3 ipval2lem4 ⊢U∈NrmCVec∧A∈X∧Z∈X∧i∈ℂ→normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2∈ℂ
37 27 36 mpan2 ⊢U∈NrmCVec∧A∈X∧Z∈X→normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2∈ℂ
38 5 37 mpd3an3 ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2∈ℂ
39 38 subidd ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2=0
40 35 39 eqtrd ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ2=0
41 40 oveq2d ⊢U∈NrmCVec∧A∈X→i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ2=i⋅0
42 23 41 oveq12d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2-normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2+i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ2=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 ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2-normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2+i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ2=0
48 47 oveq1d ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2-normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2+i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ24=04
49 4cn ⊢4∈ℂ
50 4ne0 ⊢4≠0
51 49 50 div0i ⊢04=0
52 48 51 eqtrdi ⊢U∈NrmCVec∧A∈X→normCV⁡U⁡A+v⁡UZ2-normCV⁡U⁡A+v⁡U-1⋅𝑠OLD⁡UZ2+i⁢normCV⁡U⁡A+v⁡Ui⋅𝑠OLD⁡UZ2−normCV⁡U⁡A+v⁡U−i⋅𝑠OLD⁡UZ24=0
53 10 52 eqtrd ⊢U∈NrmCVec∧A∈X→APZ=0