Metamath Proof Explorer

Theorem nmo0

Description: The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nmo0.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmo0.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmo0.3 ⊢ 0 = ( 0g ‘ 𝑇 )
Assertion nmo0 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 nmo0.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmo0.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmo0.3 ⊢ 0 = ( 0g ‘ 𝑇 )
4 eqid ⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
5 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
6 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
7 simpl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑆 ∈ NrmGrp )
8 simpr ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑇 ∈ NrmGrp )
9 ngpgrp ⊢ ( 𝑆 ∈ NrmGrp → 𝑆 ∈ Grp )
10 ngpgrp ⊢ ( 𝑇 ∈ NrmGrp → 𝑇 ∈ Grp )
11 3 2 0ghm ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) )
12 9 10 11 syl2an ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) )
13 0red ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 0 ∈ ℝ )
14 0le0 ⊢ 0 ≤ 0
15 14 a1i ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 0 ≤ 0 )
16 3 fvexi ⊢ 0 ∈ V
17 16 fvconst2 ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) = 0 )
18 17 ad2antrl ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) = 0 )
19 18 fveq2d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 0 ) )
20 5 3 nm0 ⊢ ( 𝑇 ∈ NrmGrp → ( ( norm ‘ 𝑇 ) ‘ 0 ) = 0 )
21 20 ad2antlr ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ 0 ) = 0 )
22 19 21 eqtrd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) = 0 )
23 2 4 nmcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
24 23 ad2ant2r ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
25 24 recnd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℂ )
26 25 mul02d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 0 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = 0 )
27 14 26 breqtrrid ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 0 ≤ ( 0 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
28 22 27 eqbrtrd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) ≤ ( 0 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
29 1 2 4 5 6 7 8 12 13 15 28 nmolb2d ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ≤ 0 )
30 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) )
31 12 30 mpd3an3 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 0 ≤ ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) )
32 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ∈ ℝ* )
33 12 32 mpd3an3 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ∈ ℝ* )
34 0xr ⊢ 0 ∈ ℝ*
35 xrletri3 ⊢ ( ( ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 ↔ ( ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ≤ 0 ∧ 0 ≤ ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ) ) )
36 33 34 35 sylancl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 ↔ ( ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ≤ 0 ∧ 0 ≤ ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) ) ) )
37 29 31 36 mpbir2and ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 )