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 ⊢ F = Scalar ⁡ W
Assertion phlsrng ⊢ W ∈ PreHil → F ∈ *-Ring

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ F = Scalar ⁡ W
2 eqid ⊢ Base W = Base W
3 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
4 eqid ⊢ 0 W = 0 W
5 eqid ⊢ * F = * F
6 eqid ⊢ 0 F = 0 F
7 2 1 3 4 5 6 isphl ⊢ W ∈ PreHil ↔ W ∈ LVec ∧ F ∈ *-Ring ∧ ∀ x ∈ Base W y ∈ Base W ⟼ y ⋅ 𝑖 ⁡ W x ∈ W LMHom ringLMod ⁡ F ∧ x ⋅ 𝑖 ⁡ W x = 0 F → x = 0 W ∧ ∀ y ∈ Base W x ⋅ 𝑖 ⁡ W y * F = y ⋅ 𝑖 ⁡ W x
8 7 simp2bi ⊢ W ∈ PreHil → F ∈ *-Ring