Theorem nmvs

Description: Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	isnlm.v	|- V = ( Base ` W )
	isnlm.n	|- N = ( norm ` W )
	isnlm.s	|- .x. = ( .s ` W )
	isnlm.f	|- F = ( Scalar ` W )
	isnlm.k	|- K = ( Base ` F )
	isnlm.a	|- A = ( norm ` F )
Assertion	nmvs	|- ( ( W e. NrmMod /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( A ` X ) x. ( N ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnlm.v	|- V = ( Base ` W )
2		isnlm.n	|- N = ( norm ` W )
3		isnlm.s	|- .x. = ( .s ` W )
4		isnlm.f	|- F = ( Scalar ` W )
5		isnlm.k	|- K = ( Base ` F )
6		isnlm.a	|- A = ( norm ` F )
7	1 2 3 4 5 6	isnlm	|- ( W e. NrmMod <-> ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) )
8	7	simprbi	|- ( W e. NrmMod -> A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) )
9		fvoveq1	|- ( x = X -> ( N ` ( x .x. y ) ) = ( N ` ( X .x. y ) ) )
10		fveq2	|- ( x = X -> ( A ` x ) = ( A ` X ) )
11	10	oveq1d	|- ( x = X -> ( ( A ` x ) x. ( N ` y ) ) = ( ( A ` X ) x. ( N ` y ) ) )
12	9 11	eqeq12d	|- ( x = X -> ( ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) <-> ( N ` ( X .x. y ) ) = ( ( A ` X ) x. ( N ` y ) ) ) )
13		oveq2	|- ( y = Y -> ( X .x. y ) = ( X .x. Y ) )
14	13	fveq2d	|- ( y = Y -> ( N ` ( X .x. y ) ) = ( N ` ( X .x. Y ) ) )
15		fveq2	|- ( y = Y -> ( N ` y ) = ( N ` Y ) )
16	15	oveq2d	|- ( y = Y -> ( ( A ` X ) x. ( N ` y ) ) = ( ( A ` X ) x. ( N ` Y ) ) )
17	14 16	eqeq12d	|- ( y = Y -> ( ( N ` ( X .x. y ) ) = ( ( A ` X ) x. ( N ` y ) ) <-> ( N ` ( X .x. Y ) ) = ( ( A ` X ) x. ( N ` Y ) ) ) )
18	12 17	rspc2v	|- ( ( X e. K /\ Y e. V ) -> ( A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) -> ( N ` ( X .x. Y ) ) = ( ( A ` X ) x. ( N ` Y ) ) ) )
19	8 18	syl5com	|- ( W e. NrmMod -> ( ( X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( A ` X ) x. ( N ` Y ) ) ) )
20	19	3impib	|- ( ( W e. NrmMod /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( A ` X ) x. ( N ` Y ) ) )