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 = U normOp OLD W
nmoo0.0 ⊢ Z = U 0 op W
Assertion nmoo0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → N ⁡ Z = 0

Proof

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