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 )