This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmoofval

Description: The operator norm function. (Contributed by NM, 6-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 nmoofval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑁 = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ 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 fveq2 ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
7 6 1 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
8 7 oveq2d ⊢ ( 𝑢 = 𝑈 → ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) = ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) )
9 fveq2 ⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = ( normCV ‘ 𝑈 ) )
10 9 3 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = 𝐿 )
11 10 fveq1d ⊢ ( 𝑢 = 𝑈 → ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) = ( 𝐿 ‘ 𝑧 ) )
12 11 breq1d ⊢ ( 𝑢 = 𝑈 → ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ↔ ( 𝐿 ‘ 𝑧 ) ≤ 1 ) )
13 12 anbi1d ⊢ ( 𝑢 = 𝑈 → ( ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
14 7 13 rexeqbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
15 14 abbidv ⊢ ( 𝑢 = 𝑈 → { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } )
16 15 supeq1d ⊢ ( 𝑢 = 𝑈 → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
17 8 16 mpteq12dv ⊢ ( 𝑢 = 𝑈 → ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) = ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
18 fveq2 ⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = ( BaseSet ‘ 𝑊 ) )
19 18 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = 𝑌 )
20 19 oveq1d ⊢ ( 𝑤 = 𝑊 → ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) = ( 𝑌 ↑m 𝑋 ) )
21 fveq2 ⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = ( normCV ‘ 𝑊 ) )
22 21 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = 𝑀 )
23 22 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) )
24 23 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) )
25 24 anbi2d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
26 25 rexbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
27 26 abbidv ⊢ ( 𝑤 = 𝑊 → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } )
28 27 supeq1d ⊢ ( 𝑤 = 𝑊 → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
29 20 28 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
30 df-nmoo ⊢ normOpOLD = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
31 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
32 31 mptex ⊢ ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) ∈ V
33 17 29 30 32 ovmpo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 normOpOLD 𝑊 ) = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
34 5 33 eqtrid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑁 = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )