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	|- F = ( Scalar ` W )
Assertion	phlsrng	|- ( W e. PreHil -> F e. *Ring )

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	|- F = ( Scalar ` W )
2		eqid	|- ( Base ` W ) = ( Base ` W )
3		eqid	|- ( .i ` W ) = ( .i ` W )
4		eqid	|- ( 0g ` W ) = ( 0g ` W )
5		eqid	|- ( *r ` F ) = ( *r ` F )
6		eqid	|- ( 0g ` F ) = ( 0g ` F )
7	2 1 3 4 5 6	isphl	|- ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. ( Base ` W ) ( ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ( .i ` W ) x ) = ( 0g ` F ) -> x = ( 0g ` W ) ) /\ A. y e. ( Base ` W ) ( ( *r ` F ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) ) )
8	7	simp2bi	|- ( W e. PreHil -> F e. *Ring )