nmoleub2lem

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 ℝ^{+}$
	nmoleub2lem.5	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to 0 \leq A$
	nmoleub2lem.6	$⊢ (((φ \land \forall x \in V (ψ \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)$
	nmoleub2lem.7	$⊢ (φ \land x \in V) \to (ψ \to L (x) \leq R)$
Assertion	nmoleub2lem	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (ψ \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		nmoleub2lem.5	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to 0 \leq A$
13		nmoleub2lem.6	$⊢ (((φ \land \forall x \in V (ψ \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)$
14		nmoleub2lem.7	$⊢ (φ \land x \in V) \to (ψ \to L (x) \leq R)$
15	14	adantlr	$⊢ ((φ \land N (F) \leq A) \land x \in V) \to (ψ \to L (x) \leq R)$
16	8	elin1d	$⊢ φ \to T \in NrmMod$
17		nlmngp	$⊢ T \in NrmMod \to T \in NrmGrp$
18	16 17	syl	$⊢ φ \to T \in NrmGrp$
19	18	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to T \in NrmGrp$
20		eqid	$⊢ {Base}_{T} = {Base}_{T}$
21	2 20	lmhmf	$⊢ F \in (S LMHom T) \to F : V ⟶ {Base}_{T}$
22	9 21	syl	$⊢ φ \to F : V ⟶ {Base}_{T}$
23	22	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to F : V ⟶ {Base}_{T}$
24		simprl	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to x \in V$
25	23 24	ffvelcdmd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to F (x) \in {Base}_{T}$
26	20 4	nmcl	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T}) \to M (F (x)) \in ℝ$
27	19 25 26	syl2anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to M (F (x)) \in ℝ$
28	11	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to R \in ℝ^{+}$
29	27 28	rerpdivcld	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to \frac{M (F (x))}{R} \in ℝ$
30	29	rexrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to \frac{M (F (x))}{R} \in ℝ^{*}$
31	7	elin1d	$⊢ φ \to S \in NrmMod$
32		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
33	31 32	syl	$⊢ φ \to S \in NrmGrp$
34		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
35	9 34	syl	$⊢ φ \to F \in (S GrpHom T)$
36	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
37	33 18 35 36	syl3anc	$⊢ φ \to N (F) \in ℝ^{*}$
38	37	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to N (F) \in ℝ^{*}$
39	10	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to A \in ℝ^{*}$
40	28	rpred	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to R \in ℝ$
41		rexmul	$⊢ (\frac{M (F (x))}{R} \in ℝ \land R \in ℝ) \to (\frac{M (F (x))}{R}) \cdot_{𝑒} R = (\frac{M (F (x))}{R}) R$
42	29 40 41	syl2anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to (\frac{M (F (x))}{R}) \cdot_{𝑒} R = (\frac{M (F (x))}{R}) R$
43	27	recnd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to M (F (x)) \in ℂ$
44	40	recnd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to R \in ℂ$
45	28	rpne0d	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to R \neq 0$
46	43 44 45	divcan1d	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to (\frac{M (F (x))}{R}) R = M (F (x))$
47	42 46	eqtrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to (\frac{M (F (x))}{R}) \cdot_{𝑒} R = M (F (x))$
48	27	rexrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to M (F (x)) \in ℝ^{*}$
49	33	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to S \in NrmGrp$
50	2 3	nmcl	$⊢ (S \in NrmGrp \land x \in V) \to L (x) \in ℝ$
51	49 24 50	syl2anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to L (x) \in ℝ$
52	51	rexrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to L (x) \in ℝ^{*}$
53	38 52	xmulcld	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to N (F) \cdot_{𝑒} L (x) \in ℝ^{*}$
54	28	rpxrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to R \in ℝ^{*}$
55	38 54	xmulcld	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to N (F) \cdot_{𝑒} R \in ℝ^{*}$
56	35	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to F \in (S GrpHom T)$
57	1 2 3 4	nmoix	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land x \in V) \to M (F (x)) \leq N (F) \cdot_{𝑒} L (x)$
58	49 19 56 24 57	syl31anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to M (F (x)) \leq N (F) \cdot_{𝑒} L (x)$
59	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq N (F)$
60	33 18 35 59	syl3anc	$⊢ φ \to 0 \leq N (F)$
61	37 60	jca	$⊢ φ \to (N (F) \in ℝ^{*} \land 0 \leq N (F))$
62	61	ad2antrr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to (N (F) \in ℝ^{*} \land 0 \leq N (F))$
63		simprr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to L (x) \leq R$
64		xlemul2a	$⊢ ((L (x) \in ℝ^{} \land R \in ℝ^{} \land (N (F) \in ℝ^{*} \land 0 \leq N (F))) \land L (x) \leq R) \to N (F) \cdot_{𝑒} L (x) \leq N (F) \cdot_{𝑒} R$
65	52 54 62 63 64	syl31anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to N (F) \cdot_{𝑒} L (x) \leq N (F) \cdot_{𝑒} R$
66	48 53 55 58 65	xrletrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to M (F (x)) \leq N (F) \cdot_{𝑒} R$
67	47 66	eqbrtrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to (\frac{M (F (x))}{R}) \cdot_{𝑒} R \leq N (F) \cdot_{𝑒} R$
68		xlemul1	$⊢ (\frac{M (F (x))}{R} \in ℝ^{} \land N (F) \in ℝ^{} \land R \in ℝ^{+}) \to (\frac{M (F (x))}{R} \leq N (F) \leftrightarrow (\frac{M (F (x))}{R}) \cdot_{𝑒} R \leq N (F) \cdot_{𝑒} R)$
69	30 38 28 68	syl3anc	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to (\frac{M (F (x))}{R} \leq N (F) \leftrightarrow (\frac{M (F (x))}{R}) \cdot_{𝑒} R \leq N (F) \cdot_{𝑒} R)$
70	67 69	mpbird	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to \frac{M (F (x))}{R} \leq N (F)$
71		simplr	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to N (F) \leq A$
72	30 38 39 70 71	xrletrd	$⊢ ((φ \land N (F) \leq A) \land (x \in V \land L (x) \leq R)) \to \frac{M (F (x))}{R} \leq A$
73	72	expr	$⊢ ((φ \land N (F) \leq A) \land x \in V) \to (L (x) \leq R \to \frac{M (F (x))}{R} \leq A)$
74	15 73	syld	$⊢ ((φ \land N (F) \leq A) \land x \in V) \to (ψ \to \frac{M (F (x))}{R} \leq A)$
75	74	ralrimiva	$⊢ (φ \land N (F) \leq A) \to \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)$
76		eqid	$⊢ 0_{S} = 0_{S}$
77	33	ad2antrr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \to S \in NrmGrp$
78	18	ad2antrr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \to T \in NrmGrp$
79	35	ad2antrr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \to F \in (S GrpHom T)$
80		simpr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \to A \in ℝ$
81	12	adantr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \to 0 \leq A$
82	1 2 3 4 76 77 78 79 80 81 13	nmolb2d	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A \in ℝ) \to N (F) \leq A$
83	37	ad2antrr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A = +∞) \to N (F) \in ℝ^{*}$
84		pnfge	$⊢ N (F) \in ℝ^{*} \to N (F) \leq +∞$
85	83 84	syl	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A = +∞) \to N (F) \leq +∞$
86		simpr	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A = +∞) \to A = +∞$
87	85 86	breqtrrd	$⊢ ((φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \land A = +∞) \to N (F) \leq A$
88	10	adantr	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to A \in ℝ^{*}$
89		ge0nemnf	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to A \neq −∞$
90	88 12 89	syl2anc	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to A \neq −∞$
91	88 90	jca	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to (A \in ℝ^{*} \land A \neq −∞)$
92		xrnemnf	$⊢ (A \in ℝ^{*} \land A \neq −∞) \leftrightarrow (A \in ℝ \lor A = +∞)$
93	91 92	sylib	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to (A \in ℝ \lor A = +∞)$
94	82 87 93	mpjaodan	$⊢ (φ \land \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A)) \to N (F) \leq A$
95	75 94	impbida	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (ψ \to \frac{M (F (x))}{R} \leq A))$

Metamath Proof Explorer

Theorem nmoleub2lem

Proof