nmoleub2lem3

Description: Lemma for nmoleub2a and similar theorems. (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	$⊢ φ \to S \in (NrmMod \cap CMod)$
	nmoleub2.t	$⊢ φ \to T \in (NrmMod \cap CMod)$
	nmoleub2.f	$⊢ φ \to F \in (S LMHom T)$
	nmoleub2.a	$⊢ φ \to A \in ℝ^{*}$
	nmoleub2.r	$⊢ φ \to R \in ℝ^{+}$
	nmoleub2a.5	$⊢ φ \to ℚ \subseteq K$
	nmoleub2lem3.p	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	nmoleub2lem3.1	$⊢ φ \to A \in ℝ$
	nmoleub2lem3.2	$⊢ φ \to 0 \leq A$
	nmoleub2lem3.3	$⊢ φ \to B \in V$
	nmoleub2lem3.4	$⊢ φ \to B \neq 0_{S}$
	nmoleub2lem3.5	$⊢ φ \to (r \underset{˙}{\cdot} B \in V \to (L (r \underset{˙}{\cdot} B) < R \to \frac{M (F (r \underset{˙}{\cdot} B))}{R} \leq A))$
	nmoleub2lem3.6	$⊢ φ \to \neg M (F (B)) \leq A L (B)$
Assertion	nmoleub2lem3	$⊢ \neg φ$

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	$⊢ φ \to S \in (NrmMod \cap CMod)$
8		nmoleub2.t	$⊢ φ \to T \in (NrmMod \cap CMod)$
9		nmoleub2.f	$⊢ φ \to F \in (S LMHom T)$
10		nmoleub2.a	$⊢ φ \to A \in ℝ^{*}$
11		nmoleub2.r	$⊢ φ \to R \in ℝ^{+}$
12		nmoleub2a.5	$⊢ φ \to ℚ \subseteq K$
13		nmoleub2lem3.p	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
14		nmoleub2lem3.1	$⊢ φ \to A \in ℝ$
15		nmoleub2lem3.2	$⊢ φ \to 0 \leq A$
16		nmoleub2lem3.3	$⊢ φ \to B \in V$
17		nmoleub2lem3.4	$⊢ φ \to B \neq 0_{S}$
18		nmoleub2lem3.5	$⊢ φ \to (r \underset{˙}{\cdot} B \in V \to (L (r \underset{˙}{\cdot} B) < R \to \frac{M (F (r \underset{˙}{\cdot} B))}{R} \leq A))$
19		nmoleub2lem3.6	$⊢ φ \to \neg M (F (B)) \leq A L (B)$
20		simprl	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \frac{A R}{M (F (B))} < r$
21		qre	$⊢ r \in ℚ \to r \in ℝ$
22	21	ad2antlr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r \in ℝ$
23	11	rpred	$⊢ φ \to R \in ℝ$
24	14 23	remulcld	$⊢ φ \to A R \in ℝ$
25	8	elin1d	$⊢ φ \to T \in NrmMod$
26		nlmngp	$⊢ T \in NrmMod \to T \in NrmGrp$
27	25 26	syl	$⊢ φ \to T \in NrmGrp$
28		eqid	$⊢ {Base}_{T} = {Base}_{T}$
29	2 28	lmhmf	$⊢ F \in (S LMHom T) \to F : V ⟶ {Base}_{T}$
30	9 29	syl	$⊢ φ \to F : V ⟶ {Base}_{T}$
31	30 16	ffvelcdmd	$⊢ φ \to F (B) \in {Base}_{T}$
32	28 4	nmcl	$⊢ (T \in NrmGrp \land F (B) \in {Base}_{T}) \to M (F (B)) \in ℝ$
33	27 31 32	syl2anc	$⊢ φ \to M (F (B)) \in ℝ$
34		0red	$⊢ φ \to 0 \in ℝ$
35	7	elin1d	$⊢ φ \to S \in NrmMod$
36		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
37	35 36	syl	$⊢ φ \to S \in NrmGrp$
38	2 3	nmcl	$⊢ (S \in NrmGrp \land B \in V) \to L (B) \in ℝ$
39	37 16 38	syl2anc	$⊢ φ \to L (B) \in ℝ$
40	14 39	remulcld	$⊢ φ \to A L (B) \in ℝ$
41	2 3	nmge0	$⊢ (S \in NrmGrp \land B \in V) \to 0 \leq L (B)$
42	37 16 41	syl2anc	$⊢ φ \to 0 \leq L (B)$
43	14 39 15 42	mulge0d	$⊢ φ \to 0 \leq A L (B)$
44	40 33	ltnled	$⊢ φ \to (A L (B) < M (F (B)) \leftrightarrow \neg M (F (B)) \leq A L (B))$
45	19 44	mpbird	$⊢ φ \to A L (B) < M (F (B))$
46	34 40 33 43 45	lelttrd	$⊢ φ \to 0 < M (F (B))$
47	33 46	elrpd	$⊢ φ \to M (F (B)) \in ℝ^{+}$
48	24 47	rerpdivcld	$⊢ φ \to \frac{A R}{M (F (B))} \in ℝ$
49	48	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \frac{A R}{M (F (B))} \in ℝ$
50	9	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to F \in (S LMHom T)$
51	12	sselda	$⊢ (φ \land r \in ℚ) \to r \in K$
52	51	adantr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r \in K$
53	16	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to B \in V$
54		eqid	$⊢ \cdot_{T} = \cdot_{T}$
55	5 6 2 13 54	lmhmlin	$⊢ (F \in (S LMHom T) \land r \in K \land B \in V) \to F (r \underset{˙}{\cdot} B) = r \cdot_{T} F (B)$
56	50 52 53 55	syl3anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to F (r \underset{˙}{\cdot} B) = r \cdot_{T} F (B)$
57	56	fveq2d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to M (F (r \underset{˙}{\cdot} B)) = M (r \cdot_{T} F (B))$
58	25	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to T \in NrmMod$
59		eqid	$⊢ Scalar (T) = Scalar (T)$
60	5 59	lmhmsca	$⊢ F \in (S LMHom T) \to Scalar (T) = G$
61	50 60	syl	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to Scalar (T) = G$
62	61	fveq2d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to {Base}_{Scalar (T)} = {Base}_{G}$
63	62 6	eqtr4di	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to {Base}_{Scalar (T)} = K$
64	52 63	eleqtrrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r \in {Base}_{Scalar (T)}$
65	31	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to F (B) \in {Base}_{T}$
66		eqid	$⊢ {Base}_{Scalar (T)} = {Base}_{Scalar (T)}$
67		eqid	$⊢ norm (Scalar (T)) = norm (Scalar (T))$
68	28 4 54 59 66 67	nmvs	$⊢ (T \in NrmMod \land r \in {Base}_{Scalar (T)} \land F (B) \in {Base}_{T}) \to M (r \cdot_{T} F (B)) = norm (Scalar (T)) (r) M (F (B))$
69	58 64 65 68	syl3anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to M (r \cdot_{T} F (B)) = norm (Scalar (T)) (r) M (F (B))$
70	61	fveq2d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to norm (Scalar (T)) = norm (G)$
71	70	fveq1d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to norm (Scalar (T)) (r) = norm (G) (r)$
72	7	elin2d	$⊢ φ \to S \in CMod$
73	72	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to S \in CMod$
74	5 6	clmabs	$⊢ (S \in CMod \land r \in K) \to \|r\| = norm (G) (r)$
75	73 52 74	syl2anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \|r\| = norm (G) (r)$
76		0red	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to 0 \in ℝ$
77	11	rpge0d	$⊢ φ \to 0 \leq R$
78	14 23 15 77	mulge0d	$⊢ φ \to 0 \leq A R$
79		divge0	$⊢ ((A R \in ℝ \land 0 \leq A R) \land (M (F (B)) \in ℝ \land 0 < M (F (B)))) \to 0 \leq \frac{A R}{M (F (B))}$
80	24 78 33 46 79	syl22anc	$⊢ φ \to 0 \leq \frac{A R}{M (F (B))}$
81	80	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to 0 \leq \frac{A R}{M (F (B))}$
82	76 49 22 81 20	lelttrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to 0 < r$
83	76 22 82	ltled	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to 0 \leq r$
84	22 83	absidd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \|r\| = r$
85	75 84	eqtr3d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to norm (G) (r) = r$
86	71 85	eqtrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to norm (Scalar (T)) (r) = r$
87	86	oveq1d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to norm (Scalar (T)) (r) M (F (B)) = r M (F (B))$
88	57 69 87	3eqtrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to M (F (r \underset{˙}{\cdot} B)) = r M (F (B))$
89	88	oveq1d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \frac{M (F (r \underset{˙}{\cdot} B))}{R} = \frac{r M (F (B))}{R}$
90	2 5 13 6	clmvscl	$⊢ (S \in CMod \land r \in K \land B \in V) \to r \underset{˙}{\cdot} B \in V$
91	73 52 53 90	syl3anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r \underset{˙}{\cdot} B \in V$
92	35	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to S \in NrmMod$
93		eqid	$⊢ norm (G) = norm (G)$
94	2 3 13 5 6 93	nmvs	$⊢ (S \in NrmMod \land r \in K \land B \in V) \to L (r \underset{˙}{\cdot} B) = norm (G) (r) L (B)$
95	92 52 53 94	syl3anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to L (r \underset{˙}{\cdot} B) = norm (G) (r) L (B)$
96	85	oveq1d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to norm (G) (r) L (B) = r L (B)$
97	95 96	eqtrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to L (r \underset{˙}{\cdot} B) = r L (B)$
98		simprr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r < \frac{R}{L (B)}$
99	23	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to R \in ℝ$
100		eqid	$⊢ 0_{S} = 0_{S}$
101	2 3 100	nmrpcl	$⊢ (S \in NrmGrp \land B \in V \land B \neq 0_{S}) \to L (B) \in ℝ^{+}$
102	37 16 17 101	syl3anc	$⊢ φ \to L (B) \in ℝ^{+}$
103	102	rpregt0d	$⊢ φ \to (L (B) \in ℝ \land 0 < L (B))$
104	103	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to (L (B) \in ℝ \land 0 < L (B))$
105		ltmuldiv	$⊢ (r \in ℝ \land R \in ℝ \land (L (B) \in ℝ \land 0 < L (B))) \to (r L (B) < R \leftrightarrow r < \frac{R}{L (B)})$
106	22 99 104 105	syl3anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to (r L (B) < R \leftrightarrow r < \frac{R}{L (B)})$
107	98 106	mpbird	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r L (B) < R$
108	97 107	eqbrtrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to L (r \underset{˙}{\cdot} B) < R$
109	18	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to (r \underset{˙}{\cdot} B \in V \to (L (r \underset{˙}{\cdot} B) < R \to \frac{M (F (r \underset{˙}{\cdot} B))}{R} \leq A))$
110	91 108 109	mp2d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \frac{M (F (r \underset{˙}{\cdot} B))}{R} \leq A$
111	89 110	eqbrtrrd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \frac{r M (F (B))}{R} \leq A$
112	33	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to M (F (B)) \in ℝ$
113	22 112	remulcld	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r M (F (B)) \in ℝ$
114	14	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to A \in ℝ$
115	11	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to R \in ℝ^{+}$
116	113 114 115	ledivmul2d	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to (\frac{r M (F (B))}{R} \leq A \leftrightarrow r M (F (B)) \leq A R)$
117	111 116	mpbid	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r M (F (B)) \leq A R$
118	114 99	remulcld	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to A R \in ℝ$
119	33 46	jca	$⊢ φ \to (M (F (B)) \in ℝ \land 0 < M (F (B)))$
120	119	ad2antrr	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to (M (F (B)) \in ℝ \land 0 < M (F (B)))$
121		lemuldiv	$⊢ (r \in ℝ \land A R \in ℝ \land (M (F (B)) \in ℝ \land 0 < M (F (B)))) \to (r M (F (B)) \leq A R \leftrightarrow r \leq \frac{A R}{M (F (B))})$
122	22 118 120 121	syl3anc	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to (r M (F (B)) \leq A R \leftrightarrow r \leq \frac{A R}{M (F (B))})$
123	117 122	mpbid	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to r \leq \frac{A R}{M (F (B))}$
124	22 49 123	lensymd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to \neg \frac{A R}{M (F (B))} < r$
125	20 124	pm2.21dd	$⊢ ((φ \land r \in ℚ) \land (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})) \to M (F (B)) \leq A L (B)$
126	23 102	rerpdivcld	$⊢ φ \to \frac{R}{L (B)} \in ℝ$
127	14	recnd	$⊢ φ \to A \in ℂ$
128	23	recnd	$⊢ φ \to R \in ℂ$
129	39	recnd	$⊢ φ \to L (B) \in ℂ$
130		mulass	$⊢ (A \in ℂ \land R \in ℂ \land L (B) \in ℂ) \to A R L (B) = A R L (B)$
131		mul12	$⊢ (A \in ℂ \land R \in ℂ \land L (B) \in ℂ) \to A R L (B) = R A L (B)$
132	130 131	eqtrd	$⊢ (A \in ℂ \land R \in ℂ \land L (B) \in ℂ) \to A R L (B) = R A L (B)$
133	127 128 129 132	syl3anc	$⊢ φ \to A R L (B) = R A L (B)$
134	40 33 11 45	ltmul2dd	$⊢ φ \to R A L (B) < R M (F (B))$
135	133 134	eqbrtrd	$⊢ φ \to A R L (B) < R M (F (B))$
136		lt2mul2div	$⊢ ((A R \in ℝ \land (L (B) \in ℝ \land 0 < L (B))) \land (R \in ℝ \land (M (F (B)) \in ℝ \land 0 < M (F (B))))) \to (A R L (B) < R M (F (B)) \leftrightarrow \frac{A R}{M (F (B))} < \frac{R}{L (B)})$
137	24 103 23 119 136	syl22anc	$⊢ φ \to (A R L (B) < R M (F (B)) \leftrightarrow \frac{A R}{M (F (B))} < \frac{R}{L (B)})$
138	135 137	mpbid	$⊢ φ \to \frac{A R}{M (F (B))} < \frac{R}{L (B)}$
139		qbtwnre	$⊢ (\frac{A R}{M (F (B))} \in ℝ \land \frac{R}{L (B)} \in ℝ \land \frac{A R}{M (F (B))} < \frac{R}{L (B)}) \to \exists r \in ℚ (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})$
140	48 126 138 139	syl3anc	$⊢ φ \to \exists r \in ℚ (\frac{A R}{M (F (B))} < r \land r < \frac{R}{L (B)})$
141	125 140	r19.29a	$⊢ φ \to M (F (B)) \leq A L (B)$
142	141 19	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem nmoleub2lem3

Proof