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

Metamath Proof Explorer

Theorem cphphl

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

Ref Expression
Assertion cphphl ⊢ W ∈ CPreHil → W ∈ PreHil

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base W = Base W
2 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
3 eqid ⊢ norm ⁡ W = norm ⁡ W
4 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
5 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
6 1 2 3 4 5 iscph ⊢ W ∈ CPreHil ↔ W ∈ PreHil ∧ W ∈ NrmMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W ∧ √ Base Scalar ⁡ W ∩ 0 +∞ ⊆ Base Scalar ⁡ W ∧ norm ⁡ W = x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x
7 6 simp1bi ⊢ W ∈ CPreHil → W ∈ PreHil ∧ W ∈ NrmMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W
8 7 simp1d ⊢ W ∈ CPreHil → W ∈ PreHil