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

Metamath Proof Explorer

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* , < ) )