This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ≤ ( 𝑁 ‘ 𝐹 ) )