Metamath Proof Explorer

Theorem cphip0r

Description: Inner product with a zero second argument. Complex version of ip0r . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
cphipcj.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
cphip0l.z ⊒ 0 = ( 0g β€˜ π‘Š )
Assertion cphip0r ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 , 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 cphipcj.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
2 cphipcj.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
3 cphip0l.z ⊒ 0 = ( 0g β€˜ π‘Š )
4 cphphl ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )
5 eqid ⊒ ( Scalar β€˜ π‘Š ) = ( Scalar β€˜ π‘Š )
6 eqid ⊒ ( 0g β€˜ ( Scalar β€˜ π‘Š ) ) = ( 0g β€˜ ( Scalar β€˜ π‘Š ) )
7 5 1 2 6 3 ip0r ⊒ ( ( π‘Š ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 , 0 ) = ( 0g β€˜ ( Scalar β€˜ π‘Š ) ) )
8 4 7 sylan ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 , 0 ) = ( 0g β€˜ ( Scalar β€˜ π‘Š ) ) )
9 cphclm ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ β„‚Mod )
10 5 clm0 ⊒ ( π‘Š ∈ β„‚Mod β†’ 0 = ( 0g β€˜ ( Scalar β€˜ π‘Š ) ) )
11 9 10 syl ⊒ ( π‘Š ∈ β„‚PreHil β†’ 0 = ( 0g β€˜ ( Scalar β€˜ π‘Š ) ) )
12 11 adantr ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ) β†’ 0 = ( 0g β€˜ ( Scalar β€˜ π‘Š ) ) )
13 8 12 eqtr4d ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ) β†’ ( 𝐴 , 0 ) = 0 )