isncvsngp

Description: A normed subcomplex vector space is a subcomplex vector space which is a normed group with a positively homogeneous norm. (Contributed by NM, 5-Jun-2008) (Revised by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	isncvsngp.v	$⊢ V = {Base}_{W}$
	isncvsngp.n	$⊢ N = norm (W)$
	isncvsngp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isncvsngp.f	$⊢ F = Scalar (W)$
	isncvsngp.k	$⊢ K = {Base}_{F}$
Assertion	isncvsngp	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$

Proof

Step	Hyp	Ref	Expression
1		isncvsngp.v	$⊢ V = {Base}_{W}$
2		isncvsngp.n	$⊢ N = norm (W)$
3		isncvsngp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		isncvsngp.f	$⊢ F = Scalar (W)$
5		isncvsngp.k	$⊢ K = {Base}_{F}$
6		isnvc	$⊢ W \in NrmVec \leftrightarrow (W \in NrmMod \land W \in LVec)$
7	6	biancomi	$⊢ W \in NrmVec \leftrightarrow (W \in LVec \land W \in NrmMod)$
8	7	a1i	$⊢ W \in ℂVec \to (W \in NrmVec \leftrightarrow (W \in LVec \land W \in NrmMod))$
9		id	$⊢ W \in ℂVec \to W \in ℂVec$
10	9	cvslvec	$⊢ W \in ℂVec \to W \in LVec$
11	10	biantrurd	$⊢ W \in ℂVec \to (W \in NrmMod \leftrightarrow (W \in LVec \land W \in NrmMod))$
12	9	cvsclm	$⊢ W \in ℂVec \to W \in CMod$
13		eqid	$⊢ norm (F) = norm (F)$
14	1 2 3 4 5 13	isnlm	$⊢ W \in NrmMod \leftrightarrow ((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x))$
15		3anass	$⊢ (W \in NrmGrp \land W \in LMod \land F \in NrmRing) \leftrightarrow (W \in NrmGrp \land (W \in LMod \land F \in NrmRing))$
16	15	biancomi	$⊢ (W \in NrmGrp \land W \in LMod \land F \in NrmRing) \leftrightarrow ((W \in LMod \land F \in NrmRing) \land W \in NrmGrp)$
17	16	anbi1i	$⊢ ((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow (((W \in LMod \land F \in NrmRing) \land W \in NrmGrp) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x))$
18		anass	$⊢ (((W \in LMod \land F \in NrmRing) \land W \in NrmGrp) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow ((W \in LMod \land F \in NrmRing) \land (W \in NrmGrp \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)))$
19	17 18	bitri	$⊢ ((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow ((W \in LMod \land F \in NrmRing) \land (W \in NrmGrp \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)))$
20	19	a1i	$⊢ W \in CMod \to (((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow ((W \in LMod \land F \in NrmRing) \land (W \in NrmGrp \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x))))$
21		clmlmod	$⊢ W \in CMod \to W \in LMod$
22	4 5	clmsca	$⊢ W \in CMod \to F = ℂ_{fld} ↾_{𝑠} K$
23		cnnrg	$⊢ ℂ_{fld} \in NrmRing$
24	4 5	clmsubrg	$⊢ W \in CMod \to K \in SubRing (ℂ_{fld})$
25		eqid	$⊢ ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} K$
26	25	subrgnrg	$⊢ (ℂ_{fld} \in NrmRing \land K \in SubRing (ℂ_{fld})) \to ℂ_{fld} ↾_{𝑠} K \in NrmRing$
27	23 24 26	sylancr	$⊢ W \in CMod \to ℂ_{fld} ↾_{𝑠} K \in NrmRing$
28	22 27	eqeltrd	$⊢ W \in CMod \to F \in NrmRing$
29	21 28	jca	$⊢ W \in CMod \to (W \in LMod \land F \in NrmRing)$
30	29	biantrurd	$⊢ W \in CMod \to ((W \in NrmGrp \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow ((W \in LMod \land F \in NrmRing) \land (W \in NrmGrp \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x))))$
31		ralcom	$⊢ \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x) \leftrightarrow \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)$
32	22	fveq2d	$⊢ W \in CMod \to norm (F) = norm (ℂ_{fld} ↾_{𝑠} K)$
33		subrgsubg	$⊢ K \in SubRing (ℂ_{fld}) \to K \in SubGrp (ℂ_{fld})$
34		eqid	$⊢ norm (ℂ_{fld}) = norm (ℂ_{fld})$
35		eqid	$⊢ norm (ℂ_{fld} ↾_{𝑠} K) = norm (ℂ_{fld} ↾_{𝑠} K)$
36	25 34 35	subgnm	$⊢ K \in SubGrp (ℂ_{fld}) \to norm (ℂ_{fld} ↾_{𝑠} K) = {norm (ℂ_{fld}) ↾}_{K}$
37	24 33 36	3syl	$⊢ W \in CMod \to norm (ℂ_{fld} ↾_{𝑠} K) = {norm (ℂ_{fld}) ↾}_{K}$
38	32 37	eqtrd	$⊢ W \in CMod \to norm (F) = {norm (ℂ_{fld}) ↾}_{K}$
39	38	adantr	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to norm (F) = {norm (ℂ_{fld}) ↾}_{K}$
40	39	fveq1d	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to norm (F) (k) = ({norm (ℂ_{fld}) ↾}_{K}) (k)$
41		cnfldnm	$⊢ abs = norm (ℂ_{fld})$
42	41	eqcomi	$⊢ norm (ℂ_{fld}) = abs$
43	42	reseq1i	$⊢ {norm (ℂ_{fld}) ↾}_{K} = {abs ↾}_{K}$
44	43	fveq1i	$⊢ ({norm (ℂ_{fld}) ↾}_{K}) (k) = ({abs ↾}_{K}) (k)$
45		fvres	$⊢ k \in K \to ({abs ↾}_{K}) (k) = \|k\|$
46	45	ad2antll	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to ({abs ↾}_{K}) (k) = \|k\|$
47	44 46	syl5eq	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to ({norm (ℂ_{fld}) ↾}_{K}) (k) = \|k\|$
48	40 47	eqtrd	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to norm (F) (k) = \|k\|$
49	48	oveq1d	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to norm (F) (k) N (x) = \|k\| N (x)$
50	49	eqeq2d	$⊢ (W \in CMod \land (x \in V \land k \in K)) \to (N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x) \leftrightarrow N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
51	50	2ralbidva	$⊢ W \in CMod \to (\forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x) \leftrightarrow \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
52	31 51	syl5bb	$⊢ W \in CMod \to (\forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x) \leftrightarrow \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
53	52	anbi2d	$⊢ W \in CMod \to ((W \in NrmGrp \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
54	20 30 53	3bitr2d	$⊢ W \in CMod \to (((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall k \in K \forall x \in V N (k \underset{˙}{\cdot} x) = norm (F) (k) N (x)) \leftrightarrow (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
55	14 54	syl5bb	$⊢ W \in CMod \to (W \in NrmMod \leftrightarrow (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
56	12 55	syl	$⊢ W \in ℂVec \to (W \in NrmMod \leftrightarrow (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
57	8 11 56	3bitr2d	$⊢ W \in ℂVec \to (W \in NrmVec \leftrightarrow (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
58	57	pm5.32i	$⊢ (W \in ℂVec \land W \in NrmVec) \leftrightarrow (W \in ℂVec \land (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
59		elin	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in NrmVec \land W \in ℂVec)$
60	59	biancomi	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in ℂVec \land W \in NrmVec)$
61		3anass	$⊢ (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \leftrightarrow (W \in ℂVec \land (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
62	58 60 61	3bitr4i	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$

Metamath Proof Explorer

Theorem isncvsngp

Proof