This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) ) )
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 biimtrid ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) )
53 52 ralrimiv ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) )