Metamath Proof Explorer

Theorem nvss

Description: Structure of the class of all normed complex vectors spaces. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 1-May-2015) (New usage is discouraged.)

Ref Expression
Assertion nvss ⊢ NrmCVec ⊆ CVec OLD × V

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ w = g s → w ∈ CVec OLD ↔ g s ∈ CVec OLD
2 1 biimpar ⊢ w = g s ∧ g s ∈ CVec OLD → w ∈ CVec OLD
3 2 3ad2antr1 ⊢ w = g s ∧ g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y → w ∈ CVec OLD
4 3 exlimivv ⊢ ∃ g ∃ s w = g s ∧ g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y → w ∈ CVec OLD
5 vex ⊢ n ∈ V
6 4 5 jctir ⊢ ∃ g ∃ s w = g s ∧ g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y → w ∈ CVec OLD ∧ n ∈ V
7 6 ssopab2i ⊢ w n | ∃ g ∃ s w = g s ∧ g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y ⊆ w n | w ∈ CVec OLD ∧ n ∈ V
8 df-nv ⊢ NrmCVec = g s n | g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y
9 dfoprab2 ⊢ g s n | g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y = w n | ∃ g ∃ s w = g s ∧ g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y
10 8 9 eqtri ⊢ NrmCVec = w n | ∃ g ∃ s w = g s ∧ g s ∈ CVec OLD ∧ n : ran ⁡ g ⟶ ℝ ∧ ∀ x ∈ ran ⁡ g n ⁡ x = 0 → x = GId ⁡ g ∧ ∀ y ∈ ℂ n ⁡ y s x = y ⁢ n ⁡ x ∧ ∀ y ∈ ran ⁡ g n ⁡ x g y ≤ n ⁡ x + n ⁡ y
11 df-xp ⊢ CVec OLD × V = w n | w ∈ CVec OLD ∧ n ∈ V
12 7 10 11 3sstr4i ⊢ NrmCVec ⊆ CVec OLD × V