This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ NrmCVec ↔ G S ∈ CVec OLD ∧ N : X ⟶ ℝ ∧ ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y S x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x G y ≤ 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 ∈ NrmCVec → G ∈ V ∧ S ∈ V ∧ N ∈ V
4 vcex ⊢ G S ∈ CVec OLD → G ∈ V ∧ S ∈ V
5 4 adantr ⊢ G S ∈ CVec OLD ∧ N : X ⟶ ℝ → G ∈ V ∧ S ∈ V
6 4 simpld ⊢ G S ∈ CVec OLD → G ∈ V
7 rnexg ⊢ G ∈ V → ran ⁡ G ∈ V
8 6 7 syl ⊢ G S ∈ CVec OLD → ran ⁡ G ∈ V
9 1 8 eqeltrid ⊢ G S ∈ CVec OLD → X ∈ V
10 fex ⊢ N : X ⟶ ℝ ∧ X ∈ V → N ∈ V
11 9 10 sylan2 ⊢ N : X ⟶ ℝ ∧ G S ∈ CVec OLD → N ∈ V
12 11 ancoms ⊢ G S ∈ CVec OLD ∧ N : X ⟶ ℝ → N ∈ V
13 df-3an ⊢ G ∈ V ∧ S ∈ V ∧ N ∈ V ↔ G ∈ V ∧ S ∈ V ∧ N ∈ V
14 5 12 13 sylanbrc ⊢ G S ∈ CVec OLD ∧ N : X ⟶ ℝ → G ∈ V ∧ S ∈ V ∧ N ∈ V
15 14 3adant3 ⊢ G S ∈ CVec OLD ∧ N : X ⟶ ℝ ∧ ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y S x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x G y ≤ N ⁡ x + N ⁡ y → G ∈ V ∧ S ∈ V ∧ N ∈ V
16 1 2 isnvlem ⊢ G ∈ V ∧ S ∈ V ∧ N ∈ V → G S N ∈ NrmCVec ↔ G S ∈ CVec OLD ∧ N : X ⟶ ℝ ∧ ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y S x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x G y ≤ N ⁡ x + N ⁡ y
17 3 15 16 pm5.21nii ⊢ G S N ∈ NrmCVec ↔ G S ∈ CVec OLD ∧ N : X ⟶ ℝ ∧ ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y S x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x G y ≤ N ⁡ x + N ⁡ y