supmul

Description: The supremum function distributes over multiplication, in the sense that ( sup A ) x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { a x. b | a e. A , b e. B } and is defined as C below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp ). (Contributed by Mario Carneiro, 5-Jul-2013) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		supmul.1	$⊢ C = \{z \| \exists v \in A \exists b \in B z = v b\}$
2		supmul.2	$⊢ φ \leftrightarrow ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x))$
3	2	simp2bi	$⊢ φ \to (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
4		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
5	3 4	syl	$⊢ φ \to sup (A ℝ <) \in ℝ$
6	2	simp3bi	$⊢ φ \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
7		suprcl	$⊢ (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x) \to sup (B ℝ <) \in ℝ$
8	6 7	syl	$⊢ φ \to sup (B ℝ <) \in ℝ$
9		recn	$⊢ sup (A ℝ <) \in ℝ \to sup (A ℝ <) \in ℂ$
10		recn	$⊢ sup (B ℝ <) \in ℝ \to sup (B ℝ <) \in ℂ$
11		mulcom	$⊢ (sup (A ℝ <) \in ℂ \land sup (B ℝ <) \in ℂ) \to sup (A ℝ <) sup (B ℝ <) = sup (B ℝ <) sup (A ℝ <)$
12	9 10 11	syl2an	$⊢ (sup (A ℝ <) \in ℝ \land sup (B ℝ <) \in ℝ) \to sup (A ℝ <) sup (B ℝ <) = sup (B ℝ <) sup (A ℝ <)$
13	5 8 12	syl2anc	$⊢ φ \to sup (A ℝ <) sup (B ℝ <) = sup (B ℝ <) sup (A ℝ <)$
14	6	simp2d	$⊢ φ \to B \neq \emptyset$
15		n0	$⊢ B \neq \emptyset \leftrightarrow \exists b b \in B$
16	14 15	sylib	$⊢ φ \to \exists b b \in B$
17		0red	$⊢ (φ \land b \in B) \to 0 \in ℝ$
18	6	simp1d	$⊢ φ \to B \subseteq ℝ$
19	18	sselda	$⊢ (φ \land b \in B) \to b \in ℝ$
20	8	adantr	$⊢ (φ \land b \in B) \to sup (B ℝ <) \in ℝ$
21		simp1r	$⊢ ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \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$
22	2 21	sylbi	$⊢ φ \to \forall x \in B 0 \leq x$
23		breq2	$⊢ x = b \to (0 \leq x \leftrightarrow 0 \leq b)$
24	23	rspccv	$⊢ \forall x \in B 0 \leq x \to (b \in B \to 0 \leq b)$
25	22 24	syl	$⊢ φ \to (b \in B \to 0 \leq b)$
26	25	imp	$⊢ (φ \land b \in B) \to 0 \leq b$
27		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 ℝ <)$
28	6 27	sylan	$⊢ (φ \land b \in B) \to b \leq sup (B ℝ <)$
29	17 19 20 26 28	letrd	$⊢ (φ \land b \in B) \to 0 \leq sup (B ℝ <)$
30	16 29	exlimddv	$⊢ φ \to 0 \leq sup (B ℝ <)$
31		simp1l	$⊢ ((\forall x \in A 0 \leq x \land \forall x \in B 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)) \to \forall x \in A 0 \leq x$
32	2 31	sylbi	$⊢ φ \to \forall x \in A 0 \leq x$
33		eqid	$⊢ \{z \| \exists a \in A z = sup (B ℝ <) a\} = \{z \| \exists a \in A z = sup (B ℝ <) a\}$
34		biid	$⊢ ((sup (B ℝ <) \in ℝ \land 0 \leq sup (B ℝ <) \land \forall x \in A 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)) \leftrightarrow ((sup (B ℝ <) \in ℝ \land 0 \leq sup (B ℝ <) \land \forall x \in A 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x))$
35	33 34	supmul1	$⊢ ((sup (B ℝ <) \in ℝ \land 0 \leq sup (B ℝ <) \land \forall x \in A 0 \leq x) \land (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)) \to sup (B ℝ <) sup (A ℝ <) = sup (\{z \| \exists a \in A z = sup (B ℝ <) a\} ℝ <)$
36	8 30 32 3 35	syl31anc	$⊢ φ \to sup (B ℝ <) sup (A ℝ <) = sup (\{z \| \exists a \in A z = sup (B ℝ <) a\} ℝ <)$
37	13 36	eqtrd	$⊢ φ \to sup (A ℝ <) sup (B ℝ <) = sup (\{z \| \exists a \in A z = sup (B ℝ <) a\} ℝ <)$
38		vex	$⊢ w \in V$
39		eqeq1	$⊢ z = w \to (z = sup (B ℝ <) a \leftrightarrow w = sup (B ℝ <) a)$
40	39	rexbidv	$⊢ z = w \to (\exists a \in A z = sup (B ℝ <) a \leftrightarrow \exists a \in A w = sup (B ℝ <) a)$
41	38 40	elab	$⊢ w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} \leftrightarrow \exists a \in A w = sup (B ℝ <) a$
42	8	adantr	$⊢ (φ \land a \in A) \to sup (B ℝ <) \in ℝ$
43	3	simp1d	$⊢ φ \to A \subseteq ℝ$
44	43	sselda	$⊢ (φ \land a \in A) \to a \in ℝ$
45		recn	$⊢ a \in ℝ \to a \in ℂ$
46		mulcom	$⊢ (sup (B ℝ <) \in ℂ \land a \in ℂ) \to sup (B ℝ <) a = a sup (B ℝ <)$
47	10 45 46	syl2an	$⊢ (sup (B ℝ <) \in ℝ \land a \in ℝ) \to sup (B ℝ <) a = a sup (B ℝ <)$
48	42 44 47	syl2anc	$⊢ (φ \land a \in A) \to sup (B ℝ <) a = a sup (B ℝ <)$
49		breq2	$⊢ x = a \to (0 \leq x \leftrightarrow 0 \leq a)$
50	49	rspccv	$⊢ \forall x \in A 0 \leq x \to (a \in A \to 0 \leq a)$
51	32 50	syl	$⊢ φ \to (a \in A \to 0 \leq a)$
52	51	imp	$⊢ (φ \land a \in A) \to 0 \leq a$
53	22	adantr	$⊢ (φ \land a \in A) \to \forall x \in B 0 \leq x$
54	6	adantr	$⊢ (φ \land a \in A) \to (B \subseteq ℝ \land B \neq \emptyset \land \exists x \in ℝ \forall y \in B y \leq x)$
55		eqid	$⊢ \{z \| \exists b \in B z = a b\} = \{z \| \exists b \in B z = a b\}$
56		biid	$⊢ ((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)) \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))$
57	55 56	supmul1	$⊢ ((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 sup (B ℝ <) = sup (\{z \| \exists b \in B z = a b\} ℝ <)$
58	44 52 53 54 57	syl31anc	$⊢ (φ \land a \in A) \to a sup (B ℝ <) = sup (\{z \| \exists b \in B z = a b\} ℝ <)$
59		eqeq1	$⊢ z = w \to (z = a b \leftrightarrow w = a b)$
60	59	rexbidv	$⊢ z = w \to (\exists b \in B z = a b \leftrightarrow \exists b \in B w = a b)$
61	38 60	elab	$⊢ w \in \{z \| \exists b \in B z = a b\} \leftrightarrow \exists b \in B w = a b$
62		rspe	$⊢ (a \in A \land \exists b \in B w = a b) \to \exists a \in A \exists b \in B w = a b$
63		oveq1	$⊢ v = a \to v b = a b$
64	63	eqeq2d	$⊢ v = a \to (z = v b \leftrightarrow z = a b)$
65	64	rexbidv	$⊢ v = a \to (\exists b \in B z = v b \leftrightarrow \exists b \in B z = a b)$
66	65	cbvrexvw	$⊢ \exists v \in A \exists b \in B z = v b \leftrightarrow \exists a \in A \exists b \in B z = a b$
67	59	2rexbidv	$⊢ z = w \to (\exists a \in A \exists b \in B z = a b \leftrightarrow \exists a \in A \exists b \in B w = a b)$
68	66 67	syl5bb	$⊢ z = w \to (\exists v \in A \exists b \in B z = v b \leftrightarrow \exists a \in A \exists b \in B w = a b)$
69	38 68 1	elab2	$⊢ w \in C \leftrightarrow \exists a \in A \exists b \in B w = a b$
70	62 69	sylibr	$⊢ (a \in A \land \exists b \in B w = a b) \to w \in C$
71	70	ex	$⊢ a \in A \to (\exists b \in B w = a b \to w \in C)$
72	1 2	supmullem2	$⊢ φ \to (C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x)$
73		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 ℝ <)$
74	73	ex	$⊢ (C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \to (w \in C \to w \leq sup (C ℝ <))$
75	72 74	syl	$⊢ φ \to (w \in C \to w \leq sup (C ℝ <))$
76	71 75	sylan9r	$⊢ (φ \land a \in A) \to (\exists b \in B w = a b \to w \leq sup (C ℝ <))$
77	61 76	syl5bi	$⊢ (φ \land a \in A) \to (w \in \{z \| \exists b \in B z = a b\} \to w \leq sup (C ℝ <))$
78	77	ralrimiv	$⊢ (φ \land a \in A) \to \forall w \in \{z \| \exists b \in B z = a b\} w \leq sup (C ℝ <)$
79	44	adantr	$⊢ ((φ \land a \in A) \land b \in B) \to a \in ℝ$
80	19	adantlr	$⊢ ((φ \land a \in A) \land b \in B) \to b \in ℝ$
81	79 80	remulcld	$⊢ ((φ \land a \in A) \land b \in B) \to a b \in ℝ$
82		eleq1a	$⊢ a b \in ℝ \to (z = a b \to z \in ℝ)$
83	81 82	syl	$⊢ ((φ \land a \in A) \land b \in B) \to (z = a b \to z \in ℝ)$
84	83	rexlimdva	$⊢ (φ \land a \in A) \to (\exists b \in B z = a b \to z \in ℝ)$
85	84	abssdv	$⊢ (φ \land a \in A) \to \{z \| \exists b \in B z = a b\} \subseteq ℝ$
86		ovex	$⊢ a b \in V$
87	86	isseti	$⊢ \exists w w = a b$
88	87	rgenw	$⊢ \forall b \in B \exists w w = a b$
89		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$
90	14 88 89	sylancl	$⊢ φ \to \exists b \in B \exists w w = a b$
91		rexcom4	$⊢ \exists b \in B \exists w w = a b \leftrightarrow \exists w \exists b \in B w = a b$
92	90 91	sylib	$⊢ φ \to \exists w \exists b \in B w = a b$
93	60	cbvexvw	$⊢ \exists z \exists b \in B z = a b \leftrightarrow \exists w \exists b \in B w = a b$
94	92 93	sylibr	$⊢ φ \to \exists z \exists b \in B z = a b$
95		abn0	$⊢ \{z \| \exists b \in B z = a b\} \neq \emptyset \leftrightarrow \exists z \exists b \in B z = a b$
96	94 95	sylibr	$⊢ φ \to \{z \| \exists b \in B z = a b\} \neq \emptyset$
97	96	adantr	$⊢ (φ \land a \in A) \to \{z \| \exists b \in B z = a b\} \neq \emptyset$
98		suprcl	$⊢ (C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \to sup (C ℝ <) \in ℝ$
99	72 98	syl	$⊢ φ \to sup (C ℝ <) \in ℝ$
100	99	adantr	$⊢ (φ \land a \in A) \to sup (C ℝ <) \in ℝ$
101		brralrspcev	$⊢ (sup (C ℝ <) \in ℝ \land \forall w \in \{z \| \exists b \in B z = a b\} w \leq sup (C ℝ <)) \to \exists x \in ℝ \forall w \in \{z \| \exists b \in B z = a b\} w \leq x$
102	100 78 101	syl2anc	$⊢ (φ \land a \in A) \to \exists x \in ℝ \forall w \in \{z \| \exists b \in B z = a b\} w \leq x$
103		suprleub	$⊢ ((\{z \| \exists b \in B z = a b\} \subseteq ℝ \land \{z \| \exists b \in B z = a b\} \neq \emptyset \land \exists x \in ℝ \forall w \in \{z \| \exists b \in B z = a b\} w \leq x) \land sup (C ℝ <) \in ℝ) \to (sup (\{z \| \exists b \in B z = a b\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists b \in B z = a b\} w \leq sup (C ℝ <))$
104	85 97 102 100 103	syl31anc	$⊢ (φ \land a \in A) \to (sup (\{z \| \exists b \in B z = a b\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists b \in B z = a b\} w \leq sup (C ℝ <))$
105	78 104	mpbird	$⊢ (φ \land a \in A) \to sup (\{z \| \exists b \in B z = a b\} ℝ <) \leq sup (C ℝ <)$
106	58 105	eqbrtrd	$⊢ (φ \land a \in A) \to a sup (B ℝ <) \leq sup (C ℝ <)$
107	48 106	eqbrtrd	$⊢ (φ \land a \in A) \to sup (B ℝ <) a \leq sup (C ℝ <)$
108		breq1	$⊢ w = sup (B ℝ <) a \to (w \leq sup (C ℝ <) \leftrightarrow sup (B ℝ <) a \leq sup (C ℝ <))$
109	107 108	syl5ibrcom	$⊢ (φ \land a \in A) \to (w = sup (B ℝ <) a \to w \leq sup (C ℝ <))$
110	109	rexlimdva	$⊢ φ \to (\exists a \in A w = sup (B ℝ <) a \to w \leq sup (C ℝ <))$
111	41 110	syl5bi	$⊢ φ \to (w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} \to w \leq sup (C ℝ <))$
112	111	ralrimiv	$⊢ φ \to \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq sup (C ℝ <)$
113	42 44	remulcld	$⊢ (φ \land a \in A) \to sup (B ℝ <) a \in ℝ$
114		eleq1a	$⊢ sup (B ℝ <) a \in ℝ \to (z = sup (B ℝ <) a \to z \in ℝ)$
115	113 114	syl	$⊢ (φ \land a \in A) \to (z = sup (B ℝ <) a \to z \in ℝ)$
116	115	rexlimdva	$⊢ φ \to (\exists a \in A z = sup (B ℝ <) a \to z \in ℝ)$
117	116	abssdv	$⊢ φ \to \{z \| \exists a \in A z = sup (B ℝ <) a\} \subseteq ℝ$
118	3	simp2d	$⊢ φ \to A \neq \emptyset$
119		ovex	$⊢ sup (B ℝ <) a \in V$
120	119	isseti	$⊢ \exists z z = sup (B ℝ <) a$
121	120	rgenw	$⊢ \forall a \in A \exists z z = sup (B ℝ <) a$
122		r19.2z	$⊢ (A \neq \emptyset \land \forall a \in A \exists z z = sup (B ℝ <) a) \to \exists a \in A \exists z z = sup (B ℝ <) a$
123	118 121 122	sylancl	$⊢ φ \to \exists a \in A \exists z z = sup (B ℝ <) a$
124		rexcom4	$⊢ \exists a \in A \exists z z = sup (B ℝ <) a \leftrightarrow \exists z \exists a \in A z = sup (B ℝ <) a$
125	123 124	sylib	$⊢ φ \to \exists z \exists a \in A z = sup (B ℝ <) a$
126		abn0	$⊢ \{z \| \exists a \in A z = sup (B ℝ <) a\} \neq \emptyset \leftrightarrow \exists z \exists a \in A z = sup (B ℝ <) a$
127	125 126	sylibr	$⊢ φ \to \{z \| \exists a \in A z = sup (B ℝ <) a\} \neq \emptyset$
128		brralrspcev	$⊢ (sup (C ℝ <) \in ℝ \land \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq sup (C ℝ <)) \to \exists x \in ℝ \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq x$
129	99 112 128	syl2anc	$⊢ φ \to \exists x \in ℝ \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq x$
130		suprleub	$⊢ ((\{z \| \exists a \in A z = sup (B ℝ <) a\} \subseteq ℝ \land \{z \| \exists a \in A z = sup (B ℝ <) a\} \neq \emptyset \land \exists x \in ℝ \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq x) \land sup (C ℝ <) \in ℝ) \to (sup (\{z \| \exists a \in A z = sup (B ℝ <) a\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq sup (C ℝ <))$
131	117 127 129 99 130	syl31anc	$⊢ φ \to (sup (\{z \| \exists a \in A z = sup (B ℝ <) a\} ℝ <) \leq sup (C ℝ <) \leftrightarrow \forall w \in \{z \| \exists a \in A z = sup (B ℝ <) a\} w \leq sup (C ℝ <))$
132	112 131	mpbird	$⊢ φ \to sup (\{z \| \exists a \in A z = sup (B ℝ <) a\} ℝ <) \leq sup (C ℝ <)$
133	37 132	eqbrtrd	$⊢ φ \to sup (A ℝ <) sup (B ℝ <) \leq sup (C ℝ <)$
134	1 2	supmullem1	$⊢ φ \to \forall w \in C w \leq sup (A ℝ <) sup (B ℝ <)$
135	5 8	remulcld	$⊢ φ \to sup (A ℝ <) sup (B ℝ <) \in ℝ$
136		suprleub	$⊢ ((C \subseteq ℝ \land C \neq \emptyset \land \exists x \in ℝ \forall w \in C w \leq x) \land sup (A ℝ <) sup (B ℝ <) \in ℝ) \to (sup (C ℝ <) \leq sup (A ℝ <) sup (B ℝ <) \leftrightarrow \forall w \in C w \leq sup (A ℝ <) sup (B ℝ <))$
137	72 135 136	syl2anc	$⊢ φ \to (sup (C ℝ <) \leq sup (A ℝ <) sup (B ℝ <) \leftrightarrow \forall w \in C w \leq sup (A ℝ <) sup (B ℝ <))$
138	134 137	mpbird	$⊢ φ \to sup (C ℝ <) \leq sup (A ℝ <) sup (B ℝ <)$
139	135 99	letri3d	$⊢ φ \to (sup (A ℝ <) sup (B ℝ <) = sup (C ℝ <) \leftrightarrow (sup (A ℝ <) sup (B ℝ <) \leq sup (C ℝ <) \land sup (C ℝ <) \leq sup (A ℝ <) sup (B ℝ <)))$
140	133 138 139	mpbir2and	$⊢ φ \to sup (A ℝ <) sup (B ℝ <) = sup (C ℝ <)$

Metamath Proof Explorer

Theorem supmul

Proof