supmul1

Description: The supremum function distributes over multiplication, in the sense that A x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { A x. b | b e. B } and is defined as C below. This is the simple version, with only one set argument; see supmul for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013)

	Ref	Expression
Hypotheses	supmul1.1	$⊢ C = \{z \| \exists v \in B z = A v\}$
	supmul1.2	$⊢ φ \leftrightarrow ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x))$
Assertion	supmul1	$⊢ φ \to A sup (B ℝ <) = sup (C ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		supmul1.1	$⊢ C = \{z \| \exists v \in B z = A v\}$
2		supmul1.2	$⊢ φ \leftrightarrow ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x))$
3		vex	$⊢ w \in V$
4		oveq2	$⊢ v = b \to A v = A b$
5	4	eqeq2d	$⊢ v = b \to (z = A v \leftrightarrow z = A b)$
6	5	cbvrexvw	$⊢ \exists v \in B z = A v \leftrightarrow \exists b \in B z = A b$
7		eqeq1	$⊢ z = w \to (z = A b \leftrightarrow w = A b)$
8	7	rexbidv	$⊢ z = w \to (\exists b \in B z = A b \leftrightarrow \exists b \in B w = A b)$
9	6 8	syl5bb	$⊢ z = w \to (\exists v \in B z = A v \leftrightarrow \exists b \in B w = A b)$
10	3 9 1	elab2	$⊢ w \in C \leftrightarrow \exists b \in B w = A b$
11		simpr	$⊢ ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
12	2 11	sylbi	$⊢ φ \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
13	12	simp1d	$⊢ φ \to B \subseteq ℝ$
14	13	sselda	$⊢ (φ \land b \in B) \to b \in ℝ$
15		suprcl	$⊢ (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x) \to sup (B ℝ <) \in ℝ$
16	12 15	syl	$⊢ φ \to sup (B ℝ <) \in ℝ$
17	16	adantr	$⊢ (φ \land b \in B) \to sup (B ℝ <) \in ℝ$
18		simpl1	$⊢ ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to A \in ℝ$
19	2 18	sylbi	$⊢ φ \to A \in ℝ$
20		simpl2	$⊢ ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to 0 \leq A$
21	2 20	sylbi	$⊢ φ \to 0 \leq A$
22	19 21	jca	$⊢ φ \to (A \in ℝ \land 0 \leq A)$
23	22	adantr	$⊢ (φ \land b \in B) \to (A \in ℝ \land 0 \leq A)$
24		suprub	$⊢ ((B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x) \land b \in B) \to b \leq sup (B ℝ <)$
25	12 24	sylan	$⊢ (φ \land b \in B) \to b \leq sup (B ℝ <)$
26		lemul2a	$⊢ ((b \in ℝ \land sup (B ℝ <) \in ℝ \land (A \in ℝ \land 0 \leq A)) \land b \leq sup (B ℝ <)) \to A b \leq A sup (B ℝ <)$
27	14 17 23 25 26	syl31anc	$⊢ (φ \land b \in B) \to A b \leq A sup (B ℝ <)$
28		breq1	$⊢ w = A b \to (w \leq A sup (B ℝ <) \leftrightarrow A b \leq A sup (B ℝ <))$
29	27 28	syl5ibrcom	$⊢ (φ \land b \in B) \to (w = A b \to w \leq A sup (B ℝ <))$
30	29	rexlimdva	$⊢ φ \to (\exists b \in B w = A b \to w \leq A sup (B ℝ <))$
31	10 30	syl5bi	$⊢ φ \to (w \in C \to w \leq A sup (B ℝ <))$
32	31	ralrimiv	$⊢ φ \to \forall w \in C w \leq A sup (B ℝ <)$
33	19	adantr	$⊢ (φ \land b \in B) \to A \in ℝ$
34	33 14	remulcld	$⊢ (φ \land b \in B) \to A b \in ℝ$
35		eleq1a	$⊢ A b \in ℝ \to (w = A b \to w \in ℝ)$
36	34 35	syl	$⊢ (φ \land b \in B) \to (w = A b \to w \in ℝ)$
37	36	rexlimdva	$⊢ φ \to (\exists b \in B w = A b \to w \in ℝ)$
38	10 37	syl5bi	$⊢ φ \to (w \in C \to w \in ℝ)$
39	38	ssrdv	$⊢ φ \to C \subseteq ℝ$
40		simpr2	$⊢ ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to B \neq \emptyset$
41	2 40	sylbi	$⊢ φ \to B \neq \emptyset$
42		ovex	$⊢ A b \in V$
43	42	isseti	$⊢ \exists w w = A b$
44	43	rgenw	$⊢ \forall b \in B \exists w w = A b$
45		r19.2z	$⊢ (B \neq \emptyset \land \forall b \in B \exists w w = A b) \to \exists b \in B \exists w w = A b$
46	41 44 45	sylancl	$⊢ φ \to \exists b \in B \exists w w = A b$
47	10	exbii	$⊢ \exists w w \in C \leftrightarrow \exists w \exists b \in B w = A b$
48		n0	$⊢ C \neq \emptyset \leftrightarrow \exists w w \in C$
49		rexcom4	$⊢ \exists b \in B \exists w w = A b \leftrightarrow \exists w \exists b \in B w = A b$
50	47 48 49	3bitr4i	$⊢ C \neq \emptyset \leftrightarrow \exists b \in B \exists w w = A b$
51	46 50	sylibr	$⊢ φ \to C \neq \emptyset$
52	19 16	remulcld	$⊢ φ \to A sup (B ℝ <) \in ℝ$
53		brralrspcev	$⊢ (A sup (B ℝ <) \in ℝ \land \forall w \in C w \leq A sup (B ℝ <)) \to \exists x \in ℝ \forall w \in C w \leq x$
54	52 32 53	syl2anc	$⊢ φ \to \exists x \in ℝ \forall w \in C w \leq x$
55	39 51 54	3jca	$⊢ φ \to (C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x)$
56		suprleub	$⊢ ((C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \land A sup (B ℝ <) \in ℝ) \to (sup (C ℝ <) \leq A sup (B ℝ <) \leftrightarrow \forall w \in C w \leq A sup (B ℝ <))$
57	55 52 56	syl2anc	$⊢ φ \to (sup (C ℝ <) \leq A sup (B ℝ <) \leftrightarrow \forall w \in C w \leq A sup (B ℝ <))$
58	32 57	mpbird	$⊢ φ \to sup (C ℝ <) \leq A sup (B ℝ <)$
59		simpr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to sup (C ℝ <) < A sup (B ℝ <)$
60		suprcl	$⊢ (C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \to sup (C ℝ <) \in ℝ$
61	55 60	syl	$⊢ φ \to sup (C ℝ <) \in ℝ$
62	61	adantr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to sup (C ℝ <) \in ℝ$
63	16	adantr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to sup (B ℝ <) \in ℝ$
64	19	adantr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to A \in ℝ$
65		n0	$⊢ B \neq \emptyset \leftrightarrow \exists b b \in B$
66		0red	$⊢ (φ \land b \in B) \to 0 \in ℝ$
67		simpl3	$⊢ ((A \in ℝ \land 0 \leq A \land \forall x \in B 0 \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to \forall x \in B 0 \leq x$
68	2 67	sylbi	$⊢ φ \to \forall x \in B 0 \leq x$
69		breq2	$⊢ x = b \to (0 \leq x \leftrightarrow 0 \leq b)$
70	69	rspccva	$⊢ (\forall x \in B 0 \leq x \land b \in B) \to 0 \leq b$
71	68 70	sylan	$⊢ (φ \land b \in B) \to 0 \leq b$
72	66 14 17 71 25	letrd	$⊢ (φ \land b \in B) \to 0 \leq sup (B ℝ <)$
73	72	ex	$⊢ φ \to (b \in B \to 0 \leq sup (B ℝ <))$
74	73	exlimdv	$⊢ φ \to (\exists b b \in B \to 0 \leq sup (B ℝ <))$
75	65 74	syl5bi	$⊢ φ \to (B \neq \emptyset \to 0 \leq sup (B ℝ <))$
76	41 75	mpd	$⊢ φ \to 0 \leq sup (B ℝ <)$
77	76	adantr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to 0 \leq sup (B ℝ <)$
78		0red	$⊢ (φ \land w \in C) \to 0 \in ℝ$
79	38	imp	$⊢ (φ \land w \in C) \to w \in ℝ$
80	61	adantr	$⊢ (φ \land w \in C) \to sup (C ℝ <) \in ℝ$
81	21	adantr	$⊢ (φ \land b \in B) \to 0 \leq A$
82	33 14 81 71	mulge0d	$⊢ (φ \land b \in B) \to 0 \leq A b$
83		breq2	$⊢ w = A b \to (0 \leq w \leftrightarrow 0 \leq A b)$
84	82 83	syl5ibrcom	$⊢ (φ \land b \in B) \to (w = A b \to 0 \leq w)$
85	84	rexlimdva	$⊢ φ \to (\exists b \in B w = A b \to 0 \leq w)$
86	10 85	syl5bi	$⊢ φ \to (w \in C \to 0 \leq w)$
87	86	imp	$⊢ (φ \land w \in C) \to 0 \leq w$
88		suprub	$⊢ ((C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \land w \in C) \to w \leq sup (C ℝ <)$
89	55 88	sylan	$⊢ (φ \land w \in C) \to w \leq sup (C ℝ <)$
90	78 79 80 87 89	letrd	$⊢ (φ \land w \in C) \to 0 \leq sup (C ℝ <)$
91	90	ex	$⊢ φ \to (w \in C \to 0 \leq sup (C ℝ <))$
92	91	exlimdv	$⊢ φ \to (\exists w w \in C \to 0 \leq sup (C ℝ <))$
93	48 92	syl5bi	$⊢ φ \to (C \neq \emptyset \to 0 \leq sup (C ℝ <))$
94	51 93	mpd	$⊢ φ \to 0 \leq sup (C ℝ <)$
95	94	anim1i	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to (0 \leq sup (C ℝ <) \land sup (C ℝ <) < A sup (B ℝ <))$
96		0red	$⊢ φ \to 0 \in ℝ$
97		lelttr	$⊢ (0 \in ℝ \land sup (C ℝ <) \in ℝ \land A sup (B ℝ <) \in ℝ) \to ((0 \leq sup (C ℝ <) \land sup (C ℝ <) < A sup (B ℝ <)) \to 0 < A sup (B ℝ <))$
98	96 61 52 97	syl3anc	$⊢ φ \to ((0 \leq sup (C ℝ <) \land sup (C ℝ <) < A sup (B ℝ <)) \to 0 < A sup (B ℝ <))$
99	98	adantr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to ((0 \leq sup (C ℝ <) \land sup (C ℝ <) < A sup (B ℝ <)) \to 0 < A sup (B ℝ <))$
100	95 99	mpd	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to 0 < A sup (B ℝ <)$
101		prodgt02	$⊢ ((A \in ℝ \land sup (B ℝ <) \in ℝ) \land (0 \leq sup (B ℝ <) \land 0 < A sup (B ℝ <))) \to 0 < A$
102	64 63 77 100 101	syl22anc	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to 0 < A$
103		ltdivmul	$⊢ (sup (C ℝ <) \in ℝ \land sup (B ℝ <) \in ℝ \land (A \in ℝ \land 0 < A)) \to (\frac{sup (C ℝ <)}{A} < sup (B ℝ <) \leftrightarrow sup (C ℝ <) < A sup (B ℝ <))$
104	62 63 64 102 103	syl112anc	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to (\frac{sup (C ℝ <)}{A} < sup (B ℝ <) \leftrightarrow sup (C ℝ <) < A sup (B ℝ <))$
105	59 104	mpbird	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to \frac{sup (C ℝ <)}{A} < sup (B ℝ <)$
106	12	adantr	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
107	102	gt0ne0d	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to A \neq 0$
108	62 64 107	redivcld	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to \frac{sup (C ℝ <)}{A} \in ℝ$
109		suprlub	$⊢ ((B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x) \land \frac{sup (C ℝ <)}{A} \in ℝ) \to (\frac{sup (C ℝ <)}{A} < sup (B ℝ <) \leftrightarrow \exists b \in B \frac{sup (C ℝ <)}{A} < b)$
110	106 108 109	syl2anc	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to (\frac{sup (C ℝ <)}{A} < sup (B ℝ <) \leftrightarrow \exists b \in B \frac{sup (C ℝ <)}{A} < b)$
111	105 110	mpbid	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to \exists b \in B \frac{sup (C ℝ <)}{A} < b$
112	34	adantlr	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to A b \in ℝ$
113	61	ad2antrr	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to sup (C ℝ <) \in ℝ$
114		rspe	$⊢ (b \in B \land w = A b) \to \exists b \in B w = A b$
115	114 10	sylibr	$⊢ (b \in B \land w = A b) \to w \in C$
116	115	adantl	$⊢ (φ \land (b \in B \land w = A b)) \to w \in C$
117		simplrr	$⊢ ((φ \land (b \in B \land w = A b)) \land w \in C) \to w = A b$
118	89	adantlr	$⊢ ((φ \land (b \in B \land w = A b)) \land w \in C) \to w \leq sup (C ℝ <)$
119	117 118	eqbrtrrd	$⊢ ((φ \land (b \in B \land w = A b)) \land w \in C) \to A b \leq sup (C ℝ <)$
120	116 119	mpdan	$⊢ (φ \land (b \in B \land w = A b)) \to A b \leq sup (C ℝ <)$
121	120	expr	$⊢ (φ \land b \in B) \to (w = A b \to A b \leq sup (C ℝ <))$
122	121	exlimdv	$⊢ (φ \land b \in B) \to (\exists w w = A b \to A b \leq sup (C ℝ <))$
123	43 122	mpi	$⊢ (φ \land b \in B) \to A b \leq sup (C ℝ <)$
124	123	adantlr	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to A b \leq sup (C ℝ <)$
125	112 113 124	lensymd	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to \neg sup (C ℝ <) < A b$
126	14	adantlr	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to b \in ℝ$
127	19	ad2antrr	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to A \in ℝ$
128	102	adantr	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to 0 < A$
129		ltdivmul	$⊢ (sup (C ℝ <) \in ℝ \land b \in ℝ \land (A \in ℝ \land 0 < A)) \to (\frac{sup (C ℝ <)}{A} < b \leftrightarrow sup (C ℝ <) < A b)$
130	113 126 127 128 129	syl112anc	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to (\frac{sup (C ℝ <)}{A} < b \leftrightarrow sup (C ℝ <) < A b)$
131	125 130	mtbird	$⊢ ((φ \land sup (C ℝ <) < A sup (B ℝ <)) \land b \in B) \to \neg \frac{sup (C ℝ <)}{A} < b$
132	131	nrexdv	$⊢ (φ \land sup (C ℝ <) < A sup (B ℝ <)) \to \neg \exists b \in B \frac{sup (C ℝ <)}{A} < b$
133	111 132	pm2.65da	$⊢ φ \to \neg sup (C ℝ <) < A sup (B ℝ <)$
134	58 133	jca	$⊢ φ \to (sup (C ℝ <) \leq A sup (B ℝ <) \land \neg sup (C ℝ <) < A sup (B ℝ <))$
135	61 52	eqleltd	$⊢ φ \to (sup (C ℝ <) = A sup (B ℝ <) \leftrightarrow (sup (C ℝ <) \leq A sup (B ℝ <) \land \neg sup (C ℝ <) < A sup (B ℝ <)))$
136	134 135	mpbird	$⊢ φ \to sup (C ℝ <) = A sup (B ℝ <)$
137	136	eqcomd	$⊢ φ \to A sup (B ℝ <) = sup (C ℝ <)$

Metamath Proof Explorer

Theorem supmul1

Proof