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

Metamath Proof Explorer

Theorem nmoleub2lem

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015)

Ref Expression
Hypotheses nmoleub2.n 
|- N = ( S normOp T )
nmoleub2.v 
|- V = ( Base ` S )
nmoleub2.l 
|- L = ( norm ` S )
nmoleub2.m 
|- M = ( norm ` T )
nmoleub2.g 
|- G = ( Scalar ` S )
nmoleub2.w 
|- K = ( Base ` G )
nmoleub2.s 
|- ( ph -> S e. ( NrmMod i^i CMod ) )
nmoleub2.t 
|- ( ph -> T e. ( NrmMod i^i CMod ) )
nmoleub2.f 
|- ( ph -> F e. ( S LMHom T ) )
nmoleub2.a 
|- ( ph -> A e. RR* )
nmoleub2.r 
|- ( ph -> R e. RR+ )
nmoleub2lem.5 
|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )
nmoleub2lem.6 
|- ( ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
nmoleub2lem.7 
|- ( ( ph /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )
Assertion nmoleub2lem 
|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )

Proof

Step Hyp Ref Expression
1 nmoleub2.n 
 |-  N = ( S normOp T )
2 nmoleub2.v 
 |-  V = ( Base ` S )
3 nmoleub2.l 
 |-  L = ( norm ` S )
4 nmoleub2.m 
 |-  M = ( norm ` T )
5 nmoleub2.g 
 |-  G = ( Scalar ` S )
6 nmoleub2.w 
 |-  K = ( Base ` G )
7 nmoleub2.s 
 |-  ( ph -> S e. ( NrmMod i^i CMod ) )
8 nmoleub2.t 
 |-  ( ph -> T e. ( NrmMod i^i CMod ) )
9 nmoleub2.f 
 |-  ( ph -> F e. ( S LMHom T ) )
10 nmoleub2.a 
 |-  ( ph -> A e. RR* )
11 nmoleub2.r 
 |-  ( ph -> R e. RR+ )
12 nmoleub2lem.5 
 |-  ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )
13 nmoleub2lem.6 
 |-  ( ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
14 nmoleub2lem.7 
 |-  ( ( ph /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )
15 14 adantlr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )
16 8 elin1d 
 |-  ( ph -> T e. NrmMod )
17 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
18 16 17 syl 
 |-  ( ph -> T e. NrmGrp )
19 18 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> T e. NrmGrp )
20 eqid 
 |-  ( Base ` T ) = ( Base ` T )
