This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )