Metamath Proof Explorer

Theorem isnvlem

Description: Lemma for isnv . (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isnvlem.1 ⊢ 𝑋 = ran 𝐺
isnvlem.2 ⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion isnvlem ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isnvlem.1 ⊢ 𝑋 = ran 𝐺
2 isnvlem.2 ⊢ 𝑍 = ( GId ‘ 𝐺 )
3 df-nv ⊢ NrmCVec = { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) }
4 3 eleq2i ⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) } )
5 opeq1 ⊢ ( 𝑔 = 𝐺 → ⟨ 𝑔 , 𝑠 ⟩ = ⟨ 𝐺 , 𝑠 ⟩ )
6 5 eleq1d ⊢ ( 𝑔 = 𝐺 → ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ↔ ⟨ 𝐺 , 𝑠 ⟩ ∈ CVecOLD ) )
7 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
8 7 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
9 8 feq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑛 : ran 𝑔 ⟶ ℝ ↔ 𝑛 : 𝑋 ⟶ ℝ ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = ( GId ‘ 𝐺 ) )
11 10 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = 𝑍 )
12 11 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 = ( GId ‘ 𝑔 ) ↔ 𝑥 = 𝑍 ) )
13 12 imbi2d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ↔ ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ) )
14 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
15 14 fveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) )
16 15 breq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ↔ ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) )
17 8 16 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) )
18 13 17 3anbi13d ⊢ ( 𝑔 = 𝐺 → ( ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) )
19 8 18 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) )
20 6 9 19 3anbi123d ⊢ ( 𝑔 = 𝐺 → ( ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ↔ ( ⟨ 𝐺 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) )
21 opeq2 ⊢ ( 𝑠 = 𝑆 → ⟨ 𝐺 , 𝑠 ⟩ = ⟨ 𝐺 , 𝑆 ⟩ )
22 21 eleq1d ⊢ ( 𝑠 = 𝑆 → ( ⟨ 𝐺 , 𝑠 ⟩ ∈ CVecOLD ↔ ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ) )
23 oveq ⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 𝑥 ) = ( 𝑦 𝑆 𝑥 ) )
24 23 fveqeq2d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ↔ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ) )
25 24 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ) )
26 25 3anbi2d ⊢ ( 𝑠 = 𝑆 → ( ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) )
27 26 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) )
28 22 27 3anbi13d ⊢ ( 𝑠 = 𝑆 → ( ( ⟨ 𝐺 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑛 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ) )
29 feq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 : 𝑋 ⟶ ℝ ↔ 𝑁 : 𝑋 ⟶ ℝ ) )
30 fveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) )
31 30 eqeq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ 𝑥 ) = 0 ↔ ( 𝑁 ‘ 𝑥 ) = 0 ) )
32 31 imbi1d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ↔ ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ) )
33 fveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) )
34 30 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
35 33 34 eqeq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ↔ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
36 35 ralbidv ⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
37 fveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) )
38 fveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
39 30 38 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
40 37 39 breq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
41 40 ralbidv ⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
42 32 36 41 3anbi123d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
43 42 ralbidv ⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
44 29 43 3anbi23d ⊢ ( 𝑛 = 𝑁 → ( ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑛 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑛 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )
45 20 28 44 eloprabg ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) } ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )
46 4 45 syl5bb ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )