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

Metamath Proof Explorer

Theorem supmullem2

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

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

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 sseld ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ ) )
15 2 simp3bi ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) )
16 15 simp1d ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
17 16 sseld ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ℝ ) )
18 14 17 anim12d ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) )
19 remulcl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 · 𝑏 ) ∈ ℝ )
20 18 19 syl6 ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ ℝ ) )
21 eleq1a ⊢ ( ( 𝑎 · 𝑏 ) ∈ ℝ → ( 𝑤 = ( 𝑎 · 𝑏 ) → 𝑤 ∈ ℝ ) )
22 20 21 syl6 ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑤 = ( 𝑎 · 𝑏 ) → 𝑤 ∈ ℝ ) ) )
23 22 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) → 𝑤 ∈ ℝ ) )
24 11 23 biimtrid ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ ℝ ) )
25 24 ssrdv ⊢ ( 𝜑 → 𝐶 ⊆ ℝ )
26 12 simp2d ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
27 15 simp2d ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
28 ovex ⊢ ( 𝑎 · 𝑏 ) ∈ V
29 28 isseti ⊢ ∃ 𝑤 𝑤 = ( 𝑎 · 𝑏 )
30 29 rgenw ⊢ ∀ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 · 𝑏 )
31 r19.2z ⊢ ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 · 𝑏 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 · 𝑏 ) )
32 27 30 31 sylancl ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 · 𝑏 ) )
33 rexcom4 ⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 · 𝑏 ) ↔ ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
34 32 33 sylib ⊢ ( 𝜑 → ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
35 34 ralrimivw ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
36 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
37 26 35 36 syl2anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
38 rexcom4 ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) ↔ ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
39 37 38 sylib ⊢ ( 𝜑 → ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
40 n0 ⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
41 11 exbii ⊢ ( ∃ 𝑤 𝑤 ∈ 𝐶 ↔ ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
42 40 41 bitri ⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) )
43 39 42 sylibr ⊢ ( 𝜑 → 𝐶 ≠ ∅ )
44 suprcl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
45 12 44 syl ⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
46 suprcl ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
47 15 46 syl ⊢ ( 𝜑 → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
48 45 47 remulcld ⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ∈ ℝ )
49 1 2 supmullem1 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) )
50 brralrspcev ⊢ ( ( ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ∈ ℝ ∧ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 )
51 48 49 50 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 )
52 25 43 51 3jca ⊢ ( 𝜑 → ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 ) )