Theorem isncvsngpd

Description: Properties that determine a normed subcomplex vector space. (Contributed by NM, 15-Apr-2007) (Revised by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	isncvsngp.v	$$⊢V={\mathrm{Base}}_W$$
	isncvsngp.n	$$⊢N=\mathrm{norm}\left(W\right)$$
	isncvsngp.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	isncvsngp.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	isncvsngp.k	$$⊢K={\mathrm{Base}}_F$$
	isncvsngpd.v	$$⊢\phi \to W\in \mathrm{ℂVec}$$
	isncvsngpd.g	$$⊢\phi \to W\in \mathrm{NrmGrp}$$
	isncvsngpd.t	$$⊢\left(\phi \wedge \left(x\in V\wedge k\in K\right)\right)\to N\left(k\underset{\dot{}}{·}x\right)=\left|k\right|N\left(x\right)$$
Assertion	isncvsngpd	$$⊢\phi \to W\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isncvsngp.v	$$⊢V={\mathrm{Base}}_W$$
2		isncvsngp.n	$$⊢N=\mathrm{norm}\left(W\right)$$
3		isncvsngp.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		isncvsngp.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		isncvsngp.k	$$⊢K={\mathrm{Base}}_F$$
6		isncvsngpd.v	$$⊢\phi \to W\in \mathrm{ℂVec}$$
7		isncvsngpd.g	$$⊢\phi \to W\in \mathrm{NrmGrp}$$
8		isncvsngpd.t	$$⊢\left(\phi \wedge \left(x\in V\wedge k\in K\right)\right)\to N\left(k\underset{\dot{}}{·}x\right)=\left|k\right|N\left(x\right)$$
9	8	ralrimivva	$$⊢\phi \to \forall x\in V\forall k\in KN\left(k\underset{\dot{}}{·}x\right)=\left|k\right|N\left(x\right)$$
10	1 2 3 4 5	isncvsngp	$$⊢W\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)\leftrightarrow \left(W\in \mathrm{ℂVec}\wedge W\in \mathrm{NrmGrp}\wedge \forall x\in V\forall k\in KN\left(k\underset{\dot{}}{·}x\right)=\left|k\right|N\left(x\right)\right)$$
11	6 7 9 10	syl3anbrc	$$⊢\phi \to W\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)$$