MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nmoleub2lem3 Structured version   Visualization version   GIF version

Theorem nmoleub2lem3 23402
Description: Lemma for nmoleub2a 23404 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.)
Hypotheses
Ref Expression
nmoleub2.n 𝑁 = (𝑆 normOp 𝑇)
nmoleub2.v 𝑉 = (Base‘𝑆)
nmoleub2.l 𝐿 = (norm‘𝑆)
nmoleub2.m 𝑀 = (norm‘𝑇)
nmoleub2.g 𝐺 = (Scalar‘𝑆)
nmoleub2.w 𝐾 = (Base‘𝐺)
nmoleub2.s (𝜑𝑆 ∈ (NrmMod ∩ ℂMod))
nmoleub2.t (𝜑𝑇 ∈ (NrmMod ∩ ℂMod))
nmoleub2.f (𝜑𝐹 ∈ (𝑆 LMHom 𝑇))
nmoleub2.a (𝜑𝐴 ∈ ℝ*)
nmoleub2.r (𝜑𝑅 ∈ ℝ+)
nmoleub2a.5 (𝜑 → ℚ ⊆ 𝐾)
nmoleub2lem3.p · = ( ·𝑠𝑆)
nmoleub2lem3.1 (𝜑𝐴 ∈ ℝ)
nmoleub2lem3.2 (𝜑 → 0 ≤ 𝐴)
nmoleub2lem3.3 (𝜑𝐵𝑉)
nmoleub2lem3.4 (𝜑𝐵 ≠ (0g𝑆))
nmoleub2lem3.5 (𝜑 → ((𝑟 · 𝐵) ∈ 𝑉 → ((𝐿‘(𝑟 · 𝐵)) < 𝑅 → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴)))
nmoleub2lem3.6 (𝜑 → ¬ (𝑀‘(𝐹𝐵)) ≤ (𝐴 · (𝐿𝐵)))
Assertion
Ref Expression
nmoleub2lem3 ¬ 𝜑
Distinct variable groups:   𝐴,𝑟   𝐹,𝑟   𝐿,𝑟   𝑀,𝑟   𝜑,𝑟   𝐵,𝑟   𝑅,𝑟
Allowed substitution hints:   𝑆(𝑟)   𝑇(𝑟)   · (𝑟)   𝐺(𝑟)   𝐾(𝑟)   𝑁(𝑟)   𝑉(𝑟)

