Metamath Proof Explorer

Theorem nmoleub3

Description: The operator norm is the supremum of the value of a linear operator on the unit sphere. (Contributed by Mario Carneiro, 19-Oct-2015) (Proof shortened by AV, 29-Sep-2021)

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+ )
nmoleub3.5 
|- ( ph -> 0 <_ A )
nmoleub3.6 
|- ( ph -> RR C_ K )
Assertion nmoleub3 
|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) = 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 nmoleub3.5 
 |-  ( ph -> 0 <_ A )
13 nmoleub3.6 
 |-  ( ph -> RR C_ K )
14 12 adantr 
 |-  ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )
15 9 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> F e. ( S LMHom T ) )
16 13 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> RR C_ K )
17 11 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> R e. RR+ )
18 7 elin1d 
 |-  ( ph -> S e. NrmMod )
19 18 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> S e. NrmMod )
20 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
21 19 20 syl 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> S e. NrmGrp )
22 simprl 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> y e. V )
23 simprr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> y =/= ( 0g ` S ) )
24 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
25 2 3 24 nmrpcl 
 |-  ( ( S e. NrmGrp /\ y e. V /\ y =/= ( 0g ` S ) ) -> ( L ` y ) e. RR+ )
26 21 22 23 25 syl3anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( L ` y ) e. RR+ )
27 17 26 rpdivcld 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( R / ( L ` y ) ) e. RR+ )
28 27 rpred 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( R / ( L ` y ) ) e. RR )
29 16 28 sseldd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( R / ( L ` y ) ) e. K )
30 eqid 
 |-  ( .s ` S ) = ( .s ` S )
31 eqid 
 |-  ( .s ` T ) = ( .s ` T )
32 5 6 2 30 31 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ ( R / ( L ` y ) ) e. K /\ y e. V ) -> ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = ( ( R / ( L ` y ) ) ( .s ` T ) ( F ` y ) ) )
33 15 29 22 32 syl3anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = ( ( R / ( L ` y ) ) ( .s ` T ) ( F ` y ) ) )
34 33 fveq2d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) = ( M ` ( ( R / ( L ` y ) ) ( .s ` T ) ( F ` y ) ) ) )
35 8 elin1d 
 |-  ( ph -> T e. NrmMod )
36 35 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> T e. NrmMod )
37 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
38 5 37 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = G )
39 15 38 syl 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( Scalar ` T ) = G )
40 39 fveq2d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( Base ` ( Scalar ` T ) ) = ( Base ` G ) )
41 40 6 eqtr4di 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( Base ` ( Scalar ` T ) ) = K )
42 29 41 eleqtrrd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( R / ( L ` y ) ) e. ( Base ` ( Scalar ` T ) ) )
43 eqid 
 |-  ( Base ` T ) = ( Base ` T )
44 2 43 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : V --> ( Base ` T ) )
45 15 44 syl 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> F : V --> ( Base ` T ) )
46 45 22 ffvelrnd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( F ` y ) e. ( Base ` T ) )
47 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
48 eqid 
 |-  ( norm ` ( Scalar ` T ) ) = ( norm ` ( Scalar ` T ) )
49 43 4 31 37 47 48 nmvs 
 |-  ( ( T e. NrmMod /\ ( R / ( L ` y ) ) e. ( Base ` ( Scalar ` T ) ) /\ ( F ` y ) e. ( Base ` T ) ) -> ( M ` ( ( R / ( L ` y ) ) ( .s ` T ) ( F ` y ) ) ) = ( ( ( norm ` ( Scalar ` T ) ) ` ( R / ( L ` y ) ) ) x. ( M ` ( F ` y ) ) ) )
