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

Theorem stoweidlem48 43091
 Description: This lemma is used to prove that 𝑥 built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < ε on 𝐴. Here 𝑋 is used to represent 𝑥 in the paper, 𝐸 is used to represent ε in the paper, and 𝐷 is used to represent 𝐴 in the paper (because 𝐴 is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem48.1 𝑖𝜑
stoweidlem48.2 𝑡𝜑
stoweidlem48.3 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
stoweidlem48.4 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
stoweidlem48.5 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
stoweidlem48.6 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
stoweidlem48.7 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
stoweidlem48.8 (𝜑𝑀 ∈ ℕ)
stoweidlem48.9 (𝜑𝑊:(1...𝑀)⟶𝑉)
stoweidlem48.10 (𝜑𝑈:(1...𝑀)⟶𝑌)
stoweidlem48.11 (𝜑𝐷 ran 𝑊)
stoweidlem48.12 (𝜑𝐷𝑇)
stoweidlem48.13 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < 𝐸)
stoweidlem48.14 (𝜑𝑇 ∈ V)
stoweidlem48.15 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
stoweidlem48.16 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem48.17 (𝜑𝐸 ∈ ℝ+)
Assertion
Ref Expression
stoweidlem48 (𝜑 → ∀𝑡𝐷 (𝑋𝑡) < 𝐸)
Distinct variable groups:   𝑓,𝑔,,𝑡,𝐴   𝑓,𝑖,𝑇,,𝑡   𝑓,𝐹,𝑔   𝑓,𝑀,𝑔   𝑈,𝑓,𝑔,,𝑡   𝑓,𝑌,𝑔   𝜑,𝑓,𝑔   𝑇,𝑔   𝐷,𝑖   𝑖,𝐸   𝑖,𝑀   𝑈,𝑖   𝑖,𝑊
Allowed substitution hints:   𝜑(𝑡,,𝑖)   𝐴(𝑖)   𝐷(𝑡,𝑓,𝑔,)   𝑃(𝑡,𝑓,𝑔,,𝑖)   𝐸(𝑡,𝑓,𝑔,)   𝐹(𝑡,,𝑖)   𝑀(𝑡,)   𝑉(𝑡,𝑓,𝑔,,𝑖)   𝑊(𝑡,𝑓,𝑔,)   𝑋(𝑡,𝑓,𝑔,,𝑖)   𝑌(𝑡,,𝑖)   𝑍(𝑡,𝑓,𝑔,,𝑖)