Proof of Theorem nmoleub2lem3
StepHypRef Expression
1 simprl 767 . . . 4 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟)
2 qre 12202 . . . . . 6 (𝑟 ∈ ℚ → 𝑟 ∈ ℝ)
32ad2antlr 723 . . . . 5 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑟 ∈ ℝ)
4 nmoleub2lem3.1 . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
5 nmoleub2.r . . . . . . . . 9 (𝜑𝑅 ∈ ℝ+)
65rpred 12281 . . . . . . . 8 (𝜑𝑅 ∈ ℝ)
74, 6remulcld 10520 . . . . . . 7 (𝜑 → (𝐴 · 𝑅) ∈ ℝ)
8 nmoleub2.t . . . . . . . . . . 11 (𝜑𝑇 ∈ (NrmMod ∩ ℂMod))
98elin1d 4098 . . . . . . . . . 10 (𝜑𝑇 ∈ NrmMod)
10 nlmngp 22969 . . . . . . . . . 10 (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp)
119, 10syl 17 . . . . . . . . 9 (𝜑𝑇 ∈ NrmGrp)
12 nmoleub2.f . . . . . . . . . . 11 (𝜑𝐹 ∈ (𝑆 LMHom 𝑇))
13 nmoleub2.v . . . . . . . . . . . 12 𝑉 = (Base‘𝑆)
14 eqid 2794 . . . . . . . . . . . 12 (Base‘𝑇) = (Base‘𝑇)
1513, 14lmhmf 19496 . . . . . . . . . . 11 (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇))
1612, 15syl 17 . . . . . . . . . 10 (𝜑𝐹:𝑉⟶(Base‘𝑇))
17 nmoleub2lem3.3 . . . . . . . . . 10 (𝜑𝐵𝑉)
1816, 17ffvelrnd 6720 . . . . . . . . 9 (𝜑 → (𝐹𝐵) ∈ (Base‘𝑇))
19 nmoleub2.m . . . . . . . . . 10 𝑀 = (norm‘𝑇)
2014, 19nmcl 22908 . . . . . . . . 9 ((𝑇 ∈ NrmGrp ∧ (𝐹𝐵) ∈ (Base‘𝑇)) → (𝑀‘(𝐹𝐵)) ∈ ℝ)
2111, 18, 20syl2anc 584 . . . . . . . 8 (𝜑 → (𝑀‘(𝐹𝐵)) ∈ ℝ)
22 0red 10493 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
23 nmoleub2.s . . . . . . . . . . . . 13 (𝜑𝑆 ∈ (NrmMod ∩ ℂMod))
2423elin1d 4098 . . . . . . . . . . . 12 (𝜑𝑆 ∈ NrmMod)
25 nlmngp 22969 . . . . . . . . . . . 12 (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp)
2624, 25syl 17 . . . . . . . . . . 11 (𝜑𝑆 ∈ NrmGrp)
27 nmoleub2.l . . . . . . . . . . . 12 𝐿 = (norm‘𝑆)
2813, 27nmcl 22908 . . . . . . . . . . 11 ((𝑆 ∈ NrmGrp ∧ 𝐵𝑉) → (𝐿𝐵) ∈ ℝ)
2926, 17, 28syl2anc 584 . . . . . . . . . 10 (𝜑 → (𝐿𝐵) ∈ ℝ)
304, 29remulcld 10520 . . . . . . . . 9 (𝜑 → (𝐴 · (𝐿𝐵)) ∈ ℝ)
31 nmoleub2lem3.2 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐴)
3213, 27nmge0 22909 . . . . . . . . . . 11 ((𝑆 ∈ NrmGrp ∧ 𝐵𝑉) → 0 ≤ (𝐿𝐵))
3326, 17, 32syl2anc 584 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝐿𝐵))
344, 29, 31, 33mulge0d 11067 . . . . . . . . 9 (𝜑 → 0 ≤ (𝐴 · (𝐿𝐵)))
35 nmoleub2lem3.6 . . . . . . . . . 10 (𝜑 → ¬ (𝑀‘(𝐹𝐵)) ≤ (𝐴 · (𝐿𝐵)))
3630, 21ltnled 10636 . . . . . . . . . 10 (𝜑 → ((𝐴 · (𝐿𝐵)) < (𝑀‘(𝐹𝐵)) ↔ ¬ (𝑀‘(𝐹𝐵)) ≤ (𝐴 · (𝐿𝐵))))
3735, 36mpbird 258 . . . . . . . . 9 (𝜑 → (𝐴 · (𝐿𝐵)) < (𝑀‘(𝐹𝐵)))
3822, 30, 21, 34, 37lelttrd 10647 . . . . . . . 8 (𝜑 → 0 < (𝑀‘(𝐹𝐵)))
3921, 38elrpd 12278 . . . . . . 7 (𝜑 → (𝑀‘(𝐹𝐵)) ∈ ℝ+)
407, 39rerpdivcld 12312 . . . . . 6 (𝜑 → ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) ∈ ℝ)
4140ad2antrr 722 . . . . 5 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) ∈ ℝ)
4212ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝐹 ∈ (𝑆 LMHom 𝑇))
43 nmoleub2a.5 . . . . . . . . . . . . . 14 (𝜑 → ℚ ⊆ 𝐾)
4443sselda 3891 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ ℚ) → 𝑟𝐾)
4544adantr 481 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑟𝐾)
4617ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝐵𝑉)
47 nmoleub2.g . . . . . . . . . . . . 13 𝐺 = (Scalar‘𝑆)
48 nmoleub2.w . . . . . . . . . . . . 13 𝐾 = (Base‘𝐺)
49 nmoleub2lem3.p . . . . . . . . . . . . 13 · = ( ·𝑠𝑆)
50 eqid 2794 . . . . . . . . . . . . 13 ( ·𝑠𝑇) = ( ·𝑠𝑇)
5147, 48, 13, 49, 50lmhmlin 19497 . . . . . . . . . . . 12 ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑟𝐾𝐵𝑉) → (𝐹‘(𝑟 · 𝐵)) = (𝑟( ·𝑠𝑇)(𝐹𝐵)))
5242, 45, 46, 51syl3anc 1364 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝐹‘(𝑟 · 𝐵)) = (𝑟( ·𝑠𝑇)(𝐹𝐵)))
5352fveq2d 6545 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑀‘(𝐹‘(𝑟 · 𝐵))) = (𝑀‘(𝑟( ·𝑠𝑇)(𝐹𝐵))))
549ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑇 ∈ NrmMod)
55 eqid 2794 . . . . . . . . . . . . . . . 16 (Scalar‘𝑇) = (Scalar‘𝑇)
5647, 55lmhmsca 19492 . . . . . . . . . . . . . . 15 (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = 𝐺)
5742, 56syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (Scalar‘𝑇) = 𝐺)
5857fveq2d 6545 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (Base‘(Scalar‘𝑇)) = (Base‘𝐺))
5958, 48syl6eqr 2848 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (Base‘(Scalar‘𝑇)) = 𝐾)
6045, 59eleqtrrd 2885 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑟 ∈ (Base‘(Scalar‘𝑇)))
6118ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝐹𝐵) ∈ (Base‘𝑇))
62 eqid 2794 . . . . . . . . . . . 12 (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇))
63 eqid 2794 . . . . . . . . . . . 12 (norm‘(Scalar‘𝑇)) = (norm‘(Scalar‘𝑇))
6414, 19, 50, 55, 62, 63nmvs 22968 . . . . . . . . . . 11 ((𝑇 ∈ NrmMod ∧ 𝑟 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐹𝐵) ∈ (Base‘𝑇)) → (𝑀‘(𝑟( ·𝑠𝑇)(𝐹𝐵))) = (((norm‘(Scalar‘𝑇))‘𝑟) · (𝑀‘(𝐹𝐵))))
6554, 60, 61, 64syl3anc 1364 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑀‘(𝑟( ·𝑠𝑇)(𝐹𝐵))) = (((norm‘(Scalar‘𝑇))‘𝑟) · (𝑀‘(𝐹𝐵))))
6657fveq2d 6545 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (norm‘(Scalar‘𝑇)) = (norm‘𝐺))
6766fveq1d 6543 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((norm‘(Scalar‘𝑇))‘𝑟) = ((norm‘𝐺)‘𝑟))
6823elin2d 4099 . . . . . . . . . . . . . . 15 (𝜑𝑆 ∈ ℂMod)
6968ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑆 ∈ ℂMod)
7047, 48clmabs 23370 . . . . . . . . . . . . . 14 ((𝑆 ∈ ℂMod ∧ 𝑟𝐾) → (abs‘𝑟) = ((norm‘𝐺)‘𝑟))
7169, 45, 70syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (abs‘𝑟) = ((norm‘𝐺)‘𝑟))
72 0red 10493 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 0 ∈ ℝ)
735rpge0d 12285 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑅)
744, 6, 31, 73mulge0d 11067 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (𝐴 · 𝑅))
75 divge0 11359 . . . . . . . . . . . . . . . . . 18 ((((𝐴 · 𝑅) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝑅)) ∧ ((𝑀‘(𝐹𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹𝐵)))) → 0 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))))
767, 74, 21, 38, 75syl22anc 835 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))))
7776ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 0 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))))
7872, 41, 3, 77, 1lelttrd 10647 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 0 < 𝑟)
7972, 3, 78ltled 10637 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 0 ≤ 𝑟)
803, 79absidd 14616 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (abs‘𝑟) = 𝑟)
8171, 80eqtr3d 2832 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((norm‘𝐺)‘𝑟) = 𝑟)
8267, 81eqtrd 2830 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((norm‘(Scalar‘𝑇))‘𝑟) = 𝑟)
8382oveq1d 7034 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (((norm‘(Scalar‘𝑇))‘𝑟) · (𝑀‘(𝐹𝐵))) = (𝑟 · (𝑀‘(𝐹𝐵))))
8453, 65, 833eqtrd 2834 . . . . . . . . 9 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑀‘(𝐹‘(𝑟 · 𝐵))) = (𝑟 · (𝑀‘(𝐹𝐵))))
8584oveq1d 7034 . . . . . . . 8 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) = ((𝑟 · (𝑀‘(𝐹𝐵))) / 𝑅))
8613, 47, 49, 48clmvscl 23375 . . . . . . . . . 10 ((𝑆 ∈ ℂMod ∧ 𝑟𝐾𝐵𝑉) → (𝑟 · 𝐵) ∈ 𝑉)
8769, 45, 46, 86syl3anc 1364 . . . . . . . . 9 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑟 · 𝐵) ∈ 𝑉)
8824ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑆 ∈ NrmMod)
89 eqid 2794 . . . . . . . . . . . . 13 (norm‘𝐺) = (norm‘𝐺)
9013, 27, 49, 47, 48, 89nmvs 22968 . . . . . . . . . . . 12 ((𝑆 ∈ NrmMod ∧ 𝑟𝐾𝐵𝑉) → (𝐿‘(𝑟 · 𝐵)) = (((norm‘𝐺)‘𝑟) · (𝐿𝐵)))
9188, 45, 46, 90syl3anc 1364 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝐿‘(𝑟 · 𝐵)) = (((norm‘𝐺)‘𝑟) · (𝐿𝐵)))
9281oveq1d 7034 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (((norm‘𝐺)‘𝑟) · (𝐿𝐵)) = (𝑟 · (𝐿𝐵)))
9391, 92eqtrd 2830 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝐿‘(𝑟 · 𝐵)) = (𝑟 · (𝐿𝐵)))
94 simprr 769 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑟 < (𝑅 / (𝐿𝐵)))
956ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑅 ∈ ℝ)
96 nmoleub2lem3.4 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≠ (0g𝑆))
97 eqid 2794 . . . . . . . . . . . . . . . 16 (0g𝑆) = (0g𝑆)
9813, 27, 97nmrpcl 22912 . . . . . . . . . . . . . . 15 ((𝑆 ∈ NrmGrp ∧ 𝐵𝑉𝐵 ≠ (0g𝑆)) → (𝐿𝐵) ∈ ℝ+)
9926, 17, 96, 98syl3anc 1364 . . . . . . . . . . . . . 14 (𝜑 → (𝐿𝐵) ∈ ℝ+)
10099rpregt0d 12287 . . . . . . . . . . . . 13 (𝜑 → ((𝐿𝐵) ∈ ℝ ∧ 0 < (𝐿𝐵)))
101100ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝐿𝐵) ∈ ℝ ∧ 0 < (𝐿𝐵)))
102 ltmuldiv 11363 . . . . . . . . . . . 12 ((𝑟 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((𝐿𝐵) ∈ ℝ ∧ 0 < (𝐿𝐵))) → ((𝑟 · (𝐿𝐵)) < 𝑅𝑟 < (𝑅 / (𝐿𝐵))))
1033, 95, 101, 102syl3anc 1364 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑟 · (𝐿𝐵)) < 𝑅𝑟 < (𝑅 / (𝐿𝐵))))
10494, 103mpbird 258 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑟 · (𝐿𝐵)) < 𝑅)
10593, 104eqbrtrd 4986 . . . . . . . . 9 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝐿‘(𝑟 · 𝐵)) < 𝑅)
106 nmoleub2lem3.5 . . . . . . . . . 10 (𝜑 → ((𝑟 · 𝐵) ∈ 𝑉 → ((𝐿‘(𝑟 · 𝐵)) < 𝑅 → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴)))
107106ad2antrr 722 . . . . . . . . 9 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑟 · 𝐵) ∈ 𝑉 → ((𝐿‘(𝑟 · 𝐵)) < 𝑅 → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴)))
10887, 105, 107mp2d 49 . . . . . . . 8 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴)
10985, 108eqbrtrrd 4988 . . . . . . 7 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑟 · (𝑀‘(𝐹𝐵))) / 𝑅) ≤ 𝐴)
11021ad2antrr 722 . . . . . . . . 9 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑀‘(𝐹𝐵)) ∈ ℝ)
1113, 110remulcld 10520 . . . . . . . 8 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑟 · (𝑀‘(𝐹𝐵))) ∈ ℝ)
1124ad2antrr 722 . . . . . . . 8 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝐴 ∈ ℝ)
1135ad2antrr 722 . . . . . . . 8 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑅 ∈ ℝ+)
114111, 112, 113ledivmul2d 12335 . . . . . . 7 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (((𝑟 · (𝑀‘(𝐹𝐵))) / 𝑅) ≤ 𝐴 ↔ (𝑟 · (𝑀‘(𝐹𝐵))) ≤ (𝐴 · 𝑅)))
115109, 114mpbid 233 . . . . . 6 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑟 · (𝑀‘(𝐹𝐵))) ≤ (𝐴 · 𝑅))
116112, 95remulcld 10520 . . . . . . 7 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝐴 · 𝑅) ∈ ℝ)
11721, 38jca 512 . . . . . . . 8 (𝜑 → ((𝑀‘(𝐹𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹𝐵))))
118117ad2antrr 722 . . . . . . 7 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑀‘(𝐹𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹𝐵))))
119 lemuldiv 11370 . . . . . . 7 ((𝑟 ∈ ℝ ∧ (𝐴 · 𝑅) ∈ ℝ ∧ ((𝑀‘(𝐹𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹𝐵)))) → ((𝑟 · (𝑀‘(𝐹𝐵))) ≤ (𝐴 · 𝑅) ↔ 𝑟 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵)))))
1203, 116, 118, 119syl3anc 1364 . . . . . 6 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ((𝑟 · (𝑀‘(𝐹𝐵))) ≤ (𝐴 · 𝑅) ↔ 𝑟 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵)))))
121115, 120mpbid 233 . . . . 5 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → 𝑟 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))))
1223, 41, 121lensymd 10640 . . . 4 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → ¬ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟)
1231, 122pm2.21dd 196 . . 3 (((𝜑𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵)))) → (𝑀‘(𝐹𝐵)) ≤ (𝐴 · (𝐿𝐵)))
1246, 99rerpdivcld 12312 . . . 4 (𝜑 → (𝑅 / (𝐿𝐵)) ∈ ℝ)
1254recnd 10518 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
1266recnd 10518 . . . . . . 7 (𝜑𝑅 ∈ ℂ)
12729recnd 10518 . . . . . . 7 (𝜑 → (𝐿𝐵) ∈ ℂ)
128 mulass 10474 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (𝐿𝐵) ∈ ℂ) → ((𝐴 · 𝑅) · (𝐿𝐵)) = (𝐴 · (𝑅 · (𝐿𝐵))))
129 mul12 10654 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (𝐿𝐵) ∈ ℂ) → (𝐴 · (𝑅 · (𝐿𝐵))) = (𝑅 · (𝐴 · (𝐿𝐵))))
130128, 129eqtrd 2830 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (𝐿𝐵) ∈ ℂ) → ((𝐴 · 𝑅) · (𝐿𝐵)) = (𝑅 · (𝐴 · (𝐿𝐵))))
131125, 126, 127, 130syl3anc 1364 . . . . . 6 (𝜑 → ((𝐴 · 𝑅) · (𝐿𝐵)) = (𝑅 · (𝐴 · (𝐿𝐵))))
13230, 21, 5, 37ltmul2dd 12337 . . . . . 6 (𝜑 → (𝑅 · (𝐴 · (𝐿𝐵))) < (𝑅 · (𝑀‘(𝐹𝐵))))
133131, 132eqbrtrd 4986 . . . . 5 (𝜑 → ((𝐴 · 𝑅) · (𝐿𝐵)) < (𝑅 · (𝑀‘(𝐹𝐵))))
134 lt2mul2div 11368 . . . . . 6 ((((𝐴 · 𝑅) ∈ ℝ ∧ ((𝐿𝐵) ∈ ℝ ∧ 0 < (𝐿𝐵))) ∧ (𝑅 ∈ ℝ ∧ ((𝑀‘(𝐹𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹𝐵))))) → (((𝐴 · 𝑅) · (𝐿𝐵)) < (𝑅 · (𝑀‘(𝐹𝐵))) ↔ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < (𝑅 / (𝐿𝐵))))
1357, 100, 6, 117, 134syl22anc 835 . . . . 5 (𝜑 → (((𝐴 · 𝑅) · (𝐿𝐵)) < (𝑅 · (𝑀‘(𝐹𝐵))) ↔ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < (𝑅 / (𝐿𝐵))))
136133, 135mpbid 233 . . . 4 (𝜑 → ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < (𝑅 / (𝐿𝐵)))
137 qbtwnre 12442 . . . 4 ((((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) ∈ ℝ ∧ (𝑅 / (𝐿𝐵)) ∈ ℝ ∧ ((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < (𝑅 / (𝐿𝐵))) → ∃𝑟 ∈ ℚ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵))))
13840, 124, 136, 137syl3anc 1364 . . 3 (𝜑 → ∃𝑟 ∈ ℚ (((𝐴 · 𝑅) / (𝑀‘(𝐹𝐵))) < 𝑟𝑟 < (𝑅 / (𝐿𝐵))))
139123, 138r19.29a 3251 . 2 (𝜑 → (𝑀‘(𝐹𝐵)) ≤ (𝐴 · (𝐿𝐵)))
140139, 35pm2.65i 195 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wcel 2080  wne 2983  wrex 3105  cin 3860  wss 3861   class class class wbr 4964  wf 6224  cfv 6228  (class class class)co 7019  cc 10384  cr 10385  0cc0 10386   · cmul 10391  *cxr 10523   < clt 10524  cle 10525   / cdiv 11147  cq 12197  +crp 12239  abscabs 14427  Basecbs 16312  Scalarcsca 16397   ·𝑠 cvsca 16398  0gc0g 16542   LMHom clmhm 19481  normcnm 22869  NrmGrpcngp 22870  NrmModcnlm 22873   normOp cnmo 22997  ℂModcclm 23349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-cnex 10442  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-mulcom 10450  ax-addass 10451  ax-mulass 10452  ax-distr 10453  ax-i2m1 10454  ax-1ne0 10455  ax-1rid 10456  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459  ax-pre-lttri 10460  ax-pre-lttrn 10461  ax-pre-ltadd 10462  ax-pre-mulgt0 10463  ax-pre-sup 10464  ax-addf 10465  ax-mulf 10466
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-nel 3090  df-ral 3109  df-rex 3110  df-reu 3111  df-rmo 3112  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-riota 6980  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-oadd 7960  df-er 8142  df-map 8261  df-en 8361  df-dom 8362  df-sdom 8363  df-fin 8364  df-sup 8755  df-inf 8756  df-pnf 10526  df-mnf 10527  df-xr 10528  df-ltxr 10529  df-le 10530  df-sub 10721  df-neg 10722  df-div 11148  df-nn 11489  df-2 11550  df-3 11551  df-4 11552  df-5 11553  df-6 11554  df-7 11555  df-8 11556  df-9 11557  df-n0 11748  df-z 11832  df-dec 11949  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-fz 12743  df-seq 13220  df-exp 13280  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-starv 16409  df-tset 16413  df-ple 16414  df-ds 16416  df-unif 16417  df-0g 16544  df-topgen 16546  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-grp 17864  df-subg 18030  df-ghm 18097  df-cmn 18635  df-mgp 18930  df-ring 18989  df-cring 18990  df-subrg 19223  df-lmod 19326  df-lmhm 19484  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-cnfld 20228  df-top 21186  df-topon 21203  df-topsp 21225  df-bases 21238  df-xms 22613  df-ms 22614  df-nm 22875  df-ngp 22876  df-nlm 22879  df-clm 23350
This theorem is referenced by:  nmoleub2lem2  23403
  Copyright terms: Public domain W3C validator