cphnmvs

Description: Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphnmvs.v	$⊢ V = {Base}_{W}$
	cphnmvs.n	$⊢ N = norm (W)$
	cphnmvs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	cphnmvs.f	$⊢ F = Scalar (W)$
	cphnmvs.k	$⊢ K = {Base}_{F}$
Assertion	cphnmvs	$⊢ (W \in CPreHil \land X \in K \land Y \in V) \to N (X \underset{˙}{\cdot} Y) = \|X\| N (Y)$

Step	Hyp	Ref	Expression
1		cphnmvs.v	$⊢ V = {Base}_{W}$
2		cphnmvs.n	$⊢ N = norm (W)$
3		cphnmvs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		cphnmvs.f	$⊢ F = Scalar (W)$
5		cphnmvs.k	$⊢ K = {Base}_{F}$
6		cphnlm	$⊢ W \in CPreHil \to W \in NrmMod$
7		eqid	$⊢ norm (F) = norm (F)$
8	1 2 3 4 5 7	nmvs	$⊢ (W \in NrmMod \land X \in K \land Y \in V) \to N (X \underset{˙}{\cdot} Y) = norm (F) (X) N (Y)$
9	6 8	syl3an1	$⊢ (W \in CPreHil \land X \in K \land Y \in V) \to N (X \underset{˙}{\cdot} Y) = norm (F) (X) N (Y)$
10		cphclm	$⊢ W \in CPreHil \to W \in CMod$
11	4 5	clmabs	$⊢ (W \in CMod \land X \in K) \to \|X\| = norm (F) (X)$
12	10 11	sylan	$⊢ (W \in CPreHil \land X \in K) \to \|X\| = norm (F) (X)$
13	12	3adant3	$⊢ (W \in CPreHil \land X \in K \land Y \in V) \to \|X\| = norm (F) (X)$
14	13	oveq1d	$⊢ (W \in CPreHil \land X \in K \land Y \in V) \to \|X\| N (Y) = norm (F) (X) N (Y)$
15	9 14	eqtr4d	$⊢ (W \in CPreHil \land X \in K \land Y \in V) \to N (X \underset{˙}{\cdot} Y) = \|X\| N (Y)$

Metamath Proof Explorer