Metamath Proof Explorer


Theorem nmoge0

Description: The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypothesis nmofval.1 𝑁 = ( 𝑆 normOp 𝑇 )
Assertion nmoge0 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁𝐹 ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 𝑁 = ( 𝑆 normOp 𝑇 )
2 elrege0 ( 𝑟 ∈ ( 0 [,) +∞ ) ↔ ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ) )
3 2 simprbi ( 𝑟 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑟 )
4 3 adantl ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝑟 )
5 4 a1d ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) )
6 5 ralrimiva ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) )
7 0xr 0 ∈ ℝ*
8 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9 eqid ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
10 eqid ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
11 1 8 9 10 nmogelb ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 0 ∈ ℝ* ) → ( 0 ≤ ( 𝑁𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) ) )
12 7 11 mpan2 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 0 ≤ ( 𝑁𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) ) )
13 6 12 mpbird ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁𝐹 ) )