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 ⊢X=BaseSet⁡U
nmoofval.2 ⊢Y=BaseSet⁡W
nmoofval.3 ⊢L=normCV⁡U
nmoofval.4 ⊢M=normCV⁡W
nmoofval.6 ⊢N=UnormOpOLDW
Assertion nmooval ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T=supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<

Proof

Step Hyp Ref Expression
1 nmoofval.1 ⊢X=BaseSet⁡U
2 nmoofval.2 ⊢Y=BaseSet⁡W
3 nmoofval.3 ⊢L=normCV⁡U
4 nmoofval.4 ⊢M=normCV⁡W
5 nmoofval.6 ⊢N=UnormOpOLDW
6 2 fvexi ⊢Y∈V
7 1 fvexi ⊢X∈V
8 6 7 elmap ⊢T∈YX↔T:X⟶Y
9 1 2 3 4 5 nmoofval ⊢U∈NrmCVec∧W∈NrmCVec→N=t∈YX⟼supx|∃z∈XL⁡z≤1∧x=M⁡t⁡zℝ*<
10 9 fveq1d ⊢U∈NrmCVec∧W∈NrmCVec→N⁡T=t∈YX⟼supx|∃z∈XL⁡z≤1∧x=M⁡t⁡zℝ*<⁡T
11 fveq1 ⊢t=T→t⁡z=T⁡z
12 11 fveq2d ⊢t=T→M⁡t⁡z=M⁡T⁡z
13 12 eqeq2d ⊢t=T→x=M⁡t⁡z↔x=M⁡T⁡z
14 13 anbi2d ⊢t=T→L⁡z≤1∧x=M⁡t⁡z↔L⁡z≤1∧x=M⁡T⁡z
15 14 rexbidv ⊢t=T→∃z∈XL⁡z≤1∧x=M⁡t⁡z↔∃z∈XL⁡z≤1∧x=M⁡T⁡z
16 15 abbidv ⊢t=T→x|∃z∈XL⁡z≤1∧x=M⁡t⁡z=x|∃z∈XL⁡z≤1∧x=M⁡T⁡z
17 16 supeq1d ⊢t=T→supx|∃z∈XL⁡z≤1∧x=M⁡t⁡zℝ*<=supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<
18 eqid ⊢t∈YX⟼supx|∃z∈XL⁡z≤1∧x=M⁡t⁡zℝ*<=t∈YX⟼supx|∃z∈XL⁡z≤1∧x=M⁡t⁡zℝ*<
19 xrltso ⊢<Orℝ*
20 19 supex ⊢supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<∈V
21 17 18 20 fvmpt ⊢T∈YX→t∈YX⟼supx|∃z∈XL⁡z≤1∧x=M⁡t⁡zℝ*<⁡T=supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<
22 10 21 sylan9eq ⊢U∈NrmCVec∧W∈NrmCVec∧T∈YX→N⁡T=supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<
23 8 22 sylan2br ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T=supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<
24 23 3impa ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T=supx|∃z∈XL⁡z≤1∧x=M⁡T⁡zℝ*<