Step |
Hyp |
Ref |
Expression |
1 |
|
nmofval.1 |
|- N = ( S normOp T ) |
2 |
|
elrege0 |
|- ( r e. ( 0 [,) +oo ) <-> ( r e. RR /\ 0 <_ r ) ) |
3 |
2
|
simprbi |
|- ( r e. ( 0 [,) +oo ) -> 0 <_ r ) |
4 |
3
|
adantl |
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ r e. ( 0 [,) +oo ) ) -> 0 <_ r ) |
5 |
4
|
a1d |
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ r e. ( 0 [,) +oo ) ) -> ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) ) |
6 |
5
|
ralrimiva |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> A. r e. ( 0 [,) +oo ) ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) ) |
7 |
|
0xr |
|- 0 e. RR* |
8 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
9 |
|
eqid |
|- ( norm ` S ) = ( norm ` S ) |
10 |
|
eqid |
|- ( norm ` T ) = ( norm ` T ) |
11 |
1 8 9 10
|
nmogelb |
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ 0 e. RR* ) -> ( 0 <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) ) ) |
12 |
7 11
|
mpan2 |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( 0 <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) ) ) |
13 |
6 12
|
mpbird |
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) ) |