nvi

Description: The properties of a normed complex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvi.1	$⊢ X = BaseSet (U)$
	nvi.2	$⊢ G = +_{v} (U)$
	nvi.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	nvi.5	$⊢ Z = 0_{vec} (U)$
	nvi.6	$⊢ N = {norm}_{CV} (U)$
Assertion	nvi	$⊢ U \in NrmCVec \to (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$

Proof

Step	Hyp	Ref	Expression
1		nvi.1	$⊢ X = BaseSet (U)$
2		nvi.2	$⊢ G = +_{v} (U)$
3		nvi.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		nvi.5	$⊢ Z = 0_{vec} (U)$
5		nvi.6	$⊢ N = {norm}_{CV} (U)$
6		eqid	$⊢ 1^{st} (U) = 1^{st} (U)$
7	6 5	nvop2	$⊢ U \in NrmCVec \to U = ⟨1^{st} (U), N⟩$
8	6 2 3	nvvop	$⊢ U \in NrmCVec \to 1^{st} (U) = ⟨G, S⟩$
9	8	opeq1d	$⊢ U \in NrmCVec \to ⟨1^{st} (U), N⟩ = ⟨⟨G, S⟩, N⟩$
10	7 9	eqtrd	$⊢ U \in NrmCVec \to U = ⟨⟨G, S⟩, N⟩$
11		id	$⊢ U \in NrmCVec \to U \in NrmCVec$
12	10 11	eqeltrrd	$⊢ U \in NrmCVec \to ⟨⟨G, S⟩, N⟩ \in NrmCVec$
13	1 2	bafval	$⊢ X = ran G$
14		eqid	$⊢ GId (G) = GId (G)$
15	13 14	isnv	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = GId (G)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
16	12 15	sylib	$⊢ U \in NrmCVec \to (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = GId (G)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
17	2 4	0vfval	$⊢ U \in NrmCVec \to Z = GId (G)$
18	17	eqeq2d	$⊢ U \in NrmCVec \to (x = Z \leftrightarrow x = GId (G))$
19	18	imbi2d	$⊢ U \in NrmCVec \to ((N (x) = 0 \to x = Z) \leftrightarrow (N (x) = 0 \to x = GId (G)))$
20	19	3anbi1d	$⊢ U \in NrmCVec \to (((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)) \leftrightarrow ((N (x) = 0 \to x = GId (G)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
21	20	ralbidv	$⊢ U \in NrmCVec \to (\forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)) \leftrightarrow \forall x \in X ((N (x) = 0 \to x = GId (G)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
22	21	3anbi3d	$⊢ U \in NrmCVec \to ((⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))) \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = GId (G)) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))))$
23	16 22	mpbird	$⊢ U \in NrmCVec \to (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$

Metamath Proof Explorer

Theorem nvi

Proof