tcphnmval

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

	Ref	Expression
Hypotheses	tcphval.n	$⊢ G = toCPreHil (W)$
	tcphnmval.n	$⊢ N = norm (G)$
	tcphnmval.v	$⊢ V = {Base}_{W}$
	tcphnmval.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
Assertion	tcphnmval	$⊢ (W \in Grp \land X \in V) \to N (X) = \sqrt{X \underset{˙}{,} X}$

Step	Hyp	Ref	Expression
1		tcphval.n	$⊢ G = toCPreHil (W)$
2		tcphnmval.n	$⊢ N = norm (G)$
3		tcphnmval.v	$⊢ V = {Base}_{W}$
4		tcphnmval.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
5	1 2 3 4	tchnmfval	$⊢ W \in Grp \to N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$
6	5	fveq1d	$⊢ W \in Grp \to N (X) = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}) (X)$
7		oveq12	$⊢ (x = X \land x = X) \to x \underset{˙}{,} x = X \underset{˙}{,} X$
8	7	anidms	$⊢ x = X \to x \underset{˙}{,} x = X \underset{˙}{,} X$
9	8	fveq2d	$⊢ x = X \to \sqrt{x \underset{˙}{,} x} = \sqrt{X \underset{˙}{,} X}$
10		eqid	$⊢ (x \in V ⟼ \sqrt{x \underset{˙}{,} x}) = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$
11		fvex	$⊢ \sqrt{X \underset{˙}{,} X} \in V$
12	9 10 11	fvmpt	$⊢ X \in V \to (x \in V ⟼ \sqrt{x \underset{˙}{,} x}) (X) = \sqrt{X \underset{˙}{,} X}$
13	6 12	sylan9eq	$⊢ (W \in Grp \land X \in V) \to N (X) = \sqrt{X \underset{˙}{,} X}$

Metamath Proof Explorer