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

Metamath Proof Explorer

Theorem phlsrng

Description: The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypothesis phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion phlsrng ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )

Proof

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