isnvi

Description: Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isnvi.5	$⊢ X = ran G$
	isnvi.6	$⊢ Z = GId (G)$
	isnvi.7	$⊢ ⟨G, S⟩ \in {CVec}_{OLD}$
	isnvi.8	$⊢ N : X ⟶ ℝ$
	isnvi.9	$⊢ (x \in X \land N (x) = 0) \to x = Z$
	isnvi.10	$⊢ (y \in ℂ \land x \in X) \to N (y S x) = \|y\| N (x)$
	isnvi.11	$⊢ (x \in X \land y \in X) \to N (x G y) \leq N (x) + N (y)$
	isnvi.12	$⊢ U = ⟨⟨G, S⟩, N⟩$
Assertion	isnvi	$⊢ U \in NrmCVec$

Step	Hyp	Ref	Expression
1		isnvi.5	$⊢ X = ran G$
2		isnvi.6	$⊢ Z = GId (G)$
3		isnvi.7	$⊢ ⟨G, S⟩ \in {CVec}_{OLD}$
4		isnvi.8	$⊢ N : X ⟶ ℝ$
5		isnvi.9	$⊢ (x \in X \land N (x) = 0) \to x = Z$
6		isnvi.10	$⊢ (y \in ℂ \land x \in X) \to N (y S x) = \|y\| N (x)$
7		isnvi.11	$⊢ (x \in X \land y \in X) \to N (x G y) \leq N (x) + N (y)$
8		isnvi.12	$⊢ U = ⟨⟨G, S⟩, N⟩$
9	5	ex	$⊢ x \in X \to (N (x) = 0 \to x = Z)$
10	6	ancoms	$⊢ (x \in X \land y \in ℂ) \to N (y S x) = \|y\| N (x)$
11	10	ralrimiva	$⊢ x \in X \to \forall y \in ℂ N (y S x) = \|y\| N (x)$
12	7	ralrimiva	$⊢ x \in X \to \forall y \in X N (x G y) \leq N (x) + N (y)$
13	9 11 12	3jca	$⊢ x \in X \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))$
14	13	rgen	$⊢ \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))$
15	1 2	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 = 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)))$
16	3 4 14 15	mpbir3an	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec$
17	8 16	eqeltri	$⊢ U \in NrmCVec$

Metamath Proof Explorer