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 )