Metamath Proof Explorer

Theorem nmoo0

Description: The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoo0.3 ⊢N=UnormOpOLDW
nmoo0.0 ⊢Z=U0opW
Assertion nmoo0 ⊢U∈NrmCVec∧W∈NrmCVec→N⁡Z=0

Proof

Step Hyp Ref Expression
1 nmoo0.3 ⊢N=UnormOpOLDW
2 nmoo0.0 ⊢Z=U0opW
3 eqid ⊢BaseSet⁡U=BaseSet⁡U
4 eqid ⊢BaseSet⁡W=BaseSet⁡W
5 3 4 2 0oo ⊢U∈NrmCVec∧W∈NrmCVec→Z:BaseSet⁡U⟶BaseSet⁡W
6 eqid ⊢normCV⁡U=normCV⁡U
7 eqid ⊢normCV⁡W=normCV⁡W
8 3 4 6 7 1 nmooval ⊢U∈NrmCVec∧W∈NrmCVec∧Z:BaseSet⁡U⟶BaseSet⁡W→N⁡Z=supx|∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡zℝ*<
9 5 8 mpd3an3 ⊢U∈NrmCVec∧W∈NrmCVec→N⁡Z=supx|∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡zℝ*<
10 df-sn ⊢0=x|x=0
11 eqid ⊢0vec⁡U=0vec⁡U
12 3 11 nvzcl ⊢U∈NrmCVec→0vec⁡U∈BaseSet⁡U
13 11 6 nvz0 ⊢U∈NrmCVec→normCV⁡U⁡0vec⁡U=0
14 0le1 ⊢0≤1
15 13 14 eqbrtrdi ⊢U∈NrmCVec→normCV⁡U⁡0vec⁡U≤1
16 fveq2 ⊢z=0vec⁡U→normCV⁡U⁡z=normCV⁡U⁡0vec⁡U
17 16 breq1d ⊢z=0vec⁡U→normCV⁡U⁡z≤1↔normCV⁡U⁡0vec⁡U≤1
18 17 rspcev ⊢0vec⁡U∈BaseSet⁡U∧normCV⁡U⁡0vec⁡U≤1→∃z∈BaseSet⁡UnormCV⁡U⁡z≤1
19 12 15 18 syl2anc ⊢U∈NrmCVec→∃z∈BaseSet⁡UnormCV⁡U⁡z≤1
20 19 biantrurd ⊢U∈NrmCVec→x=0↔∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=0
21 20 adantr ⊢U∈NrmCVec∧W∈NrmCVec→x=0↔∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=0
22 eqid ⊢0vec⁡W=0vec⁡W
23 3 22 2 0oval ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→Z⁡z=0vec⁡W
24 23 3expa ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→Z⁡z=0vec⁡W
25 24 fveq2d ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→normCV⁡W⁡Z⁡z=normCV⁡W⁡0vec⁡W
26 22 7 nvz0 ⊢W∈NrmCVec→normCV⁡W⁡0vec⁡W=0
27 26 ad2antlr ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→normCV⁡W⁡0vec⁡W=0
28 25 27 eqtrd ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→normCV⁡W⁡Z⁡z=0
29 28 eqeq2d ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→x=normCV⁡W⁡Z⁡z↔x=0
30 29 anbi2d ⊢U∈NrmCVec∧W∈NrmCVec∧z∈BaseSet⁡U→normCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡z↔normCV⁡U⁡z≤1∧x=0
31 30 rexbidva ⊢U∈NrmCVec∧W∈NrmCVec→∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡z↔∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=0
32 r19.41v ⊢∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=0↔∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=0
33 31 32 bitr2di ⊢U∈NrmCVec∧W∈NrmCVec→∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=0↔∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡z
34 21 33 bitrd ⊢U∈NrmCVec∧W∈NrmCVec→x=0↔∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡z
35 34 abbidv ⊢U∈NrmCVec∧W∈NrmCVec→x|x=0=x|∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡z
36 10 35 eqtr2id ⊢U∈NrmCVec∧W∈NrmCVec→x|∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡z=0
37 36 supeq1d ⊢U∈NrmCVec∧W∈NrmCVec→supx|∃z∈BaseSet⁡UnormCV⁡U⁡z≤1∧x=normCV⁡W⁡Z⁡zℝ*<=sup0ℝ*<
38 9 37 eqtrd ⊢U∈NrmCVec∧W∈NrmCVec→N⁡Z=sup0ℝ*<
39 xrltso ⊢<Orℝ*
40 0xr ⊢0∈ℝ*
41 supsn ⊢<Orℝ*∧0∈ℝ*→sup0ℝ*<=0
42 39 40 41 mp2an ⊢sup0ℝ*<=0
43 38 42 eqtrdi ⊢U∈NrmCVec∧W∈NrmCVec→N⁡Z=0