# 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}\mathrm{normOp}{T}$
nmoleub2.v ${⊢}{V}={\mathrm{Base}}_{{S}}$
nmoleub2.l ${⊢}{L}=\mathrm{norm}\left({S}\right)$
nmoleub2.m ${⊢}{M}=\mathrm{norm}\left({T}\right)$
nmoleub2.g ${⊢}{G}=\mathrm{Scalar}\left({S}\right)$
nmoleub2.w ${⊢}{K}={\mathrm{Base}}_{{G}}$
nmoleub2.s ${⊢}{\phi }\to {S}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
nmoleub2.t ${⊢}{\phi }\to {T}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
nmoleub2.f ${⊢}{\phi }\to {F}\in \left({S}\mathrm{LMHom}{T}\right)$
nmoleub2.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
nmoleub2.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
nmoleub2a.5 ${⊢}{\phi }\to ℚ\subseteq {K}$
nmoleub2lem2.6 ${⊢}\left({L}\left({x}\right)\in ℝ\wedge {R}\in ℝ\right)\to \left({L}\left({x}\right){O}{R}\to {L}\left({x}\right)\le {R}\right)$
nmoleub2lem2.7 ${⊢}\left({L}\left({x}\right)\in ℝ\wedge {R}\in ℝ\right)\to \left({L}\left({x}\right)<{R}\to {L}\left({x}\right){O}{R}\right)$
Assertion nmoleub2lem2 ${⊢}{\phi }\to \left({N}\left({F}\right)\le {A}↔\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nmoleub2.n ${⊢}{N}={S}\mathrm{normOp}{T}$
2 nmoleub2.v ${⊢}{V}={\mathrm{Base}}_{{S}}$
3 nmoleub2.l ${⊢}{L}=\mathrm{norm}\left({S}\right)$
4 nmoleub2.m ${⊢}{M}=\mathrm{norm}\left({T}\right)$
5 nmoleub2.g ${⊢}{G}=\mathrm{Scalar}\left({S}\right)$
6 nmoleub2.w ${⊢}{K}={\mathrm{Base}}_{{G}}$
7 nmoleub2.s ${⊢}{\phi }\to {S}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
8 nmoleub2.t ${⊢}{\phi }\to {T}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
9 nmoleub2.f ${⊢}{\phi }\to {F}\in \left({S}\mathrm{LMHom}{T}\right)$
10 nmoleub2.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
11 nmoleub2.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
12 nmoleub2a.5 ${⊢}{\phi }\to ℚ\subseteq {K}$
13 nmoleub2lem2.6 ${⊢}\left({L}\left({x}\right)\in ℝ\wedge {R}\in ℝ\right)\to \left({L}\left({x}\right){O}{R}\to {L}\left({x}\right)\le {R}\right)$
14 nmoleub2lem2.7 ${⊢}\left({L}\left({x}\right)\in ℝ\wedge {R}\in ℝ\right)\to \left({L}\left({x}\right)<{R}\to {L}\left({x}\right){O}{R}\right)$
15 lmghm ${⊢}{F}\in \left({S}\mathrm{LMHom}{T}\right)\to {F}\in \left({S}\mathrm{GrpHom}{T}\right)$
16 eqid ${⊢}{0}_{{S}}={0}_{{S}}$
17 eqid ${⊢}{0}_{{T}}={0}_{{T}}$
18 16 17 ghmid ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {F}\left({0}_{{S}}\right)={0}_{{T}}$
19 9 15 18 3syl ${⊢}{\phi }\to {F}\left({0}_{{S}}\right)={0}_{{T}}$
20 19 fveq2d ${⊢}{\phi }\to {M}\left({F}\left({0}_{{S}}\right)\right)={M}\left({0}_{{T}}\right)$
21 8 elin1d ${⊢}{\phi }\to {T}\in \mathrm{NrmMod}$
22 nlmngp ${⊢}{T}\in \mathrm{NrmMod}\to {T}\in \mathrm{NrmGrp}$
23 4 17 nm0 ${⊢}{T}\in \mathrm{NrmGrp}\to {M}\left({0}_{{T}}\right)=0$
24 21 22 23 3syl ${⊢}{\phi }\to {M}\left({0}_{{T}}\right)=0$
25 20 24 eqtrd ${⊢}{\phi }\to {M}\left({F}\left({0}_{{S}}\right)\right)=0$
26 25 adantr ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {M}\left({F}\left({0}_{{S}}\right)\right)=0$
27 26 oveq1d ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to \frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}=\frac{0}{{R}}$
28 11 adantr ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {R}\in {ℝ}^{+}$
29 28 rpcnd ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {R}\in ℂ$
30 28 rpne0d ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {R}\ne 0$
31 29 30 div0d ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to \frac{0}{{R}}=0$
32 27 31 eqtrd ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to \frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}=0$
33 7 elin1d ${⊢}{\phi }\to {S}\in \mathrm{NrmMod}$
34 nlmngp ${⊢}{S}\in \mathrm{NrmMod}\to {S}\in \mathrm{NrmGrp}$
35 3 16 nm0 ${⊢}{S}\in \mathrm{NrmGrp}\to {L}\left({0}_{{S}}\right)=0$
36 33 34 35 3syl ${⊢}{\phi }\to {L}\left({0}_{{S}}\right)=0$
37 36 adantr ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {L}\left({0}_{{S}}\right)=0$
38 28 rpgt0d ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to 0<{R}$
39 37 38 eqbrtrd ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {L}\left({0}_{{S}}\right)<{R}$
40 fveq2 ${⊢}{x}={0}_{{S}}\to {L}\left({x}\right)={L}\left({0}_{{S}}\right)$
41 40 breq1d ${⊢}{x}={0}_{{S}}\to \left({L}\left({x}\right)<{R}↔{L}\left({0}_{{S}}\right)<{R}\right)$
42 2fveq3 ${⊢}{x}={0}_{{S}}\to {M}\left({F}\left({x}\right)\right)={M}\left({F}\left({0}_{{S}}\right)\right)$
43 42 oveq1d ${⊢}{x}={0}_{{S}}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}=\frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}$
44 43 breq1d ${⊢}{x}={0}_{{S}}\to \left(\frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}↔\frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}\le {A}\right)$
45 41 44 imbi12d ${⊢}{x}={0}_{{S}}\to \left(\left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)↔\left({L}\left({0}_{{S}}\right)<{R}\to \frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}\le {A}\right)\right)$
46 33 34 syl ${⊢}{\phi }\to {S}\in \mathrm{NrmGrp}$
47 2 3 nmcl ${⊢}\left({S}\in \mathrm{NrmGrp}\wedge {x}\in {V}\right)\to {L}\left({x}\right)\in ℝ$
48 46 47 sylan ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to {L}\left({x}\right)\in ℝ$
49 11 adantr ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to {R}\in {ℝ}^{+}$
50 49 rpred ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to {R}\in ℝ$
51 48 50 14 syl2anc ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to \left({L}\left({x}\right)<{R}\to {L}\left({x}\right){O}{R}\right)$
52 51 imim1d ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to \left(\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\to \left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)$
53 52 ralimdva ${⊢}{\phi }\to \left(\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)$
54 53 imp ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)$
55 ngpgrp ${⊢}{S}\in \mathrm{NrmGrp}\to {S}\in \mathrm{Grp}$
56 2 16 grpidcl ${⊢}{S}\in \mathrm{Grp}\to {0}_{{S}}\in {V}$
57 46 55 56 3syl ${⊢}{\phi }\to {0}_{{S}}\in {V}$
58 57 adantr ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to {0}_{{S}}\in {V}$
59 45 54 58 rspcdva ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to \left({L}\left({0}_{{S}}\right)<{R}\to \frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}\le {A}\right)$
60 39 59 mpd ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to \frac{{M}\left({F}\left({0}_{{S}}\right)\right)}{{R}}\le {A}$
61 32 60 eqbrtrrd ${⊢}\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\to 0\le {A}$
62 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {\phi }$
63 62 7 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {S}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
64 62 8 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {T}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
65 62 9 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {F}\in \left({S}\mathrm{LMHom}{T}\right)$
66 62 10 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {A}\in {ℝ}^{*}$
67 62 11 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {R}\in {ℝ}^{+}$
68 62 12 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to ℚ\subseteq {K}$
69 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
70 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {A}\in ℝ$
71 61 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to 0\le {A}$
72 simplrl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {y}\in {V}$
73 simplrr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to {y}\ne {0}_{{S}}$
74 54 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)$
75 fveq2 ${⊢}{x}={z}{\cdot }_{{S}}{y}\to {L}\left({x}\right)={L}\left({z}{\cdot }_{{S}}{y}\right)$
76 75 breq1d ${⊢}{x}={z}{\cdot }_{{S}}{y}\to \left({L}\left({x}\right)<{R}↔{L}\left({z}{\cdot }_{{S}}{y}\right)<{R}\right)$
77 2fveq3 ${⊢}{x}={z}{\cdot }_{{S}}{y}\to {M}\left({F}\left({x}\right)\right)={M}\left({F}\left({z}{\cdot }_{{S}}{y}\right)\right)$
78 77 oveq1d ${⊢}{x}={z}{\cdot }_{{S}}{y}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}=\frac{{M}\left({F}\left({z}{\cdot }_{{S}}{y}\right)\right)}{{R}}$
79 78 breq1d ${⊢}{x}={z}{\cdot }_{{S}}{y}\to \left(\frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}↔\frac{{M}\left({F}\left({z}{\cdot }_{{S}}{y}\right)\right)}{{R}}\le {A}\right)$
80 76 79 imbi12d ${⊢}{x}={z}{\cdot }_{{S}}{y}\to \left(\left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)↔\left({L}\left({z}{\cdot }_{{S}}{y}\right)<{R}\to \frac{{M}\left({F}\left({z}{\cdot }_{{S}}{y}\right)\right)}{{R}}\le {A}\right)\right)$
81 80 rspccv ${⊢}\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)<{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\to \left({z}{\cdot }_{{S}}{y}\in {V}\to \left({L}\left({z}{\cdot }_{{S}}{y}\right)<{R}\to \frac{{M}\left({F}\left({z}{\cdot }_{{S}}{y}\right)\right)}{{R}}\le {A}\right)\right)$
82 74 81 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to \left({z}{\cdot }_{{S}}{y}\in {V}\to \left({L}\left({z}{\cdot }_{{S}}{y}\right)<{R}\to \frac{{M}\left({F}\left({z}{\cdot }_{{S}}{y}\right)\right)}{{R}}\le {A}\right)\right)$
83 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)\to ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)$
84 1 2 3 4 5 6 63 64 65 66 67 68 69 70 71 72 73 82 83 nmoleub2lem3 ${⊢}¬\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)$
85 iman ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\to {M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)↔¬\left(\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\wedge ¬{M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)\right)$
86 84 85 mpbir ${⊢}\left(\left(\left({\phi }\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)\wedge {A}\in ℝ\right)\wedge \left({y}\in {V}\wedge {y}\ne {0}_{{S}}\right)\right)\to {M}\left({F}\left({y}\right)\right)\le {A}{L}\left({y}\right)$
87 48 50 13 syl2anc ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to \left({L}\left({x}\right){O}{R}\to {L}\left({x}\right)\le {R}\right)$
88 1 2 3 4 5 6 7 8 9 10 11 61 86 87 nmoleub2lem ${⊢}{\phi }\to \left({N}\left({F}\right)\le {A}↔\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right){O}{R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)$