Metamath Proof Explorer

Theorem isnv

Description: The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	isnv.1	$⊢ X = ran G$
		isnv.2	$⊢ Z = GId (G)$
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		isnv.1	$⊢ X = ran G$
2		isnv.2	$⊢ Z = GId (G)$
3		nvex	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to (G \in V \land S \in V \land N \in V)$
4		vcex	$⊢ ⟨G, S⟩ \in {CVec}_{OLD} \to (G \in V \land S \in V)$
5	4	adantr	$⊢ (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ) \to (G \in V \land S \in V)$
6	4	simpld	$⊢ ⟨G, S⟩ \in {CVec}_{OLD} \to G \in V$
7		rnexg	$⊢ G \in V \to ran G \in V$
8	6 7	syl	$⊢ ⟨G, S⟩ \in {CVec}_{OLD} \to ran G \in V$
9	1 8	eqeltrid	$⊢ ⟨G, S⟩ \in {CVec}_{OLD} \to X \in V$
10		fex	$⊢ (N : X ⟶ ℝ \land X \in V) \to N \in V$
11	9 10	sylan2	$⊢ (N : X ⟶ ℝ \land ⟨G, S⟩ \in {CVec}_{OLD}) \to N \in V$
12	11	ancoms	$⊢ (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ) \to N \in V$
13		df-3an	$⊢ (G \in V \land S \in V \land N \in V) \leftrightarrow ((G \in V \land S \in V) \land N \in V)$
14	5 12 13	sylanbrc	$⊢ (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ) \to (G \in V \land S \in V \land N \in V)$
15	14	3adant3	$⊢ (⟨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))) \to (G \in V \land S \in V \land N \in V)$
16	1 2	isnvlem	$⊢ (G \in V \land S \in V \land N \in V) \to (⟨⟨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))))$
17	3 15 16	pm5.21nii	$⊢ ⟨⟨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)))$