| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑤 = 〈𝑔, 𝑠〉 → (𝑤 ∈ CVecOLD ↔ 〈𝑔, 𝑠〉 ∈
CVecOLD)) | 
| 2 | 1 | biimpar 477 | . . . . . 6
⊢ ((𝑤 = 〈𝑔, 𝑠〉 ∧ 〈𝑔, 𝑠〉 ∈ CVecOLD) →
𝑤 ∈
CVecOLD) | 
| 3 | 2 | 3ad2antr1 1188 | . . . . 5
⊢ ((𝑤 = 〈𝑔, 𝑠〉 ∧ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))) → 𝑤 ∈ CVecOLD) | 
| 4 | 3 | exlimivv 1931 | . . . 4
⊢
(∃𝑔∃𝑠(𝑤 = 〈𝑔, 𝑠〉 ∧ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))) → 𝑤 ∈ CVecOLD) | 
| 5 |  | vex 3483 | . . . 4
⊢ 𝑛 ∈ V | 
| 6 | 4, 5 | jctir 520 | . . 3
⊢
(∃𝑔∃𝑠(𝑤 = 〈𝑔, 𝑠〉 ∧ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))) → (𝑤 ∈ CVecOLD ∧ 𝑛 ∈ V)) | 
| 7 | 6 | ssopab2i 5554 | . 2
⊢
{〈𝑤, 𝑛〉 ∣ ∃𝑔∃𝑠(𝑤 = 〈𝑔, 𝑠〉 ∧ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)))))} ⊆ {〈𝑤, 𝑛〉 ∣ (𝑤 ∈ CVecOLD ∧ 𝑛 ∈ V)} | 
| 8 |  | df-nv 30612 | . . 3
⊢ NrmCVec =
{〈〈𝑔, 𝑠〉, 𝑛〉 ∣ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))} | 
| 9 |  | dfoprab2 7492 | . . 3
⊢
{〈〈𝑔,
𝑠〉, 𝑛〉 ∣ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))} = {〈𝑤, 𝑛〉 ∣ ∃𝑔∃𝑠(𝑤 = 〈𝑔, 𝑠〉 ∧ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)))))} | 
| 10 | 8, 9 | eqtri 2764 | . 2
⊢ NrmCVec =
{〈𝑤, 𝑛〉 ∣ ∃𝑔∃𝑠(𝑤 = 〈𝑔, 𝑠〉 ∧ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)))))} | 
| 11 |  | df-xp 5690 | . 2
⊢
(CVecOLD × V) = {〈𝑤, 𝑛〉 ∣ (𝑤 ∈ CVecOLD ∧ 𝑛 ∈ V)} | 
| 12 | 7, 10, 11 | 3sstr4i 4034 | 1
⊢ NrmCVec
⊆ (CVecOLD × V) |