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

Metamath Proof Explorer

Theorem tcphphl

Description: Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space (because all the original components are the same). (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypothesis tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
Assertion tcphphl ( 𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 eqidd ⊢ ( ⊤ → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 1 3 tcphbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝐺 )
5 4 a1i ⊢ ( ⊤ → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐺 ) )
6 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
7 1 6 tchplusg ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝐺 )
8 7 a1i ⊢ ( ⊤ → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐺 ) )
9 8 oveqdr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
10 eqidd ⊢ ( ⊤ → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 1 11 tcphsca ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝐺 )
13 12 a1i ⊢ ( ⊤ → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝐺 ) )
14 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
15 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
16 1 15 tcphvsca ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐺 )
17 16 a1i ⊢ ( ⊤ → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐺 ) )
18 17 oveqdr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) )
19 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
20 1 19 tcphip ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝐺 )
21 20 a1i ⊢ ( ⊤ → ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝐺 ) )
22 21 oveqdr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝐺 ) 𝑦 ) )
23 2 5 9 10 13 14 18 22 phlpropd ⊢ ( ⊤ → ( 𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil ) )
24 23 mptru ⊢ ( 𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil )