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 )