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