Metamath Proof Explorer

Theorem nmoleub2lem2

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+ )
nmoleub2a.5 
|- ( ph -> QQ C_ K )
nmoleub2lem2.6 
|- ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) O R -> ( L ` x ) <_ R ) )
nmoleub2lem2.7 
|- ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) < R -> ( L ` x ) O R ) )
Assertion nmoleub2lem2 
|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) O R -> ( ( 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 nmoleub2a.5 
 |-  ( ph -> QQ C_ K )
13 nmoleub2lem2.6 
 |-  ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) O R -> ( L ` x ) <_ R ) )
14 nmoleub2lem2.7 
 |-  ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) < R -> ( L ` x ) O R ) )
15 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
16 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
17 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
18 16 17 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
19 9 15 18 3syl 
 |-  ( ph -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
20 19 fveq2d 
 |-  ( ph -> ( M ` ( F ` ( 0g ` S ) ) ) = ( M ` ( 0g ` T ) ) )
21 8 elin1d 
 |-  ( ph -> T e. NrmMod )
22 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
23 4 17 nm0 
 |-  ( T e. NrmGrp -> ( M ` ( 0g ` T ) ) = 0 )
24 21 22 23 3syl 
 |-  ( ph -> ( M ` ( 0g ` T ) ) = 0 )
25 20 24 eqtrd 
 |-  ( ph -> ( M ` ( F ` ( 0g ` S ) ) ) = 0 )
26 25 adantr 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( M ` ( F ` ( 0g ` S ) ) ) = 0 )
27 26 oveq1d 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) = ( 0 / R ) )
28 11 adantr 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> R e. RR+ )
29 28 rpcnd 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> R e. CC )
30 28 rpne0d 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> R =/= 0 )
31 29 30 div0d 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( 0 / R ) = 0 )
32 27 31 eqtrd 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) = 0 )
33 7 elin1d 
 |-  ( ph -> S e. NrmMod )
34 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
35 3 16 nm0 
 |-  ( S e. NrmGrp -> ( L ` ( 0g ` S ) ) = 0 )
36 33 34 35 3syl 
 |-  ( ph -> ( L ` ( 0g ` S ) ) = 0 )
37 36 adantr 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( L ` ( 0g ` S ) ) = 0 )
38 28 rpgt0d 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 < R )
39 37 38 eqbrtrd 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( L ` ( 0g ` S ) ) < R )
40 fveq2 
 |-  ( x = ( 0g ` S ) -> ( L ` x ) = ( L ` ( 0g ` S ) ) )
41 40 breq1d 
 |-  ( x = ( 0g ` S ) -> ( ( L ` x ) < R <-> ( L ` ( 0g ` S ) ) < R ) )
42 2fveq3 
 |-  ( x = ( 0g ` S ) -> ( M ` ( F ` x ) ) = ( M ` ( F ` ( 0g ` S ) ) ) )
43 42 oveq1d 
 |-  ( x = ( 0g ` S ) -> ( ( M ` ( F ` x ) ) / R ) = ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) )
44 43 breq1d 
 |-  ( x = ( 0g ` S ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ A <-> ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) <_ A ) )
45 41 44 imbi12d 
 |-  ( x = ( 0g ` S ) -> ( ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) <-> ( ( L ` ( 0g ` S ) ) < R -> ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) <_ A ) ) )
46 33 34 syl 
 |-  ( ph -> S e. NrmGrp )
47 2 3 nmcl 
 |-  ( ( S e. NrmGrp /\ x e. V ) -> ( L ` x ) e. RR )
48 46 47 sylan 
 |-  ( ( ph /\ x e. V ) -> ( L ` x ) e. RR )
49 11 adantr 
 |-  ( ( ph /\ x e. V ) -> R e. RR+ )
50 49 rpred 
 |-  ( ( ph /\ x e. V ) -> R e. RR )
51 48 50 14 syl2anc 
 |-  ( ( ph /\ x e. V ) -> ( ( L ` x ) < R -> ( L ` x ) O R ) )
52 51 imim1d 
 |-  ( ( ph /\ x e. V ) -> ( ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) -> ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
53 52 ralimdva 
 |-  ( ph -> ( A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) -> A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
54 53 imp 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
55 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
56 2 16 grpidcl 
 |-  ( S e. Grp -> ( 0g ` S ) e. V )
57 46 55 56 3syl 
 |-  ( ph -> ( 0g ` S ) e. V )
58 57 adantr 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( 0g ` S ) e. V )
59 45 54 58 rspcdva 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( ( L ` ( 0g ` S ) ) < R -> ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) <_ A ) )
60 39 59 mpd 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( ( M ` ( F ` ( 0g ` S ) ) ) / R ) <_ A )
61 32 60 eqbrtrrd 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )
62 simp-4l 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> ph )
63 62 7 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> S e. ( NrmMod i^i CMod ) )
64 62 8 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> T e. ( NrmMod i^i CMod ) )
65 62 9 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> F e. ( S LMHom T ) )
66 62 10 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> A e. RR* )
67 62 11 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> R e. RR+ )
68 62 12 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> QQ C_ K )
69 eqid 
 |-  ( .s ` S ) = ( .s ` S )
