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