21 2 20 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : V --> ( Base ` T ) )
22 9 21 syl 
 |-  ( ph -> F : V --> ( Base ` T ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> F : V --> ( Base ` T ) )
24 simprl 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> x e. V )
25 23 24 ffvelcdmd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( F ` x ) e. ( Base ` T ) )
26 20 4 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` x ) e. ( Base ` T ) ) -> ( M ` ( F ` x ) ) e. RR )
27 19 25 26 syl2anc 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) e. RR )
28 11 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. RR+ )
29 27 28 rerpdivcld 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) e. RR )
30 29 rexrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) e. RR* )
31 7 elin1d 
 |-  ( ph -> S e. NrmMod )
32 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
33 31 32 syl 
 |-  ( ph -> S e. NrmGrp )
34 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
35 9 34 syl 
 |-  ( ph -> F e. ( S GrpHom T ) )
36 1 nmocl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
37 33 18 35 36 syl3anc 
 |-  ( ph -> ( N ` F ) e. RR* )
38 37 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( N ` F ) e. RR* )
39 10 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> A e. RR* )
40 28 rpred 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. RR )
41 rexmul 
 |-  ( ( ( ( M ` ( F ` x ) ) / R ) e. RR /\ R e. RR ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) = ( ( ( M ` ( F ` x ) ) / R ) x. R ) )
42 29 40 41 syl2anc 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) = ( ( ( M ` ( F ` x ) ) / R ) x. R ) )
43 27 recnd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) e. CC )
44 40 recnd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. CC )
45 28 rpne0d 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R =/= 0 )
46 43 44 45 divcan1d 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) x. R ) = ( M ` ( F ` x ) ) )
47 42 46 eqtrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) = ( M ` ( F ` x ) ) )
48 27 rexrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) e. RR* )
49 33 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> S e. NrmGrp )
50 2 3 nmcl 
 |-  ( ( S e. NrmGrp /\ x e. V ) -> ( L ` x ) e. RR )
51 49 24 50 syl2anc 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( L ` x ) e. RR )
52 51 rexrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( L ` x ) e. RR* )
53 38 52 xmulcld 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) *e ( L ` x ) ) e. RR* )
54 28 rpxrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. RR* )
55 38 54 xmulcld 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) *e R ) e. RR* )
56 35 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> F e. ( S GrpHom T ) )
57 1 2 3 4 nmoix 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ x e. V ) -> ( M ` ( F ` x ) ) <_ ( ( N ` F ) *e ( L ` x ) ) )
58 49 19 56 24 57 syl31anc 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) <_ ( ( N ` F ) *e ( L ` x ) ) )
59 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
60 33 18 35 59 syl3anc 
 |-  ( ph -> 0 <_ ( N ` F ) )
61 37 60 jca 
 |-  ( ph -> ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) )
62 61 ad2antrr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) )
63 simprr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( L ` x ) <_ R )
64 xlemul2a 
 |-  ( ( ( ( L ` x ) e. RR* /\ R e. RR* /\ ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) ) /\ ( L ` x ) <_ R ) -> ( ( N ` F ) *e ( L ` x ) ) <_ ( ( N ` F ) *e R ) )
65 52 54 62 63 64 syl31anc 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) *e ( L ` x ) ) <_ ( ( N ` F ) *e R ) )
66 48 53 55 58 65 xrletrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) <_ ( ( N ` F ) *e R ) )
67 47 66 eqbrtrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) <_ ( ( N ` F ) *e R ) )
68 xlemul1 
 |-  ( ( ( ( M ` ( F ` x ) ) / R ) e. RR* /\ ( N ` F ) e. RR* /\ R e. RR+ ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ ( N ` F ) <-> ( ( ( M ` ( F ` x ) ) / R ) *e R ) <_ ( ( N ` F ) *e R ) ) )
69 30 38 28 68 syl3anc 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ ( N ` F ) <-> ( ( ( M ` ( F ` x ) ) / R ) *e R ) <_ ( ( N ` F ) *e R ) ) )
70 67 69 mpbird 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) <_ ( N ` F ) )
71 simplr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( N ` F ) <_ A )
72 30 38 39 70 71 xrletrd 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) <_ A )
73 72 expr 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( ( L ` x ) <_ R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
74 15 73 syld 
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
75 74 ralrimiva 
 |-  ( ( ph /\ ( N ` F ) <_ A ) -> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
76 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
77 33 ad2antrr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> S e. NrmGrp )
78 18 ad2antrr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> T e. NrmGrp )
79 35 ad2antrr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> F e. ( S GrpHom T ) )
80 simpr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> A e. RR )
81 12 adantr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> 0 <_ A )
82 1 2 3 4 76 77 78 79 80 81 13 nmolb2d 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> ( N ` F ) <_ A )
83 37 ad2antrr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) e. RR* )
84 pnfge 
 |-  ( ( N ` F ) e. RR* -> ( N ` F ) <_ +oo )
85 83 84 syl 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) <_ +oo )
86 simpr 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> A = +oo )
87 85 86 breqtrrd 
 |-  ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) <_ A )
88 10 adantr 
 |-  ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> A e. RR* )
89 ge0nemnf 
 |-  ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )
90 88 12 89 syl2anc 
 |-  ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> A =/= -oo )
91 88 90 jca 
 |-  ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( A e. RR* /\ A =/= -oo ) )
92 xrnemnf 
 |-  ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
93 91 92 sylib 
 |-  ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( A e. RR \/ A = +oo ) )
94 82 87 93 mpjaodan 
 |-  ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( N ` F ) <_ A )
95 75 94 impbida 
 |-  ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )