Metamath Proof Explorer

Theorem nmooval

Description: The operator norm function. (Contributed by NM, 27-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoofval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoofval.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoofval.3 ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmoofval.4 ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmoofval.6 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
Assertion nmooval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 nmoofval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoofval.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoofval.3 ⊢ 𝐿 = ( normCV ‘ 𝑈 )
4 nmoofval.4 ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmoofval.6 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 2 fvexi ⊢ 𝑌 ∈ V
7 1 fvexi ⊢ 𝑋 ∈ V
8 6 7 elmap ⊢ ( 𝑇 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑇 : 𝑋 ⟶ 𝑌 )
9 1 2 3 4 5 nmoofval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑁 = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
10 9 fveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑁 ‘ 𝑇 ) = ( ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) ‘ 𝑇 ) )
11 fveq1 ⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑧 ) )
12 11 fveq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) )
13 12 eqeq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
14 13 anbi2d ⊢ ( 𝑡 = 𝑇 → ( ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) )
15 14 rexbidv ⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) )
16 15 abbidv ⊢ ( 𝑡 = 𝑇 → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } )
17 16 supeq1d ⊢ ( 𝑡 = 𝑇 → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
18 eqid ⊢ ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
19 xrltso ⊢ < Or ℝ*
20 19 supex ⊢ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) ∈ V
21 17 18 20 fvmpt ⊢ ( 𝑇 ∈ ( 𝑌 ↑m 𝑋 ) → ( ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
22 10 21 sylan9eq ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑇 ∈ ( 𝑌 ↑m 𝑋 ) ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
23 8 22 sylan2br ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
24 23 3impa ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )