Theorem nmoval

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	nmoval	|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )

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	1 2 3 4	nmofval	|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )
6	5	fveq1d	|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` F ) = ( ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) ` F ) )
7		fveq1	|- ( f = F -> ( f ` x ) = ( F ` x ) )
8	7	fveq2d	|- ( f = F -> ( M ` ( f ` x ) ) = ( M ` ( F ` x ) ) )
9	8	breq1d	|- ( f = F -> ( ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) <-> ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) ) )
10	9	ralbidv	|- ( f = F -> ( A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) <-> A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) ) )
11	10	rabbidv	|- ( f = F -> { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } = { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } )
12	11	infeq1d	|- ( f = F -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
13		eqid	|- ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
14		xrltso	|- < Or RR*
15	14	infex	|- inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. _V
16	12 13 15	fvmpt	|- ( F e. ( S GrpHom T ) -> ( ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) ` F ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
17	6 16	sylan9eq	|- ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ F e. ( S GrpHom T ) ) -> ( N ` F ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
18	17	3impa	|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )