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 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmoo0.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
Assertion nmoo0 ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑁 ‘ 𝑍 ) = 0 )

Proof

Step Hyp Ref Expression
1 nmoo0.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2 nmoo0.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
3 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
4 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
5 3 4 2 0oo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) )
6 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
7 eqid ⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
8 3 4 6 7 1 nmooval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑍 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑍 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
9 5 8 mpd3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑁 ‘ 𝑍 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
10 df-sn ⊢ { 0 } = { 𝑥 ∣ 𝑥 = 0 }
11 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
12 3 11 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → ( 0vec ‘ 𝑈 ) ∈ ( BaseSet ‘ 𝑈 ) )
13 11 6 nvz0 ⊢ ( 𝑈 ∈ NrmCVec → ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) = 0 )
14 0le1 ⊢ 0 ≤ 1
15 13 14 eqbrtrdi ⊢ ( 𝑈 ∈ NrmCVec → ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ≤ 1 )
16 fveq2 ⊢ ( 𝑧 = ( 0vec ‘ 𝑈 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) )
17 16 breq1d ⊢ ( 𝑧 = ( 0vec ‘ 𝑈 ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ↔ ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ≤ 1 ) )
18 17 rspcev ⊢ ( ( ( 0vec ‘ 𝑈 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ ( ( normCV ‘ 𝑈 ) ‘ ( 0vec ‘ 𝑈 ) ) ≤ 1 ) → ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 )
19 12 15 18 syl2anc ⊢ ( 𝑈 ∈ NrmCVec → ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 )
20 19 biantrurd ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 = 0 ↔ ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
21 20 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑥 = 0 ↔ ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
22 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
23 3 22 2 0oval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑍 ‘ 𝑧 ) = ( 0vec ‘ 𝑊 ) )
24 23 3expa ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑍 ‘ 𝑧 ) = ( 0vec ‘ 𝑊 ) )
25 24 fveq2d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( 0vec ‘ 𝑊 ) ) )
26 22 7 nvz0 ⊢ ( 𝑊 ∈ NrmCVec → ( ( normCV ‘ 𝑊 ) ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
27 26 ad2antlr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
28 25 27 eqtrd ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) = 0 )
29 28 eqeq2d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ↔ 𝑥 = 0 ) )
30 29 anbi2d ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) ↔ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
31 30 rexbidva ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
32 r19.41v ⊢ ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) )
33 31 32 bitr2di ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) ) )
34 21 33 bitrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑥 = 0 ↔ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) ) )
35 34 abbidv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → { 𝑥 ∣ 𝑥 = 0 } = { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) } )
36 10 35 syl5req ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) } = { 0 } )
37 36 supeq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑍 ‘ 𝑧 ) ) ) } , ℝ* , < ) = sup ( { 0 } , ℝ* , < ) )
38 9 37 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑁 ‘ 𝑍 ) = 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 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑁 ‘ 𝑍 ) = 0 )