Proof of Theorem stoweidlem48
Dummy variables 𝑗 𝑘 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem48.2 . 2 𝑡𝜑
2 stoweidlem48.12 . . . . . 6 (𝜑𝐷𝑇)
32sselda 3894 . . . . 5 ((𝜑𝑡𝐷) → 𝑡𝑇)
4 stoweidlem48.1 . . . . . 6 𝑖𝜑
5 stoweidlem48.3 . . . . . . 7 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
6 nfra1 3147 . . . . . . . 8 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
7 nfcv 2919 . . . . . . . 8 𝑡𝐴
86, 7nfrabw 3303 . . . . . . 7 𝑡{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
95, 8nfcxfr 2917 . . . . . 6 𝑡𝑌
10 stoweidlem48.4 . . . . . 6 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
11 stoweidlem48.5 . . . . . 6 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
12 stoweidlem48.6 . . . . . 6 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
13 stoweidlem48.7 . . . . . 6 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
14 stoweidlem48.14 . . . . . 6 (𝜑𝑇 ∈ V)
15 stoweidlem48.8 . . . . . 6 (𝜑𝑀 ∈ ℕ)
16 stoweidlem48.10 . . . . . 6 (𝜑𝑈:(1...𝑀)⟶𝑌)
175eleq2i 2843 . . . . . . . . 9 (𝑓𝑌𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
18 fveq1 6662 . . . . . . . . . . . . 13 ( = 𝑓 → (𝑡) = (𝑓𝑡))
1918breq2d 5048 . . . . . . . . . . . 12 ( = 𝑓 → (0 ≤ (𝑡) ↔ 0 ≤ (𝑓𝑡)))
2018breq1d 5046 . . . . . . . . . . . 12 ( = 𝑓 → ((𝑡) ≤ 1 ↔ (𝑓𝑡) ≤ 1))
2119, 20anbi12d 633 . . . . . . . . . . 11 ( = 𝑓 → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2221ralbidv 3126 . . . . . . . . . 10 ( = 𝑓 → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2322elrab 3604 . . . . . . . . 9 (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↔ (𝑓𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2417, 23sylbb 222 . . . . . . . 8 (𝑓𝑌 → (𝑓𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2524simpld 498 . . . . . . 7 (𝑓𝑌𝑓𝐴)
26 stoweidlem48.15 . . . . . . 7 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
2725, 26sylan2 595 . . . . . 6 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
28 eqid 2758 . . . . . . 7 (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) = (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))
29 stoweidlem48.16 . . . . . . 7 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
301, 5, 28, 26, 29stoweidlem16 43059 . . . . . 6 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
314, 9, 10, 11, 12, 13, 14, 15, 16, 27, 30fmuldfeq 42626 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
323, 31syldan 594 . . . 4 ((𝜑𝑡𝐷) → (𝑋𝑡) = (𝑍𝑡))
33 elnnuz 12335 . . . . . . . . 9 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
3415, 33sylib 221 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘1))
3534adantr 484 . . . . . . 7 ((𝜑𝑡𝐷) → 𝑀 ∈ (ℤ‘1))
36 nfv 1915 . . . . . . . . . . . 12 𝑖 𝑡𝑇
374, 36nfan 1900 . . . . . . . . . . 11 𝑖(𝜑𝑡𝑇)
3816ffvelrnda 6848 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
39 fveq1 6662 . . . . . . . . . . . . . . . . . . . 20 ( = (𝑈𝑖) → (𝑡) = ((𝑈𝑖)‘𝑡))
4039breq2d 5048 . . . . . . . . . . . . . . . . . . 19 ( = (𝑈𝑖) → (0 ≤ (𝑡) ↔ 0 ≤ ((𝑈𝑖)‘𝑡)))
4139breq1d 5046 . . . . . . . . . . . . . . . . . . 19 ( = (𝑈𝑖) → ((𝑡) ≤ 1 ↔ ((𝑈𝑖)‘𝑡) ≤ 1))
4240, 41anbi12d 633 . . . . . . . . . . . . . . . . . 18 ( = (𝑈𝑖) → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4342ralbidv 3126 . . . . . . . . . . . . . . . . 17 ( = (𝑈𝑖) → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4443, 5elrab2 3607 . . . . . . . . . . . . . . . 16 ((𝑈𝑖) ∈ 𝑌 ↔ ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4538, 44sylib 221 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4645simpld 498 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝐴)
47 simpl 486 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
4847, 46jca 515 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝐴))
49 eleq1 2839 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑈𝑖) → (𝑓𝐴 ↔ (𝑈𝑖) ∈ 𝐴))
5049anbi2d 631 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝐴) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝐴)))
51 feq1 6484 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
5250, 51imbi12d 348 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ)))
5352, 26vtoclg 3487 . . . . . . . . . . . . . 14 ((𝑈𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ))
5446, 48, 53sylc 65 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5554adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
56 simplr 768 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
5755, 56ffvelrnd 6849 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
58 eqid 2758 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
5937, 57, 58fmptdf 6878 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ)
60 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑡𝑇)
61 ovex 7189 . . . . . . . . . . . . 13 (1...𝑀) ∈ V
62 mptexg 6981 . . . . . . . . . . . . 13 ((1...𝑀) ∈ V → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
6361, 62mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
6412fvmpt2 6775 . . . . . . . . . . . 12 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6560, 63, 64syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6665feq1d 6488 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐹𝑡):(1...𝑀)⟶ℝ ↔ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ))
6759, 66mpbird 260 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐹𝑡):(1...𝑀)⟶ℝ)
683, 67syldan 594 . . . . . . . 8 ((𝜑𝑡𝐷) → (𝐹𝑡):(1...𝑀)⟶ℝ)
6968ffvelrnda 6848 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
70 remulcl 10673 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑘 · 𝑗) ∈ ℝ)
7170adantl 485 . . . . . . 7 (((𝜑𝑡𝐷) ∧ (𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑘 · 𝑗) ∈ ℝ)
7235, 69, 71seqcl 13453 . . . . . 6 ((𝜑𝑡𝐷) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
7313fvmpt2 6775 . . . . . 6 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
743, 72, 73syl2anc 587 . . . . 5 ((𝜑𝑡𝐷) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
75 nfcv 2919 . . . . . . . . 9 𝑖𝑇
76 nfmpt1 5134 . . . . . . . . 9 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
7775, 76nfmpt 5133 . . . . . . . 8 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
7812, 77nfcxfr 2917 . . . . . . 7 𝑖𝐹
79 nfcv 2919 . . . . . . 7 𝑖𝑡
8078, 79nffv 6673 . . . . . 6 𝑖(𝐹𝑡)
81 nfv 1915 . . . . . . 7 𝑖 𝑡𝐷
824, 81nfan 1900 . . . . . 6 𝑖(𝜑𝑡𝐷)
83 nfcv 2919 . . . . . 6 𝑗seq1( · , (𝐹𝑡))
84 eqid 2758 . . . . . 6 seq1( · , (𝐹𝑡)) = seq1( · , (𝐹𝑡))
8515adantr 484 . . . . . 6 ((𝜑𝑡𝐷) → 𝑀 ∈ ℕ)
86 simpll 766 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
87 simpr 488 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
883adantr 484 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
8945simprd 499 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1))
9089r19.21bi 3137 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1))
9190simpld 498 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → 0 ≤ ((𝑈𝑖)‘𝑡))
9286, 87, 88, 91syl21anc 836 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝑈𝑖)‘𝑡))
9365fveq1d 6665 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
9486, 88, 93syl2anc 587 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
9586, 88, 87, 57syl21anc 836 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
9658fvmpt2 6775 . . . . . . . . 9 ((𝑖 ∈ (1...𝑀) ∧ ((𝑈𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
9787, 95, 96syl2anc 587 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
9894, 97eqtrd 2793 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡))
9992, 98breqtrrd 5064 . . . . . 6 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝐹𝑡)‘𝑖))
10090simprd 499 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → ((𝑈𝑖)‘𝑡) ≤ 1)
10186, 87, 88, 100syl21anc 836 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ≤ 1)
10298, 101eqbrtrd 5058 . . . . . 6 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ≤ 1)
103 stoweidlem48.17 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
104103adantr 484 . . . . . 6 ((𝜑𝑡𝐷) → 𝐸 ∈ ℝ+)
105 stoweidlem48.11 . . . . . . . . . . 11 (𝜑𝐷 ran 𝑊)
106105sselda 3894 . . . . . . . . . 10 ((𝜑𝑡𝐷) → 𝑡 ran 𝑊)
107 eluni 4804 . . . . . . . . . 10 (𝑡 ran 𝑊 ↔ ∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊))
108106, 107sylib 221 . . . . . . . . 9 ((𝜑𝑡𝐷) → ∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊))
109 stoweidlem48.9 . . . . . . . . . . . . . . . 16 (𝜑𝑊:(1...𝑀)⟶𝑉)
110 ffn 6503 . . . . . . . . . . . . . . . 16 (𝑊:(1...𝑀)⟶𝑉𝑊 Fn (1...𝑀))
111 fvelrnb 6719 . . . . . . . . . . . . . . . 16 (𝑊 Fn (1...𝑀) → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤))
112109, 110, 1113syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤))
113112biimpa 480 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤)
114113adantrl 715 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤)
115 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → 𝑡𝑤)
116 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → (𝑊𝑗) = 𝑤)
117115, 116eleqtrrd 2855 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → 𝑡 ∈ (𝑊𝑗))
118117ex 416 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑤) → ((𝑊𝑗) = 𝑤𝑡 ∈ (𝑊𝑗)))
119118reximdv 3197 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑤) → (∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
120119adantrr 716 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → (∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
121114, 120mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗))
122121ex 416 . . . . . . . . . . 11 (𝜑 → ((𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
123122exlimdv 1934 . . . . . . . . . 10 (𝜑 → (∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
124123adantr 484 . . . . . . . . 9 ((𝜑𝑡𝐷) → (∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
125108, 124mpd 15 . . . . . . . 8 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗))
126 simplll 774 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝜑)
127 simplr 768 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝑗 ∈ (1...𝑀))
128 simpr 488 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝑡 ∈ (𝑊𝑗))
129 nfv 1915 . . . . . . . . . . . . . 14 𝑖 𝑗 ∈ (1...𝑀)
130 nfv 1915 . . . . . . . . . . . . . 14 𝑖 𝑡 ∈ (𝑊𝑗)
1314, 129, 130nf3an 1902 . . . . . . . . . . . . 13 𝑖(𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗))
132 nfv 1915 . . . . . . . . . . . . 13 𝑖((𝑈𝑗)‘𝑡) < 𝐸
133131, 132nfim 1897 . . . . . . . . . . . 12 𝑖((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
134 eleq1 2839 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑖 ∈ (1...𝑀) ↔ 𝑗 ∈ (1...𝑀)))
135 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → (𝑊𝑖) = (𝑊𝑗))
136135eleq2d 2837 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑡 ∈ (𝑊𝑖) ↔ 𝑡 ∈ (𝑊𝑗)))
137134, 1363anbi23d 1436 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) ↔ (𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗))))
138 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → (𝑈𝑖) = (𝑈𝑗))
139138fveq1d 6665 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → ((𝑈𝑖)‘𝑡) = ((𝑈𝑗)‘𝑡))
140139breq1d 5046 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝑈𝑖)‘𝑡) < 𝐸 ↔ ((𝑈𝑗)‘𝑡) < 𝐸))
141137, 140imbi12d 348 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸) ↔ ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)))
142 stoweidlem48.13 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < 𝐸)
143142r19.21bi 3137 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
1441433impa 1107 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
145133, 141, 144chvarfv 2240 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
146126, 127, 128, 145syl3anc 1368 . . . . . . . . . 10 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
147146ex 416 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (𝑡 ∈ (𝑊𝑗) → ((𝑈𝑗)‘𝑡) < 𝐸))
148147reximdva 3198 . . . . . . . 8 ((𝜑𝑡𝐷) → (∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗) → ∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸))
149125, 148mpd 15 . . . . . . 7 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸)
15082, 129nfan 1900 . . . . . . . . . . . 12 𝑖((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀))
151 nfcv 2919 . . . . . . . . . . . . . 14 𝑖𝑗
15280, 151nffv 6673 . . . . . . . . . . . . 13 𝑖((𝐹𝑡)‘𝑗)
153152nfeq1 2934 . . . . . . . . . . . 12 𝑖((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡)
154150, 153nfim 1897 . . . . . . . . . . 11 𝑖(((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))
155134anbi2d 631 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀))))
156 fveq2 6663 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑗))
157156, 139eqeq12d 2774 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡) ↔ ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡)))
158155, 157imbi12d 348 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡)) ↔ (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))))
159154, 158, 98chvarfv 2240 . . . . . . . . . 10 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))
160159breq1d 5046 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝐹𝑡)‘𝑗) < 𝐸 ↔ ((𝑈𝑗)‘𝑡) < 𝐸))
161160biimprd 251 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝑈𝑗)‘𝑡) < 𝐸 → ((𝐹𝑡)‘𝑗) < 𝐸))
162161reximdva 3198 . . . . . . 7 ((𝜑𝑡𝐷) → (∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸 → ∃𝑗 ∈ (1...𝑀)((𝐹𝑡)‘𝑗) < 𝐸))
163149, 162mpd 15 . . . . . 6 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)((𝐹𝑡)‘𝑗) < 𝐸)
16480, 82, 83, 84, 85, 68, 99, 102, 104, 163fmul01lt1 42629 . . . . 5 ((𝜑𝑡𝐷) → (seq1( · , (𝐹𝑡))‘𝑀) < 𝐸)
16574, 164eqbrtrd 5058 . . . 4 ((𝜑𝑡𝐷) → (𝑍𝑡) < 𝐸)
16632, 165eqbrtrd 5058 . . 3 ((𝜑𝑡𝐷) → (𝑋𝑡) < 𝐸)
167166ex 416 . 2 (𝜑 → (𝑡𝐷 → (𝑋𝑡) < 𝐸))
1681, 167ralrimi 3144 1 (𝜑 → ∀𝑡𝐷 (𝑋𝑡) < 𝐸)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ⊆ wss 3860  ∪ cuni 4801   class class class wbr 5036   ↦ cmpt 5116  ran crn 5529   Fn wfn 6335  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156   ∈ cmpo 7158  ℝcr 10587  0cc0 10588  1c1 10589   · cmul 10593   < clt 10726   ≤ cle 10727  ℕcn 11687  ℤ≥cuz 12295  ℝ+crp 12443  ...cfz 12952  seqcseq 13431 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-er 8305  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-nn 11688  df-n0 11948  df-z 12034  df-uz 12296  df-rp 12444  df-fz 12953  df-fzo 13096  df-seq 13432 This theorem is referenced by:  stoweidlem51  43094
 Copyright terms: Public domain W3C validator