Metamath Proof Explorer

Theorem dip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. (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 dip0l ⊢ U ∈ NrmCVec ∧ A ∈ X → Z P A = 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 1 3 dipcj ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ Z ∈ X → A P Z ‾ = Z P A
7 5 6 mpd3an3 ⊢ U ∈ NrmCVec ∧ A ∈ X → A P Z ‾ = Z P A
8 1 2 3 dip0r ⊢ U ∈ NrmCVec ∧ A ∈ X → A P Z = 0
9 8 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → A P Z ‾ = 0 ‾
10 cj0 ⊢ 0 ‾ = 0
11 9 10 eqtrdi ⊢ U ∈ NrmCVec ∧ A ∈ X → A P Z ‾ = 0
12 7 11 eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ X → Z P A = 0