Metamath Proof Explorer

Theorem isnlm

Description: A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (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 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 ) ) ) )

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 anass 
 |-  ( ( ( W e. ( NrmGrp i^i LMod ) /\ F e. NrmRing ) /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) <-> ( W e. ( NrmGrp i^i LMod ) /\ ( F e. NrmRing /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) ) )
8 df-3an 
 |-  ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) <-> ( ( W e. NrmGrp /\ W e. LMod ) /\ F e. NrmRing ) )
9 elin 
 |-  ( W e. ( NrmGrp i^i LMod ) <-> ( W e. NrmGrp /\ W e. LMod ) )
10 9 anbi1i 
 |-  ( ( W e. ( NrmGrp i^i LMod ) /\ F e. NrmRing ) <-> ( ( W e. NrmGrp /\ W e. LMod ) /\ F e. NrmRing ) )
11 8 10 bitr4i 
 |-  ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) <-> ( W e. ( NrmGrp i^i LMod ) /\ F e. NrmRing ) )
12 11 anbi1i 
 |-  ( ( ( 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 ) ) ) <-> ( ( W e. ( NrmGrp i^i LMod ) /\ F e. NrmRing ) /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) )
13 fvexd 
 |-  ( w = W -> ( Scalar ` w ) e. _V )
14 id 
 |-  ( f = ( Scalar ` w ) -> f = ( Scalar ` w ) )
15 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
16 15 4 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = F )
17 14 16 sylan9eqr 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> f = F )
18 17 eleq1d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( f e. NrmRing <-> F e. NrmRing ) )
19 17 fveq2d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` f ) = ( Base ` F ) )
20 19 5 eqtr4di 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` f ) = K )
21 simpl 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> w = W )
22 21 fveq2d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` w ) = ( Base ` W ) )
23 22 1 eqtr4di 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` w ) = V )
24 21 fveq2d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( norm ` w ) = ( norm ` W ) )
25 24 2 eqtr4di 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( norm ` w ) = N )
26 21 fveq2d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( .s ` w ) = ( .s ` W ) )
27 26 3 eqtr4di 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( .s ` w ) = .x. )
28 27 oveqd 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( x ( .s ` w ) y ) = ( x .x. y ) )
29 25 28 fveq12d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( N ` ( x .x. y ) ) )
30 17 fveq2d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( norm ` f ) = ( norm ` F ) )
31 30 6 eqtr4di 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( norm ` f ) = A )
32 31 fveq1d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( ( norm ` f ) ` x ) = ( A ` x ) )
33 25 fveq1d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( ( norm ` w ) ` y ) = ( N ` y ) )
34 32 33 oveq12d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) = ( ( A ` x ) x. ( N ` y ) ) )
35 29 34 eqeq12d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) <-> ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) )
36 23 35 raleqbidv 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) <-> A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) )
37 20 36 raleqbidv 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) <-> A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) )
38 18 37 anbi12d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) <-> ( F e. NrmRing /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) ) )
39 13 38 sbcied 
 |-  ( w = W -> ( [. ( Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) <-> ( F e. NrmRing /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) ) )
40 df-nlm 
 |-  NrmMod = { w e. ( NrmGrp i^i LMod ) | [. ( Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) }
41 39 40 elrab2 
 |-  ( W e. NrmMod <-> ( W e. ( NrmGrp i^i LMod ) /\ ( F e. NrmRing /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) ) )
42 7 12 41 3bitr4ri 
 |-  ( 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 ) ) ) )