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 |
|
elrege0 |
|- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) ) |
6 |
1 2 3 4
|
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* , < ) ) |
7 |
|
ssrab2 |
|- { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ ( 0 [,) +oo ) |
8 |
|
icossxr |
|- ( 0 [,) +oo ) C_ RR* |
9 |
7 8
|
sstri |
|- { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR* |
10 |
|
infxrcl |
|- ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR* -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. RR* ) |
11 |
9 10
|
mp1i |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. RR* ) |
12 |
6 11
|
eqeltrd |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* ) |
13 |
12
|
xrleidd |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) <_ ( N ` F ) ) |
14 |
1 2 3 4
|
nmogelb |
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) e. RR* ) -> ( ( N ` F ) <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) ) ) |
15 |
12 14
|
mpdan |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) ) ) |
16 |
13 15
|
mpbid |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) ) |
17 |
|
oveq1 |
|- ( r = A -> ( r x. ( L ` x ) ) = ( A x. ( L ` x ) ) ) |
18 |
17
|
breq2d |
|- ( r = A -> ( ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) <-> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) ) |
19 |
18
|
ralbidv |
|- ( r = A -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) <-> A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) ) |
20 |
|
breq2 |
|- ( r = A -> ( ( N ` F ) <_ r <-> ( N ` F ) <_ A ) ) |
21 |
19 20
|
imbi12d |
|- ( r = A -> ( ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) <-> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) ) |
22 |
21
|
rspccv |
|- ( A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( N ` F ) <_ r ) -> ( A e. ( 0 [,) +oo ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) ) |
23 |
16 22
|
syl |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( A e. ( 0 [,) +oo ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) ) |
24 |
5 23
|
syl5bir |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) ) |
25 |
24
|
3impib |
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) ) |