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

Proof

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