tcphvsca

Description: The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

Step	Hyp	Ref	Expression
1		tcphval.n	$⊢ G = toCPreHil (W)$
2		tcphvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	3	tcphex	$⊢ (x \in {Base}_{W} ⟼ \sqrt{x \cdot_{𝑖} (W) x}) \in V$
5		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
6	1 3 5	tcphval	$⊢ G = W toNrmGrp (x \in {Base}_{W} ⟼ \sqrt{x \cdot_{𝑖} (W) x})$
7	6 2	tngvsca	$⊢ (x \in {Base}_{W} ⟼ \sqrt{x \cdot_{𝑖} (W) x}) \in V \to \underset{˙}{\cdot} = \cdot_{G}$
8	4 7	ax-mp	$⊢ \underset{˙}{\cdot} = \cdot_{G}$

Metamath Proof Explorer