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 ) |