Metamath Proof Explorer

Theorem cphipcl

Description: An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses nmsq.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
nmsq.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
Assertion cphipcl ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉 ) β†’ ( 𝐴 , 𝐡 ) ∈ β„‚ )

Proof

Step Hyp Ref Expression
1 nmsq.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
2 nmsq.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
3 eqid ⊒ ( Scalar β€˜ π‘Š ) = ( Scalar β€˜ π‘Š )
4 eqid ⊒ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) = ( Base β€˜ ( Scalar β€˜ π‘Š ) )
5 3 4 cphsubrg ⊒ ( π‘Š ∈ β„‚PreHil β†’ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ∈ ( SubRing β€˜ β„‚fld ) )
6 cnfldbas ⊒ β„‚ = ( Base β€˜ β„‚fld )
7 6 subrgss ⊒ ( ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ∈ ( SubRing β€˜ β„‚fld ) β†’ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) βŠ† β„‚ )
8 5 7 syl ⊒ ( π‘Š ∈ β„‚PreHil β†’ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) βŠ† β„‚ )
9 8 3ad2ant1 ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉 ) β†’ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) βŠ† β„‚ )
10 cphphl ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )
11 3 2 1 4 ipcl ⊒ ( ( π‘Š ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉 ) β†’ ( 𝐴 , 𝐡 ) ∈ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) )
12 10 11 syl3an1 ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉 ) β†’ ( 𝐴 , 𝐡 ) ∈ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) )
13 9 12 sseldd ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉 ) β†’ ( 𝐴 , 𝐡 ) ∈ β„‚ )