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 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) )