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

Metamath Proof Explorer

Theorem nmoleub2lem2

Proof