Metamath Proof Explorer

Theorem cphphl

Description: A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Assertion cphphl ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )

Proof

Step Hyp Ref Expression
1 eqid ⊒ ( Base β€˜ π‘Š ) = ( Base β€˜ π‘Š )
2 eqid ⊒ ( ·𝑖 β€˜ π‘Š ) = ( ·𝑖 β€˜ π‘Š )
3 eqid ⊒ ( norm β€˜ π‘Š ) = ( norm β€˜ π‘Š )
4 eqid ⊒ ( Scalar β€˜ π‘Š ) = ( Scalar β€˜ π‘Š )
5 eqid ⊒ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) = ( Base β€˜ ( Scalar β€˜ π‘Š ) )
6 1 2 3 4 5 iscph ⊒ ( π‘Š ∈ β„‚PreHil ↔ ( ( π‘Š ∈ PreHil ∧ π‘Š ∈ NrmMod ∧ ( Scalar β€˜ π‘Š ) = ( β„‚fld β†Ύs ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ) ) ∧ ( √ β€œ ( ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ∩ ( 0 [,) +∞ ) ) ) βŠ† ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ∧ ( norm β€˜ π‘Š ) = ( π‘₯ ∈ ( Base β€˜ π‘Š ) ↦ ( √ β€˜ ( π‘₯ ( ·𝑖 β€˜ π‘Š ) π‘₯ ) ) ) ) )
7 6 simp1bi ⊒ ( π‘Š ∈ β„‚PreHil β†’ ( π‘Š ∈ PreHil ∧ π‘Š ∈ NrmMod ∧ ( Scalar β€˜ π‘Š ) = ( β„‚fld β†Ύs ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ) ) )
8 7 simp1d ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )