Metamath Proof Explorer

Theorem 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 ⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) }
supmul.2 ⊢ ( 𝜑 ↔ ( ( ∀ 𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 0 ≤ 𝑥 ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ) )
Assertion supmul ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) · sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) )

Proof

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