50 36 42 46 49 syl3anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( ( R / ( L ` y ) ) ( .s ` T ) ( F ` y ) ) ) = ( ( ( norm ` ( Scalar ` T ) ) ` ( R / ( L ` y ) ) ) x. ( M ` ( F ` y ) ) ) )
51 39 fveq2d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( norm ` ( Scalar ` T ) ) = ( norm ` G ) )
52 51 fveq1d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( norm ` ( Scalar ` T ) ) ` ( R / ( L ` y ) ) ) = ( ( norm ` G ) ` ( R / ( L ` y ) ) ) )
53 7 elin2d 
 |-  ( ph -> S e. CMod )
54 53 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> S e. CMod )
55 5 6 clmabs 
 |-  ( ( S e. CMod /\ ( R / ( L ` y ) ) e. K ) -> ( abs ` ( R / ( L ` y ) ) ) = ( ( norm ` G ) ` ( R / ( L ` y ) ) ) )
56 54 29 55 syl2anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( abs ` ( R / ( L ` y ) ) ) = ( ( norm ` G ) ` ( R / ( L ` y ) ) ) )
57 27 rpge0d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> 0 <_ ( R / ( L ` y ) ) )
58 28 57 absidd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( abs ` ( R / ( L ` y ) ) ) = ( R / ( L ` y ) ) )
59 56 58 eqtr3d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( norm ` G ) ` ( R / ( L ` y ) ) ) = ( R / ( L ` y ) ) )
60 52 59 eqtrd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( norm ` ( Scalar ` T ) ) ` ( R / ( L ` y ) ) ) = ( R / ( L ` y ) ) )
61 60 oveq1d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( ( norm ` ( Scalar ` T ) ) ` ( R / ( L ` y ) ) ) x. ( M ` ( F ` y ) ) ) = ( ( R / ( L ` y ) ) x. ( M ` ( F ` y ) ) ) )
62 34 50 61 3eqtrd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) = ( ( R / ( L ` y ) ) x. ( M ` ( F ` y ) ) ) )
63 62 oveq1d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) = ( ( ( R / ( L ` y ) ) x. ( M ` ( F ` y ) ) ) / R ) )
64 27 rpcnd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( R / ( L ` y ) ) e. CC )
65 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
66 36 65 syl 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> T e. NrmGrp )
67 43 4 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` y ) e. ( Base ` T ) ) -> ( M ` ( F ` y ) ) e. RR )
68 66 46 67 syl2anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) e. RR )
69 68 recnd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) e. CC )
70 17 rpcnd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> R e. CC )
71 17 rpne0d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> R =/= 0 )
72 64 69 70 71 divassd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( ( R / ( L ` y ) ) x. ( M ` ( F ` y ) ) ) / R ) = ( ( R / ( L ` y ) ) x. ( ( M ` ( F ` y ) ) / R ) ) )
73 26 rpcnd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( L ` y ) e. CC )
74 26 rpne0d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( L ` y ) =/= 0 )
75 69 70 73 71 74 dmdcand 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( R / ( L ` y ) ) x. ( ( M ` ( F ` y ) ) / R ) ) = ( ( M ` ( F ` y ) ) / ( L ` y ) ) )
76 63 72 75 3eqtrd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) = ( ( M ` ( F ` y ) ) / ( L ` y ) ) )
77 eqid 
 |-  ( norm ` G ) = ( norm ` G )
78 2 3 30 5 6 77 nmvs 
 |-  ( ( S e. NrmMod /\ ( R / ( L ` y ) ) e. K /\ y e. V ) -> ( L ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = ( ( ( norm ` G ) ` ( R / ( L ` y ) ) ) x. ( L ` y ) ) )
79 19 29 22 78 syl3anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( L ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = ( ( ( norm ` G ) ` ( R / ( L ` y ) ) ) x. ( L ` y ) ) )
80 59 oveq1d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( ( norm ` G ) ` ( R / ( L ` y ) ) ) x. ( L ` y ) ) = ( ( R / ( L ` y ) ) x. ( L ` y ) ) )
81 70 73 74 divcan1d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( R / ( L ` y ) ) x. ( L ` y ) ) = R )
82 79 80 81 3eqtrd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( L ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = R )
83 fveqeq2 
 |-  ( x = ( ( R / ( L ` y ) ) ( .s ` S ) y ) -> ( ( L ` x ) = R <-> ( L ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = R ) )
84 2fveq3 
 |-  ( x = ( ( R / ( L ` y ) ) ( .s ` S ) y ) -> ( M ` ( F ` x ) ) = ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) )
85 84 oveq1d 
 |-  ( x = ( ( R / ( L ` y ) ) ( .s ` S ) y ) -> ( ( M ` ( F ` x ) ) / R ) = ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) )
86 85 breq1d 
 |-  ( x = ( ( R / ( L ` y ) ) ( .s ` S ) y ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ A <-> ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) <_ A ) )
87 83 86 imbi12d 
 |-  ( x = ( ( R / ( L ` y ) ) ( .s ` S ) y ) -> ( ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) <-> ( ( L ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = R -> ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) <_ A ) ) )
88 simpllr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
89 2 5 30 6 clmvscl 
 |-  ( ( S e. CMod /\ ( R / ( L ` y ) ) e. K /\ y e. V ) -> ( ( R / ( L ` y ) ) ( .s ` S ) y ) e. V )
90 54 29 22 89 syl3anc 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( R / ( L ` y ) ) ( .s ` S ) y ) e. V )
91 87 88 90 rspcdva 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( L ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) = R -> ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) <_ A ) )
92 82 91 mpd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( M ` ( F ` ( ( R / ( L ` y ) ) ( .s ` S ) y ) ) ) / R ) <_ A )
93 76 92 eqbrtrrd 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( M ` ( F ` y ) ) / ( L ` y ) ) <_ A )
94 simplr 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> A e. RR )
95 68 94 26 ledivmul2d 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( ( ( M ` ( F ` y ) ) / ( L ` y ) ) <_ A <-> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) ) )
96 93 95 mpbid 
 |-  ( ( ( ( ph /\ A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
97 11 adantr 
 |-  ( ( ph /\ x e. V ) -> R e. RR+ )
98 97 rpred 
 |-  ( ( ph /\ x e. V ) -> R e. RR )
99 98 leidd 
 |-  ( ( ph /\ x e. V ) -> R <_ R )
100 breq1 
 |-  ( ( L ` x ) = R -> ( ( L ` x ) <_ R <-> R <_ R ) )
101 99 100 syl5ibrcom 
 |-  ( ( ph /\ x e. V ) -> ( ( L ` x ) = R -> ( L ` x ) <_ R ) )
102 1 2 3 4 5 6 7 8 9 10 11 14 96 101 nmoleub2lem 
 |-  ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )