Theorem supmullem1

Description: Lemma for supmul . (Contributed by Mario Carneiro, 5-Jul-2013)

	Ref	Expression
Hypotheses	supmul.1	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) }
	supmul.2	⊢ ( 𝜑 ↔ ( ( ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ) )
Assertion	supmullem1	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		supmul.1	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) }
2		supmul.2	⊢ ( 𝜑 ↔ ( ( ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ) )
3		vex	⊢ 𝑤 ∈ V
4		oveq1	⊢ ( 𝑣 = 𝑎 → ( 𝑣 · 𝑏 ) = ( 𝑎 · 𝑏 ) )
5	4	eqeq2d	⊢ ( 𝑣 = 𝑎 → ( 𝑧 = ( 𝑣 · 𝑏 ) ↔ 𝑧 = ( 𝑎 · 𝑏 ) ) )
6	5	rexbidv	⊢ ( 𝑣 = 𝑎 → ( ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 · 𝑏 ) ) )
7	6	cbvrexvw	⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 · 𝑏 ) )
8		eqeq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑎 · 𝑏 ) ↔ 𝑤 = ( 𝑎 · 𝑏 ) ) )
9	8	2rexbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 · 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) ) )
10	7 9	syl5bb	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) ) )
11	3 10 1	elab2	⊢ ( 𝑤 ∈ 𝐶 ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
12	2	simp2bi	⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
13	12	simp1d	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
14	13	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℝ )
15	14	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ ℝ )
16		suprcl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
17	12 16	syl	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
19	2	simp3bi	⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) )
20	19	simp1d	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
21	20	sselda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ℝ )
22	21	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ ℝ )
23		suprcl	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
24	19 23	syl	⊢ ( 𝜑 → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
26		simp1l	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 )
27	2 26	sylbi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 )
28		breq2	⊢ ( 𝑥 = 𝑎 → ( 0 ≤ 𝑥 ↔ 0 ≤ 𝑎 ) )
29	28	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 → ( 𝑎 ∈ 𝐴 → 0 ≤ 𝑎 ) )
30	27 29	syl	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 → 0 ≤ 𝑎 ) )
31	30	imp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 0 ≤ 𝑎 )
32	31	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 0 ≤ 𝑎 )
33		simp1r	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 )
34	2 33	sylbi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 )
35		breq2	⊢ ( 𝑥 = 𝑏 → ( 0 ≤ 𝑥 ↔ 0 ≤ 𝑏 ) )
36	35	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 → ( 𝑏 ∈ 𝐵 → 0 ≤ 𝑏 ) )
37	34 36	syl	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 → 0 ≤ 𝑏 ) )
38	37	imp	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 ≤ 𝑏 )
39	38	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 0 ≤ 𝑏 )
40		suprub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ≤ sup ( 𝐴 , ℝ , < ) )
41	12 40	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ≤ sup ( 𝐴 , ℝ , < ) )
42	41	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ≤ sup ( 𝐴 , ℝ , < ) )
43		suprub	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
44	19 43	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
45	44	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
46	15 18 22 25 32 39 42 45	lemul12ad	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) )
47	46	ex	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) )
48		breq1	⊢ ( 𝑤 = ( 𝑎 · 𝑏 ) → ( 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ↔ ( 𝑎 · 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) )
49	48	biimprcd	⊢ ( ( 𝑎 · 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) → ( 𝑤 = ( 𝑎 · 𝑏 ) → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) )
50	47 49	syl6	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑤 = ( 𝑎 · 𝑏 ) → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) ) )
51	50	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) )
52	11 51	syl5bi	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) )
53	52	ralrimiv	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) )