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

Proof

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