Metamath Proof Explorer

Theorem nmofval

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

Ref Expression
Hypotheses nmofval.1 ⊢ N = S normOp T
nmofval.2 ⊢ V = Base S
nmofval.3 ⊢ L = norm ⁡ S
nmofval.4 ⊢ M = norm ⁡ T
Assertion nmofval ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N = f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ N = S normOp T
2 nmofval.2 ⊢ V = Base S
3 nmofval.3 ⊢ L = norm ⁡ S
4 nmofval.4 ⊢ M = norm ⁡ T
5 oveq12 ⊢ s = S ∧ t = T → s GrpHom t = S GrpHom T
6 simpl ⊢ s = S ∧ t = T → s = S
7 6 fveq2d ⊢ s = S ∧ t = T → Base s = Base S
8 7 2 eqtr4di ⊢ s = S ∧ t = T → Base s = V
9 simpr ⊢ s = S ∧ t = T → t = T
10 9 fveq2d ⊢ s = S ∧ t = T → norm ⁡ t = norm ⁡ T
11 10 4 eqtr4di ⊢ s = S ∧ t = T → norm ⁡ t = M
12 11 fveq1d ⊢ s = S ∧ t = T → norm ⁡ t ⁡ f ⁡ x = M ⁡ f ⁡ x
13 6 fveq2d ⊢ s = S ∧ t = T → norm ⁡ s = norm ⁡ S
14 13 3 eqtr4di ⊢ s = S ∧ t = T → norm ⁡ s = L
15 14 fveq1d ⊢ s = S ∧ t = T → norm ⁡ s ⁡ x = L ⁡ x
16 15 oveq2d ⊢ s = S ∧ t = T → r ⁢ norm ⁡ s ⁡ x = r ⁢ L ⁡ x
17 12 16 breq12d ⊢ s = S ∧ t = T → norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ↔ M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x
18 8 17 raleqbidv ⊢ s = S ∧ t = T → ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ↔ ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x
19 18 rabbidv ⊢ s = S ∧ t = T → r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x = r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x
20 19 infeq1d ⊢ s = S ∧ t = T → sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < = sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
21 5 20 mpteq12dv ⊢ s = S ∧ t = T → f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * < = f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
22 df-nmo ⊢ normOp = s ∈ NrmGrp , t ∈ NrmGrp ⟼ f ∈ s GrpHom t ⟼ sup r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <
23 eqid ⊢ f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < = f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
24 ssrab2 ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ⊆ 0 +∞
25 icossxr ⊢ 0 +∞ ⊆ ℝ *
26 24 25 sstri ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ⊆ ℝ *
27 infxrcl ⊢ r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ⊆ ℝ * → sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ ℝ *
28 26 27 mp1i ⊢ f ∈ S GrpHom T → sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ ℝ *
29 23 28 fmpti ⊢ f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < : S GrpHom T ⟶ ℝ *
30 ovex ⊢ S GrpHom T ∈ V
31 xrex ⊢ ℝ * ∈ V
32 fex2 ⊢ f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < : S GrpHom T ⟶ ℝ * ∧ S GrpHom T ∈ V ∧ ℝ * ∈ V → f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ V
33 29 30 31 32 mp3an ⊢ f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * < ∈ V
34 21 22 33 ovmpoa ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → S normOp T = f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <
35 1 34 syl5eq ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → N = f ∈ S GrpHom T ⟼ sup r ∈ 0 +∞ | ∀ x ∈ V M ⁡ f ⁡ x ≤ r ⁢ L ⁡ x ℝ * <