Theorem 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	|- ., = ( .i ` W )
Assertion	tcphnmval	|- ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqrt ` ( X ., X ) ) )

Proof

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	|- ., = ( .i ` W )
5	1 2 3 4	tchnmfval	|- ( W e. Grp -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
6	5	fveq1d	|- ( W e. Grp -> ( N ` X ) = ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` X ) )
7		oveq12	|- ( ( x = X /\ x = X ) -> ( x ., x ) = ( X ., X ) )
8	7	anidms	|- ( x = X -> ( x ., x ) = ( X ., X ) )
9	8	fveq2d	|- ( x = X -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( X ., X ) ) )
10		eqid	|- ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
11		fvex	|- ( sqrt ` ( X ., X ) ) e. _V
12	9 10 11	fvmpt	|- ( X e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` X ) = ( sqrt ` ( X ., X ) ) )
13	6 12	sylan9eq	|- ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqrt ` ( X ., X ) ) )