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

Metamath Proof Explorer

Theorem nmogelb

Description: Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

		Ref	Expression
	Hypotheses	nmofval.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
		nmofval.2	⊢ 𝑉 = ( Base ‘ 𝑆 )
		nmofval.3	⊢ 𝐿 = ( norm ‘ 𝑆 )
		nmofval.4	⊢ 𝑀 = ( norm ‘ 𝑇 )
	Assertion	nmogelb	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ^* ) → ( 𝐴 ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → 𝐴 ≤ 𝑟 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2		nmofval.2	⊢ 𝑉 = ( Base ‘ 𝑆 )
3		nmofval.3	⊢ 𝐿 = ( norm ‘ 𝑆 )
4		nmofval.4	⊢ 𝑀 = ( norm ‘ 𝑇 )
5	1 2 3 4	nmoval	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ^* , < ) )
6	5	breq2d	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐴 ≤ ( 𝑁 ‘ 𝐹 ) ↔ 𝐴 ≤ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ^* , < ) ) )
7		ssrab2	⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ( 0 [,) +∞ )
8		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ^*
9	7 8	sstri	⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ℝ^*
10		infxrgelb	⊢ ( ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( 𝐴 ≤ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ^* , < ) ↔ ∀ 𝑠 ∈ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } 𝐴 ≤ 𝑠 ) )
11	9 10	mpan	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐴 ≤ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ^* , < ) ↔ ∀ 𝑠 ∈ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } 𝐴 ≤ 𝑠 ) )
12		breq2	⊢ ( 𝑠 = 𝑟 → ( 𝐴 ≤ 𝑠 ↔ 𝐴 ≤ 𝑟 ) )
13	12	ralrab2	⊢ ( ∀ 𝑠 ∈ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } 𝐴 ≤ 𝑠 ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → 𝐴 ≤ 𝑟 ) )
14	11 13	bitrdi	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐴 ≤ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ^* , < ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → 𝐴 ≤ 𝑟 ) ) )
15	6 14	sylan9bb	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ^* ) → ( 𝐴 ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → 𝐴 ≤ 𝑟 ) ) )