70 simpllr 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> A e. RR )
71 61 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> 0 <_ A )
72 simplrl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> y e. V )
73 simplrr 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> y =/= ( 0g ` S ) )
74 54 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
75 fveq2 
 |-  ( x = ( z ( .s ` S ) y ) -> ( L ` x ) = ( L ` ( z ( .s ` S ) y ) ) )
76 75 breq1d 
 |-  ( x = ( z ( .s ` S ) y ) -> ( ( L ` x ) < R <-> ( L ` ( z ( .s ` S ) y ) ) < R ) )
77 2fveq3 
 |-  ( x = ( z ( .s ` S ) y ) -> ( M ` ( F ` x ) ) = ( M ` ( F ` ( z ( .s ` S ) y ) ) ) )
78 77 oveq1d 
 |-  ( x = ( z ( .s ` S ) y ) -> ( ( M ` ( F ` x ) ) / R ) = ( ( M ` ( F ` ( z ( .s ` S ) y ) ) ) / R ) )
79 78 breq1d 
 |-  ( x = ( z ( .s ` S ) y ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ A <-> ( ( M ` ( F ` ( z ( .s ` S ) y ) ) ) / R ) <_ A ) )
80 76 79 imbi12d 
 |-  ( x = ( z ( .s ` S ) y ) -> ( ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) <-> ( ( L ` ( z ( .s ` S ) y ) ) < R -> ( ( M ` ( F ` ( z ( .s ` S ) y ) ) ) / R ) <_ A ) ) )
81 80 rspccv 
 |-  ( A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) -> ( ( z ( .s ` S ) y ) e. V -> ( ( L ` ( z ( .s ` S ) y ) ) < R -> ( ( M ` ( F ` ( z ( .s ` S ) y ) ) ) / R ) <_ A ) ) )
82 74 81 syl 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> ( ( z ( .s ` S ) y ) e. V -> ( ( L ` ( z ( .s ` S ) y ) ) < R -> ( ( M ` ( F ` ( z ( .s ` S ) y ) ) ) / R ) <_ A ) ) )
83 simpr 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) -> -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
84 1 2 3 4 5 6 63 64 65 66 67 68 69 70 71 72 73 82 83 nmoleub2lem3 
 |-  -. ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
85 iman 
 |-  ( ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) <-> -. ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) /\ -. ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) )
86 84 85 mpbir 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
87 48 50 13 syl2anc 
 |-  ( ( ph /\ x e. V ) -> ( ( L ` x ) O R -> ( L ` x ) <_ R ) )
88 1 2 3 4 5 6 7 8 9 10 11 61 86 87 nmoleub2lem 
 |-  ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )