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	syl5bb	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 · 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 · 𝑏 ) ) )
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	syl5bi	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ ℝ ) )
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	⊢ ( 𝜑 → ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 ) )