# 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}={\mathrm{Base}}_{{W}}$
isnlm.n ${⊢}{N}=\mathrm{norm}\left({W}\right)$
isnlm.s
isnlm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
isnlm.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
isnlm.a ${⊢}{A}=\mathrm{norm}\left({F}\right)$
Assertion nmvs

### Proof

Step Hyp Ref Expression
1 isnlm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 isnlm.n ${⊢}{N}=\mathrm{norm}\left({W}\right)$
3 isnlm.s
4 isnlm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
5 isnlm.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
6 isnlm.a ${⊢}{A}=\mathrm{norm}\left({F}\right)$
7 1 2 3 4 5 6 isnlm
8 7 simprbi
9 fvoveq1
10 fveq2 ${⊢}{x}={X}\to {A}\left({x}\right)={A}\left({X}\right)$
11 10 oveq1d ${⊢}{x}={X}\to {A}\left({x}\right){N}\left({y}\right)={A}\left({X}\right){N}\left({y}\right)$
12 9 11 eqeq12d
13 oveq2
14 13 fveq2d
15 fveq2 ${⊢}{y}={Y}\to {N}\left({y}\right)={N}\left({Y}\right)$
16 15 oveq2d ${⊢}{y}={Y}\to {A}\left({X}\right){N}\left({y}\right)={A}\left({X}\right){N}\left({Y}\right)$
17 14 16 eqeq12d
18 12 17 rspc2v
19 8 18 syl5com
20 19 3impib