Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smfmullem4 Structured version   Visualization version   GIF version

Theorem smfmullem4 39483
Description: The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
smfmullem4.x 𝑥𝜑
smfmullem4.s (𝜑𝑆 ∈ SAlg)
smfmullem4.a (𝜑𝐴𝑉)
smfmullem4.b ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
smfmullem4.d ((𝜑𝑥𝐶) → 𝐷 ∈ ℝ)
smfmullem4.m (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
smfmullem4.n (𝜑 → (𝑥𝐶𝐷) ∈ (SMblFn‘𝑆))
smfmullem4.r (𝜑𝑅 ∈ ℝ)
smfmullem4.k 𝐾 = {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅}
smfmullem4.e 𝐸 = (𝑞𝐾 ↦ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
Assertion
Ref Expression
smfmullem4 (𝜑 → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ∈ (𝑆t (𝐴𝐶)))
Distinct variable groups:   𝐴,𝑞,𝑢,𝑣,𝑥   𝐵,𝑞,𝑢,𝑣   𝐶,𝑞,𝑢,𝑣,𝑥   𝐷,𝑞,𝑢,𝑣   𝐾,𝑞,𝑥   𝑅,𝑞,𝑢,𝑣   𝑆,𝑞   𝜑,𝑞,𝑢,𝑣
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐷(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑣,𝑢)   𝐸(𝑥,𝑣,𝑢,𝑞)   𝐾(𝑣,𝑢)   𝑉(𝑥,𝑣,𝑢,𝑞)

Proof of Theorem smfmullem4
StepHypRef Expression
1 smfmullem4.x . . . . 5 𝑥𝜑
2 smfmullem4.r . . . . . . . . . 10 (𝜑𝑅 ∈ ℝ)
323ad2ant1 1074 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝑅 ∈ ℝ)
4 smfmullem4.k . . . . . . . . 9 𝐾 = {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅}
5 inss1 3794 . . . . . . . . . . . . 13 (𝐴𝐶) ⊆ 𝐴
65a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐶) ⊆ 𝐴)
76sselda 3567 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴𝐶)) → 𝑥𝐴)
8 smfmullem4.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
97, 8syldan 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴𝐶)) → 𝐵 ∈ ℝ)
1093adant3 1073 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝐵 ∈ ℝ)
11 elinel2 3761 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴𝐶) → 𝑥𝐶)
1211adantl 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴𝐶)) → 𝑥𝐶)
13 smfmullem4.d . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝐷 ∈ ℝ)
1412, 13syldan 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴𝐶)) → 𝐷 ∈ ℝ)
15143adant3 1073 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝐷 ∈ ℝ)
16 simp3 1055 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → (𝐵 · 𝐷) < 𝑅)
17 eqid 2609 . . . . . . . . 9 ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))) = ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷))))
18 eqid 2609 . . . . . . . . 9 if(1 ≤ ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))), 1, ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷))))) = if(1 ≤ ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))), 1, ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))))
193, 4, 10, 15, 16, 17, 18smfmullem3 39482 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → ∃𝑞𝐾 (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))))
20 rabid 3094 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ↔ (𝑥 ∈ (𝐴𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))))
2120bicomi 212 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝐴𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) ↔ 𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
2221biimpi 204 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝐴𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
2322adantll 745 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐴𝐶)) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
2423adantlr 746 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐴𝐶)) ∧ 𝑞𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
25 smfmullem4.e . . . . . . . . . . . . . . . . 17 𝐸 = (𝑞𝐾 ↦ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
2625a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐸 = (𝑞𝐾 ↦ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}))
27 inrab 3857 . . . . . . . . . . . . . . . . . 18 ({𝑥 ∈ (𝐴𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∩ {𝑥 ∈ (𝐴𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))}) = {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}
28 smfmullem4.s . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 ∈ SAlg)
29 smfmullem4.a . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐴𝑉)
3029, 6ssexd 4728 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴𝐶) ∈ V)
31 eqid 2609 . . . . . . . . . . . . . . . . . . . . 21 (𝑆t (𝐴𝐶)) = (𝑆t (𝐴𝐶))
3228, 30, 31subsalsal 39057 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆t (𝐴𝐶)) ∈ SAlg)
3332adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑞𝐾) → (𝑆t (𝐴𝐶)) ∈ SAlg)
34 nfv 1829 . . . . . . . . . . . . . . . . . . . . 21 𝑥 𝑞𝐾
351, 34nfan 1815 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝜑𝑞𝐾)
3628adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → 𝑆 ∈ SAlg)
3730adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝐴𝐶) ∈ V)
389adantlr 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐴𝐶)) → 𝐵 ∈ ℝ)
39 smfmullem4.m . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
4028, 39, 6sssmfmpt 39441 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥 ∈ (𝐴𝐶) ↦ 𝐵) ∈ (SMblFn‘𝑆))
4140adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝑥 ∈ (𝐴𝐶) ↦ 𝐵) ∈ (SMblFn‘𝑆))
42 ssrab2 3649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} ⊆ (ℚ ↑𝑚 (0...3))
434, 42eqsstri 3597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐾 ⊆ (ℚ ↑𝑚 (0...3))
44 reex 9883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ∈ V
45 qssre 11630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℚ ⊆ ℝ
46 mapss 7763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((ℝ ∈ V ∧ ℚ ⊆ ℝ) → (ℚ ↑𝑚 (0...3)) ⊆ (ℝ ↑𝑚 (0...3)))
4744, 45, 46mp2an 703 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ℚ ↑𝑚 (0...3)) ⊆ (ℝ ↑𝑚 (0...3))
4843, 47sstri 3576 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐾 ⊆ (ℝ ↑𝑚 (0...3))
49 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝐾𝑞𝐾)
5048, 49sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞𝐾𝑞 ∈ (ℝ ↑𝑚 (0...3)))
5144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝐾 → ℝ ∈ V)
52 ovex 6555 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0...3) ∈ V
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝐾 → (0...3) ∈ V)
5451, 53elmapd 7735 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞𝐾 → (𝑞 ∈ (ℝ ↑𝑚 (0...3)) ↔ 𝑞:(0...3)⟶ℝ))
5550, 54mpbid 220 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝐾𝑞:(0...3)⟶ℝ)
56 0z 11221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℤ
57 3z 11243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3 ∈ ℤ
58 0re 9896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ ℝ
59 3re 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 ∈ ℝ
60 3pos 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 < 3
6158, 59, 60ltleii 10011 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ 3
6256, 57, 613pm3.2i 1231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ ℤ ∧ 3 ∈ ℤ ∧ 0 ≤ 3)
63 eluz2 11525 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 3 ∈ ℤ ∧ 0 ≤ 3))
6462, 63mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 ∈ (ℤ‘0)
65 eluzfz1 12174 . . . . . . . . . . . . . . . . . . . . . . . . 25 (3 ∈ (ℤ‘0) → 0 ∈ (0...3))
6664, 65ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ (0...3)
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝐾 → 0 ∈ (0...3))
6855, 67ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞𝐾 → (𝑞‘0) ∈ ℝ)
6968adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑞𝐾) → (𝑞‘0) ∈ ℝ)
7069rexrd 9945 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝑞‘0) ∈ ℝ*)
71 0le1 10400 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≤ 1
72 1re 9895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 ∈ ℝ
73 1lt3 11043 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 < 3
7472, 59, 73ltleii 10011 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ≤ 3
7571, 74pm3.2i 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ≤ 1 ∧ 1 ≤ 3)
76 1z 11240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℤ
77 elfz 12158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) → (1 ∈ (0...3) ↔ (0 ≤ 1 ∧ 1 ≤ 3)))
7876, 56, 57, 77mp3an 1415 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (0...3) ↔ (0 ≤ 1 ∧ 1 ≤ 3))
7975, 78mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ (0...3)
8079a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝐾 → 1 ∈ (0...3))
8155, 80ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞𝐾 → (𝑞‘1) ∈ ℝ)
8281adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑞𝐾) → (𝑞‘1) ∈ ℝ)
8382rexrd 9945 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝑞‘1) ∈ ℝ*)
8435, 36, 37, 38, 41, 70, 83smfpimioompt 39475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑞𝐾) → {𝑥 ∈ (𝐴𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∈ (𝑆t (𝐴𝐶)))
8514adantlr 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐴𝐶)) → 𝐷 ∈ ℝ)
86 smfmullem4.n . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐶𝐷) ∈ (SMblFn‘𝑆))
871, 12ssdf 38076 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴𝐶) ⊆ 𝐶)
8828, 86, 87sssmfmpt 39441 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥 ∈ (𝐴𝐶) ↦ 𝐷) ∈ (SMblFn‘𝑆))
8988adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝑥 ∈ (𝐴𝐶) ↦ 𝐷) ∈ (SMblFn‘𝑆))
90 0le2 10958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≤ 2
91 2re 10937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ
92 2lt3 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 < 3
9391, 59, 92ltleii 10011 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ≤ 3
9490, 93pm3.2i 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ≤ 2 ∧ 2 ≤ 3)
95 2z 11242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℤ
96 elfz 12158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) → (2 ∈ (0...3) ↔ (0 ≤ 2 ∧ 2 ≤ 3)))
9795, 56, 57, 96mp3an 1415 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ (0...3) ↔ (0 ≤ 2 ∧ 2 ≤ 3))
9894, 97mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ (0...3)
9998a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝐾 → 2 ∈ (0...3))
10055, 99ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞𝐾 → (𝑞‘2) ∈ ℝ)
101100adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑞𝐾) → (𝑞‘2) ∈ ℝ)
102101rexrd 9945 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝑞‘2) ∈ ℝ*)
103 eluzfz2 12175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (3 ∈ (ℤ‘0) → 3 ∈ (0...3))
10464, 103ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 3 ∈ (0...3)
105104a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝐾 → 3 ∈ (0...3))
10655, 105ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞𝐾 → (𝑞‘3) ∈ ℝ)
107106adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑞𝐾) → (𝑞‘3) ∈ ℝ)
108107rexrd 9945 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑞𝐾) → (𝑞‘3) ∈ ℝ*)
10935, 36, 37, 85, 89, 102, 108smfpimioompt 39475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑞𝐾) → {𝑥 ∈ (𝐴𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))} ∈ (𝑆t (𝐴𝐶)))
11033, 84, 109salincld 39050 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐾) → ({𝑥 ∈ (𝐴𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∩ {𝑥 ∈ (𝐴𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))}) ∈ (𝑆t (𝐴𝐶)))
11127, 110syl5eqelr 2692 . . . . . . . . . . . . . . . . 17 ((𝜑𝑞𝐾) → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ∈ (𝑆t (𝐴𝐶)))
112111elexd 3186 . . . . . . . . . . . . . . . 16 ((𝜑𝑞𝐾) → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ∈ V)
11326, 112fvmpt2d 6187 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐾) → (𝐸𝑞) = {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
114113eqcomd 2615 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐾) → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸𝑞))
115114adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐴𝐶)) ∧ 𝑞𝐾) → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸𝑞))
116115adantr 479 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐴𝐶)) ∧ 𝑞𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸𝑞))
11724, 116eleqtrd 2689 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴𝐶)) ∧ 𝑞𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ (𝐸𝑞))
118117ex 448 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐴𝐶)) ∧ 𝑞𝐾) → ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → 𝑥 ∈ (𝐸𝑞)))
1191183adantl3 1211 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) ∧ 𝑞𝐾) → ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → 𝑥 ∈ (𝐸𝑞)))
120119reximdva 2999 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → (∃𝑞𝐾 (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → ∃𝑞𝐾 𝑥 ∈ (𝐸𝑞)))
12119, 120mpd 15 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → ∃𝑞𝐾 𝑥 ∈ (𝐸𝑞))
122 eliun 4454 . . . . . . 7 (𝑥 𝑞𝐾 (𝐸𝑞) ↔ ∃𝑞𝐾 𝑥 ∈ (𝐸𝑞))
123121, 122sylibr 222 . . . . . 6 ((𝜑𝑥 ∈ (𝐴𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝑥 𝑞𝐾 (𝐸𝑞))
1241233exp 1255 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴𝐶) → ((𝐵 · 𝐷) < 𝑅𝑥 𝑞𝐾 (𝐸𝑞))))
1251, 124ralrimi 2939 . . . 4 (𝜑 → ∀𝑥 ∈ (𝐴𝐶)((𝐵 · 𝐷) < 𝑅𝑥 𝑞𝐾 (𝐸𝑞)))
12634nfci 2740 . . . . . 6 𝑥𝐾
127 nfrab1 3098 . . . . . . . . 9 𝑥{𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}
128126, 127nfmpt 4668 . . . . . . . 8 𝑥(𝑞𝐾 ↦ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
12925, 128nfcxfr 2748 . . . . . . 7 𝑥𝐸
130 nfcv 2750 . . . . . . 7 𝑥𝑞
131129, 130nffv 6095 . . . . . 6 𝑥(𝐸𝑞)
132126, 131nfiun 4478 . . . . 5 𝑥 𝑞𝐾 (𝐸𝑞)
133132rabssf 38137 . . . 4 ({𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ⊆ 𝑞𝐾 (𝐸𝑞) ↔ ∀𝑥 ∈ (𝐴𝐶)((𝐵 · 𝐷) < 𝑅𝑥 𝑞𝐾 (𝐸𝑞)))
134125, 133sylibr 222 . . 3 (𝜑 → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ⊆ 𝑞𝐾 (𝐸𝑞))
135 ssrab2 3649 . . . . . . 7 {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ⊆ (𝐴𝐶)
136113, 135syl6eqss 3617 . . . . . 6 ((𝜑𝑞𝐾) → (𝐸𝑞) ⊆ (𝐴𝐶))
137 simpr 475 . . . . . . . . . . . 12 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → 𝑥 ∈ (𝐸𝑞))
138113adantr 479 . . . . . . . . . . . 12 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → (𝐸𝑞) = {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
139137, 138eleqtrd 2689 . . . . . . . . . . 11 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → 𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})
140 rabidim2 38116 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} → (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))))
141139, 140syl 17 . . . . . . . . . 10 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))))
142141simprd 477 . . . . . . . . 9 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))
143141simpld 473 . . . . . . . . . 10 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)))
14449, 4syl6eleq 2697 . . . . . . . . . . . 12 (𝑞𝐾𝑞 ∈ {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅})
145 rabidim2 38116 . . . . . . . . . . . 12 (𝑞 ∈ {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅)
146144, 145syl 17 . . . . . . . . . . 11 (𝑞𝐾 → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅)
147146ad2antlr 758 . . . . . . . . . 10 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅)
148 oveq1 6534 . . . . . . . . . . . . 13 (𝑢 = 𝐵 → (𝑢 · 𝑣) = (𝐵 · 𝑣))
149148breq1d 4587 . . . . . . . . . . . 12 (𝑢 = 𝐵 → ((𝑢 · 𝑣) < 𝑅 ↔ (𝐵 · 𝑣) < 𝑅))
150149ralbidv 2968 . . . . . . . . . . 11 (𝑢 = 𝐵 → (∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅 ↔ ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅))
151150rspcva 3279 . . . . . . . . . 10 ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) → ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅)
152143, 147, 151syl2anc 690 . . . . . . . . 9 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅)
153 oveq2 6535 . . . . . . . . . . 11 (𝑣 = 𝐷 → (𝐵 · 𝑣) = (𝐵 · 𝐷))
154153breq1d 4587 . . . . . . . . . 10 (𝑣 = 𝐷 → ((𝐵 · 𝑣) < 𝑅 ↔ (𝐵 · 𝐷) < 𝑅))
155154rspcva 3279 . . . . . . . . 9 ((𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)) ∧ ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) → (𝐵 · 𝐷) < 𝑅)
156142, 152, 155syl2anc 690 . . . . . . . 8 (((𝜑𝑞𝐾) ∧ 𝑥 ∈ (𝐸𝑞)) → (𝐵 · 𝐷) < 𝑅)
157156ex 448 . . . . . . 7 ((𝜑𝑞𝐾) → (𝑥 ∈ (𝐸𝑞) → (𝐵 · 𝐷) < 𝑅))
15835, 157ralrimi 2939 . . . . . 6 ((𝜑𝑞𝐾) → ∀𝑥 ∈ (𝐸𝑞)(𝐵 · 𝐷) < 𝑅)
159136, 158jca 552 . . . . 5 ((𝜑𝑞𝐾) → ((𝐸𝑞) ⊆ (𝐴𝐶) ∧ ∀𝑥 ∈ (𝐸𝑞)(𝐵 · 𝐷) < 𝑅))
160 nfcv 2750 . . . . . 6 𝑥(𝐴𝐶)
161131, 160ssrabf 38132 . . . . 5 ((𝐸𝑞) ⊆ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ↔ ((𝐸𝑞) ⊆ (𝐴𝐶) ∧ ∀𝑥 ∈ (𝐸𝑞)(𝐵 · 𝐷) < 𝑅))
162159, 161sylibr 222 . . . 4 ((𝜑𝑞𝐾) → (𝐸𝑞) ⊆ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅})
163162iunssd 38102 . . 3 (𝜑 𝑞𝐾 (𝐸𝑞) ⊆ {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅})
164134, 163eqssd 3584 . 2 (𝜑 → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅} = 𝑞𝐾 (𝐸𝑞))
165 ovex 6555 . . . . . . 7 (ℚ ↑𝑚 (0...3)) ∈ V
166 ssdomg 7864 . . . . . . 7 ((ℚ ↑𝑚 (0...3)) ∈ V → (𝐾 ⊆ (ℚ ↑𝑚 (0...3)) → 𝐾 ≼ (ℚ ↑𝑚 (0...3))))
167165, 166ax-mp 5 . . . . . 6 (𝐾 ⊆ (ℚ ↑𝑚 (0...3)) → 𝐾 ≼ (ℚ ↑𝑚 (0...3)))
16843, 167ax-mp 5 . . . . 5 𝐾 ≼ (ℚ ↑𝑚 (0...3))
169 qct 38323 . . . . . . . 8 ℚ ≼ ω
170169a1i 11 . . . . . . 7 (⊤ → ℚ ≼ ω)
171 fzfid 12589 . . . . . . 7 (⊤ → (0...3) ∈ Fin)
172170, 171mpct 38191 . . . . . 6 (⊤ → (ℚ ↑𝑚 (0...3)) ≼ ω)
173172trud 1483 . . . . 5 (ℚ ↑𝑚 (0...3)) ≼ ω
174 domtr 7872 . . . . 5 ((𝐾 ≼ (ℚ ↑𝑚 (0...3)) ∧ (ℚ ↑𝑚 (0...3)) ≼ ω) → 𝐾 ≼ ω)
175168, 173, 174mp2an 703 . . . 4 𝐾 ≼ ω
176175a1i 11 . . 3 (𝜑𝐾 ≼ ω)
177111, 25fmptd 6277 . . . 4 (𝜑𝐸:𝐾⟶(𝑆t (𝐴𝐶)))
178177ffvelrnda 6252 . . 3 ((𝜑𝑞𝐾) → (𝐸𝑞) ∈ (𝑆t (𝐴𝐶)))
17932, 176, 178saliuncl 39022 . 2 (𝜑 𝑞𝐾 (𝐸𝑞) ∈ (𝑆t (𝐴𝐶)))
180164, 179eqeltrd 2687 1 (𝜑 → {𝑥 ∈ (𝐴𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ∈ (𝑆t (𝐴𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wtru 1475  wnf 1698  wcel 1976  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cin 3538  wss 3539  ifcif 4035   ciun 4449   class class class wbr 4577  cmpt 4637  wf 5786  cfv 5790  (class class class)co 6527  ωcom 6934  𝑚 cmap 7721  cdom 7816  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117   / cdiv 10533  2c2 10917  3c3 10918  cz 11210  cuz 11519  cq 11620  (,)cioo 12002  ...cfz 12152  abscabs 13768  t crest 15850  SAlgcsalg 39008  SMblFncsmblfn 39390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cc 9117  ax-ac2 9145  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-omul 7429  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-acn 8628  df-ac 8799  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-n0 11140  df-z 11211  df-uz 11520  df-q 11621  df-rp 11665  df-ioo 12006  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-seq 12619  df-exp 12678  df-hash 12935  df-word 13100  df-concat 13102  df-s1 13103  df-s2 13390  df-s3 13391  df-s4 13392  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-rest 15852  df-salg 39009  df-smblfn 39391
This theorem is referenced by:  smfmul  39484
  Copyright terms: Public domain W3C validator