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