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

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 ⊆ ( CVecOLD × V )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ → ( 𝑤 ∈ CVecOLD ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ) )
2 1 biimpar ⊢ ( ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ) → 𝑤 ∈ CVecOLD )
3 2 3ad2antr1 ⊢ ( ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) → 𝑤 ∈ CVecOLD )
4 3 exlimivv ⊢ ( ∃ 𝑔 ∃ 𝑠 ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) → 𝑤 ∈ CVecOLD )
5 vex ⊢ 𝑛 ∈ V
6 4 5 jctir ⊢ ( ∃ 𝑔 ∃ 𝑠 ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) → ( 𝑤 ∈ CVecOLD ∧ 𝑛 ∈ V ) )
7 6 ssopab2i ⊢ { ⟨ 𝑤 , 𝑛 ⟩ ∣ ∃ 𝑔 ∃ 𝑠 ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) } ⊆ { ⟨ 𝑤 , 𝑛 ⟩ ∣ ( 𝑤 ∈ CVecOLD ∧ 𝑛 ∈ V ) }
8 df-nv ⊢ NrmCVec = { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) }
9 dfoprab2 ⊢ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) } = { ⟨ 𝑤 , 𝑛 ⟩ ∣ ∃ 𝑔 ∃ 𝑠 ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) }
10 8 9 eqtri ⊢ NrmCVec = { ⟨ 𝑤 , 𝑛 ⟩ ∣ ∃ 𝑔 ∃ 𝑠 ( 𝑤 = ⟨ 𝑔 , 𝑠 ⟩ ∧ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) }
11 df-xp ⊢ ( CVecOLD × V ) = { ⟨ 𝑤 , 𝑛 ⟩ ∣ ( 𝑤 ∈ CVecOLD ∧ 𝑛 ∈ V ) }
12 7 10 11 3sstr4i ⊢ NrmCVec ⊆ ( CVecOLD × V )