ncvsi

Description: The properties of a normed subcomplex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006) (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}$
	ncvsi.m	$⊢ \underset{˙}{-} = -_{W}$
	ncvsi.0	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	ncvsi	$⊢ W \in (NrmVec \cap ℂVec) \to (W \in ℂVec \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \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		ncvsi.m	$⊢ \underset{˙}{-} = -_{W}$
7		ncvsi.0	$⊢ \underset{˙}{0} = 0_{W}$
8	1 2 3 4 5	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))$
9		simp1	$⊢ (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to W \in ℂVec$
10	1 2	nmf	$⊢ W \in NrmGrp \to N : V ⟶ ℝ$
11	10	3ad2ant2	$⊢ (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to N : V ⟶ ℝ$
12	1 2 6 7	ngpi	$⊢ W \in NrmGrp \to (W \in Grp \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)))$
13		r19.26	$⊢ \forall x \in V (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \leftrightarrow (\forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
14		simpll	$⊢ (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
15		simplr	$⊢ (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)$
16		simpr	$⊢ (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)$
17	14 15 16	3jca	$⊢ (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
18	17	ralimi	$⊢ \forall x \in V (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
19	13 18	sylbir	$⊢ (\forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
20	19	ex	$⊢ \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)) \to (\forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
21	20	3ad2ant3	$⊢ (W \in Grp \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y))) \to (\forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
22	12 21	syl	$⊢ W \in NrmGrp \to (\forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
23	22	imp	$⊢ (W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
24	23	3adant1	$⊢ (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x))$
25	9 11 24	3jca	$⊢ (W \in ℂVec \land W \in NrmGrp \land \forall x \in V \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)) \to (W \in ℂVec \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$
26	8 25	sylbi	$⊢ W \in (NrmVec \cap ℂVec) \to (W \in ℂVec \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y) \land \forall k \in K N (k \underset{˙}{\cdot} x) = \|k\| N (x)))$

Metamath Proof Explorer

Theorem ncvsi

Proof