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 ⊢N=SnormOpT
Assertion nmoge0 ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→0≤N⁡F

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢N=SnormOpT
2 elrege0 ⊢r∈0+∞↔r∈ℝ∧0≤r
3 2 simprbi ⊢r∈0+∞→0≤r
4 3 adantl ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT∧r∈0+∞→0≤r
5 4 a1d ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT∧r∈0+∞→∀x∈BaseSnorm⁡T⁡F⁡x≤r⁢norm⁡S⁡x→0≤r
6 5 ralrimiva ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→∀r∈0+∞∀x∈BaseSnorm⁡T⁡F⁡x≤r⁢norm⁡S⁡x→0≤r
7 0xr ⊢0∈ℝ*
8 eqid ⊢BaseS=BaseS
9 eqid ⊢norm⁡S=norm⁡S
10 eqid ⊢norm⁡T=norm⁡T
11 1 8 9 10 nmogelb ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT∧0∈ℝ*→0≤N⁡F↔∀r∈0+∞∀x∈BaseSnorm⁡T⁡F⁡x≤r⁢norm⁡S⁡x→0≤r
12 7 11 mpan2 ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→0≤N⁡F↔∀r∈0+∞∀x∈BaseSnorm⁡T⁡F⁡x≤r⁢norm⁡S⁡x→0≤r
13 6 12 mpbird ⊢S∈NrmGrp∧T∈NrmGrp∧F∈SGrpHomT→0≤N⁡F