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	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	isnlm.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	isnlm.k	$$⊢K={\mathrm{Base}}_F$$
	isnlm.a	$$⊢A=\mathrm{norm}\left(F\right)$$
Assertion	nmvs	$$⊢\left(W\in \mathrm{NrmMod}\wedge X\in K\wedge Y\in V\right)\to N\left(X\underset{\dot{}}{·}Y\right)=A\left(X\right)N\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		isnlm.v	$$⊢V={\mathrm{Base}}_W$$
2		isnlm.n	$$⊢N=\mathrm{norm}\left(W\right)$$
3		isnlm.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
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	$$⊢W\in \mathrm{NrmMod}\leftrightarrow \left(\left(W\in \mathrm{NrmGrp}\wedge W\in \mathrm{LMod}\wedge F\in \mathrm{NrmRing}\right)\wedge \forall x\in K\forall y\in VN\left(x\underset{\dot{}}{·}y\right)=A\left(x\right)N\left(y\right)\right)$$
8	7	simprbi	$$⊢W\in \mathrm{NrmMod}\to \forall x\in K\forall y\in VN\left(x\underset{\dot{}}{·}y\right)=A\left(x\right)N\left(y\right)$$
9		fvoveq1	$$⊢x=X\to N\left(x\underset{\dot{}}{·}y\right)=N\left(X\underset{\dot{}}{·}y\right)$$
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	$$⊢x=X\to \left(N\left(x\underset{\dot{}}{·}y\right)=A\left(x\right)N\left(y\right)\leftrightarrow N\left(X\underset{\dot{}}{·}y\right)=A\left(X\right)N\left(y\right)\right)$$
13		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
14	13	fveq2d	$$⊢y=Y\to N\left(X\underset{\dot{}}{·}y\right)=N\left(X\underset{\dot{}}{·}Y\right)$$
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	$$⊢y=Y\to \left(N\left(X\underset{\dot{}}{·}y\right)=A\left(X\right)N\left(y\right)\leftrightarrow N\left(X\underset{\dot{}}{·}Y\right)=A\left(X\right)N\left(Y\right)\right)$$
18	12 17	rspc2v	$$⊢\left(X\in K\wedge Y\in V\right)\to \left(\forall x\in K\forall y\in VN\left(x\underset{\dot{}}{·}y\right)=A\left(x\right)N\left(y\right)\to N\left(X\underset{\dot{}}{·}Y\right)=A\left(X\right)N\left(Y\right)\right)$$
19	8 18	syl5com	$$⊢W\in \mathrm{NrmMod}\to \left(\left(X\in K\wedge Y\in V\right)\to N\left(X\underset{\dot{}}{·}Y\right)=A\left(X\right)N\left(Y\right)\right)$$
20	19	3impib	$$⊢\left(W\in \mathrm{NrmMod}\wedge X\in K\wedge Y\in V\right)\to N\left(X\underset{\dot{}}{·}Y\right)=A\left(X\right)N\left(Y\right)$$