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 )