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	$⊢ G = toCPreHil (W)$
	Assertion	tcphphl	$⊢ W \in PreHil \leftrightarrow G \in PreHil$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$⊢ G = toCPreHil (W)$
2		eqidd	$⊢ ⊤ \to {Base}_{W} = {Base}_{W}$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	1 3	tcphbas	$⊢ {Base}_{W} = {Base}_{G}$
5	4	a1i	$⊢ ⊤ \to {Base}_{W} = {Base}_{G}$
6		eqid	$⊢ +_{W} = +_{W}$
7	1 6	tchplusg	$⊢ +_{W} = +_{G}$
8	7	a1i	$⊢ ⊤ \to +_{W} = +_{G}$
9	8	oveqdr	$⊢ (⊤ \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to x +_{W} y = x +_{G} y$
10		eqidd	$⊢ ⊤ \to Scalar (W) = Scalar (W)$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12	1 11	tcphsca	$⊢ Scalar (W) = Scalar (G)$
13	12	a1i	$⊢ ⊤ \to Scalar (W) = Scalar (G)$
14		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
15		eqid	$⊢ \cdot_{W} = \cdot_{W}$
16	1 15	tcphvsca	$⊢ \cdot_{W} = \cdot_{G}$
17	16	a1i	$⊢ ⊤ \to \cdot_{W} = \cdot_{G}$
18	17	oveqdr	$⊢ (⊤ \land (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W})) \to x \cdot_{W} y = x \cdot_{G} y$
19		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
20	1 19	tcphip	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (G)$
21	20	a1i	$⊢ ⊤ \to \cdot_{𝑖} (W) = \cdot_{𝑖} (G)$
22	21	oveqdr	$⊢ (⊤ \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to x \cdot_{𝑖} (W) y = x \cdot_{𝑖} (G) y$
23	2 5 9 10 13 14 18 22	phlpropd	$⊢ ⊤ \to (W \in PreHil \leftrightarrow G \in PreHil)$
24	23	mptru	$⊢ W \in PreHil \leftrightarrow G \in PreHil$

Metamath Proof Explorer

Theorem tcphphl

Proof