This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem phllvec

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

Ref Expression
Assertion phllvec ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
3 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
4 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
5 eqid ⊢ ( *𝑟 ‘ ( Scalar ‘ 𝑊 ) ) = ( *𝑟 ‘ ( Scalar ‘ 𝑊 ) )
6 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
7 1 2 3 4 5 6 isphl ⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ ( Scalar ‘ 𝑊 ) ∈ *-Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → 𝑥 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
8 7 simp1bi ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )