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

Theorem stoweidlem48 42210
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 3964 . . . . 5 ((𝜑𝑡𝐷) → 𝑡𝑇)
4 stoweidlem48.1 . . . . . 6 𝑖𝜑
5 stoweidlem48.3 . . . . . . 7 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
6 nfra1 3216 . . . . . . . 8 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
7 nfcv 2974 . . . . . . . 8 𝑡𝐴
86, 7nfrabw 3383 . . . . . . 7 𝑡{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
95, 8nfcxfr 2972 . . . . . 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 2901 . . . . . . . . 9 (𝑓𝑌𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
18 fveq1 6662 . . . . . . . . . . . . 13 ( = 𝑓 → (𝑡) = (𝑓𝑡))
1918breq2d 5069 . . . . . . . . . . . 12 ( = 𝑓 → (0 ≤ (𝑡) ↔ 0 ≤ (𝑓𝑡)))
2018breq1d 5067 . . . . . . . . . . . 12 ( = 𝑓 → ((𝑡) ≤ 1 ↔ (𝑓𝑡) ≤ 1))
2119, 20anbi12d 630 . . . . . . . . . . 11 ( = 𝑓 → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2221ralbidv 3194 . . . . . . . . . 10 ( = 𝑓 → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2322elrab 3677 . . . . . . . . 9 (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↔ (𝑓𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2417, 23sylbb 220 . . . . . . . 8 (𝑓𝑌 → (𝑓𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2524simpld 495 . . . . . . 7 (𝑓𝑌𝑓𝐴)
26 stoweidlem48.15 . . . . . . 7 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
2725, 26sylan2 592 . . . . . 6 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
28 eqid 2818 . . . . . . 7 (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) = (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))
29 stoweidlem48.16 . . . . . . 7 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
301, 5, 28, 26, 29stoweidlem16 42178 . . . . . 6 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
314, 9, 10, 11, 12, 13, 14, 15, 16, 27, 30fmuldfeq 41740 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
323, 31syldan 591 . . . 4 ((𝜑𝑡𝐷) → (𝑋𝑡) = (𝑍𝑡))
33 elnnuz 12270 . . . . . . . . 9 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
3415, 33sylib 219 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘1))
3534adantr 481 . . . . . . 7 ((𝜑𝑡𝐷) → 𝑀 ∈ (ℤ‘1))
36 nfv 1906 . . . . . . . . . . . 12 𝑖 𝑡𝑇
374, 36nfan 1891 . . . . . . . . . . 11 𝑖(𝜑𝑡𝑇)
3816ffvelrnda 6843 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
39 fveq1 6662 . . . . . . . . . . . . . . . . . . . 20 ( = (𝑈𝑖) → (𝑡) = ((𝑈𝑖)‘𝑡))
4039breq2d 5069 . . . . . . . . . . . . . . . . . . 19 ( = (𝑈𝑖) → (0 ≤ (𝑡) ↔ 0 ≤ ((𝑈𝑖)‘𝑡)))
4139breq1d 5067 . . . . . . . . . . . . . . . . . . 19 ( = (𝑈𝑖) → ((𝑡) ≤ 1 ↔ ((𝑈𝑖)‘𝑡) ≤ 1))
4240, 41anbi12d 630 . . . . . . . . . . . . . . . . . 18 ( = (𝑈𝑖) → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4342ralbidv 3194 . . . . . . . . . . . . . . . . 17 ( = (𝑈𝑖) → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4443, 5elrab2 3680 . . . . . . . . . . . . . . . 16 ((𝑈𝑖) ∈ 𝑌 ↔ ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4538, 44sylib 219 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4645simpld 495 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝐴)
47 simpl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
4847, 46jca 512 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝐴))
49 eleq1 2897 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑈𝑖) → (𝑓𝐴 ↔ (𝑈𝑖) ∈ 𝐴))
5049anbi2d 628 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝐴) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝐴)))
51 feq1 6488 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
5250, 51imbi12d 346 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ)))
5352, 26vtoclg 3565 . . . . . . . . . . . . . 14 ((𝑈𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ))
5446, 48, 53sylc 65 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5554adantlr 711 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
56 simplr 765 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
5755, 56ffvelrnd 6844 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
58 eqid 2818 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
5937, 57, 58fmptdf 6873 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ)
60 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑡𝑇)
61 ovex 7178 . . . . . . . . . . . . 13 (1...𝑀) ∈ V
62 mptexg 6975 . . . . . . . . . . . . 13 ((1...𝑀) ∈ V → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
6361, 62mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
6412fvmpt2 6771 . . . . . . . . . . . 12 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6560, 63, 64syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6665feq1d 6492 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐹𝑡):(1...𝑀)⟶ℝ ↔ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ))
6759, 66mpbird 258 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐹𝑡):(1...𝑀)⟶ℝ)
683, 67syldan 591 . . . . . . . 8 ((𝜑𝑡𝐷) → (𝐹𝑡):(1...𝑀)⟶ℝ)
6968ffvelrnda 6843 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
70 remulcl 10610 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑘 · 𝑗) ∈ ℝ)
7170adantl 482 . . . . . . 7 (((𝜑𝑡𝐷) ∧ (𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑘 · 𝑗) ∈ ℝ)
7235, 69, 71seqcl 13378 . . . . . 6 ((𝜑𝑡𝐷) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
7313fvmpt2 6771 . . . . . 6 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
743, 72, 73syl2anc 584 . . . . 5 ((𝜑𝑡𝐷) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
75 nfcv 2974 . . . . . . . . 9 𝑖𝑇
76 nfmpt1 5155 . . . . . . . . 9 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
7775, 76nfmpt 5154 . . . . . . . 8 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
7812, 77nfcxfr 2972 . . . . . . 7 𝑖𝐹
79 nfcv 2974 . . . . . . 7 𝑖𝑡
8078, 79nffv 6673 . . . . . 6 𝑖(𝐹𝑡)
81 nfv 1906 . . . . . . 7 𝑖 𝑡𝐷
824, 81nfan 1891 . . . . . 6 𝑖(𝜑𝑡𝐷)
83 nfcv 2974 . . . . . 6 𝑗seq1( · , (𝐹𝑡))
84 eqid 2818 . . . . . 6 seq1( · , (𝐹𝑡)) = seq1( · , (𝐹𝑡))
8515adantr 481 . . . . . 6 ((𝜑𝑡𝐷) → 𝑀 ∈ ℕ)
86 simpll 763 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
87 simpr 485 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
883adantr 481 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
8945simprd 496 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1))
9089r19.21bi 3205 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1))
9190simpld 495 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → 0 ≤ ((𝑈𝑖)‘𝑡))
9286, 87, 88, 91syl21anc 833 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝑈𝑖)‘𝑡))
9365fveq1d 6665 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
9486, 88, 93syl2anc 584 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
9586, 88, 87, 57syl21anc 833 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
9658fvmpt2 6771 . . . . . . . . 9 ((𝑖 ∈ (1...𝑀) ∧ ((𝑈𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
9787, 95, 96syl2anc 584 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
9894, 97eqtrd 2853 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡))
9992, 98breqtrrd 5085 . . . . . 6 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝐹𝑡)‘𝑖))
10090simprd 496 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → ((𝑈𝑖)‘𝑡) ≤ 1)
10186, 87, 88, 100syl21anc 833 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ≤ 1)
10298, 101eqbrtrd 5079 . . . . . 6 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ≤ 1)
103 stoweidlem48.17 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
104103adantr 481 . . . . . 6 ((𝜑𝑡𝐷) → 𝐸 ∈ ℝ+)
105 stoweidlem48.11 . . . . . . . . . . 11 (𝜑𝐷 ran 𝑊)
106105sselda 3964 . . . . . . . . . 10 ((𝜑𝑡𝐷) → 𝑡 ran 𝑊)
107 eluni 4833 . . . . . . . . . 10 (𝑡 ran 𝑊 ↔ ∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊))
108106, 107sylib 219 . . . . . . . . 9 ((𝜑𝑡𝐷) → ∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊))
109 stoweidlem48.9 . . . . . . . . . . . . . . . 16 (𝜑𝑊:(1...𝑀)⟶𝑉)
110 ffn 6507 . . . . . . . . . . . . . . . 16 (𝑊:(1...𝑀)⟶𝑉𝑊 Fn (1...𝑀))
111 fvelrnb 6719 . . . . . . . . . . . . . . . 16 (𝑊 Fn (1...𝑀) → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤))
112109, 110, 1113syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤))
113112biimpa 477 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤)
114113adantrl 712 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤)
115 simplr 765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → 𝑡𝑤)
116 simpr 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → (𝑊𝑗) = 𝑤)
117115, 116eleqtrrd 2913 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → 𝑡 ∈ (𝑊𝑗))
118117ex 413 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑤) → ((𝑊𝑗) = 𝑤𝑡 ∈ (𝑊𝑗)))
119118reximdv 3270 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑤) → (∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
120119adantrr 713 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → (∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
121114, 120mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗))
122121ex 413 . . . . . . . . . . 11 (𝜑 → ((𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
123122exlimdv 1925 . . . . . . . . . 10 (𝜑 → (∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
124123adantr 481 . . . . . . . . 9 ((𝜑𝑡𝐷) → (∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
125108, 124mpd 15 . . . . . . . 8 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗))
126 simplll 771 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝜑)
127 simplr 765 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝑗 ∈ (1...𝑀))
128 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝑡 ∈ (𝑊𝑗))
129 nfv 1906 . . . . . . . . . . . . . 14 𝑖 𝑗 ∈ (1...𝑀)
130 nfv 1906 . . . . . . . . . . . . . 14 𝑖 𝑡 ∈ (𝑊𝑗)
1314, 129, 130nf3an 1893 . . . . . . . . . . . . 13 𝑖(𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗))
132 nfv 1906 . . . . . . . . . . . . 13 𝑖((𝑈𝑗)‘𝑡) < 𝐸
133131, 132nfim 1888 . . . . . . . . . . . 12 𝑖((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
134 eleq1 2897 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑖 ∈ (1...𝑀) ↔ 𝑗 ∈ (1...𝑀)))
135 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → (𝑊𝑖) = (𝑊𝑗))
136135eleq2d 2895 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑡 ∈ (𝑊𝑖) ↔ 𝑡 ∈ (𝑊𝑗)))
137134, 1363anbi23d 1430 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) ↔ (𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗))))
138 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → (𝑈𝑖) = (𝑈𝑗))
139138fveq1d 6665 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → ((𝑈𝑖)‘𝑡) = ((𝑈𝑗)‘𝑡))
140139breq1d 5067 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝑈𝑖)‘𝑡) < 𝐸 ↔ ((𝑈𝑗)‘𝑡) < 𝐸))
141137, 140imbi12d 346 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸) ↔ ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)))
142 stoweidlem48.13 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < 𝐸)
143142r19.21bi 3205 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
1441433impa 1102 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
145133, 141, 144chvarfv 2232 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
146126, 127, 128, 145syl3anc 1363 . . . . . . . . . 10 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
147146ex 413 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (𝑡 ∈ (𝑊𝑗) → ((𝑈𝑗)‘𝑡) < 𝐸))
148147reximdva 3271 . . . . . . . 8 ((𝜑𝑡𝐷) → (∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗) → ∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸))
149125, 148mpd 15 . . . . . . 7 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸)
15082, 129nfan 1891 . . . . . . . . . . . 12 𝑖((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀))
151 nfcv 2974 . . . . . . . . . . . . . 14 𝑖𝑗
15280, 151nffv 6673 . . . . . . . . . . . . 13 𝑖((𝐹𝑡)‘𝑗)
153152nfeq1 2990 . . . . . . . . . . . 12 𝑖((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡)
154150, 153nfim 1888 . . . . . . . . . . 11 𝑖(((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))
155134anbi2d 628 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀))))
156 fveq2 6663 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑗))
157156, 139eqeq12d 2834 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡) ↔ ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡)))
158155, 157imbi12d 346 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡)) ↔ (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))))
159154, 158, 98chvarfv 2232 . . . . . . . . . 10 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))
160159breq1d 5067 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝐹𝑡)‘𝑗) < 𝐸 ↔ ((𝑈𝑗)‘𝑡) < 𝐸))
161160biimprd 249 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝑈𝑗)‘𝑡) < 𝐸 → ((𝐹𝑡)‘𝑗) < 𝐸))
162161reximdva 3271 . . . . . . 7 ((𝜑𝑡𝐷) → (∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸 → ∃𝑗 ∈ (1...𝑀)((𝐹𝑡)‘𝑗) < 𝐸))
163149, 162mpd 15 . . . . . 6 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)((𝐹𝑡)‘𝑗) < 𝐸)
16480, 82, 83, 84, 85, 68, 99, 102, 104, 163fmul01lt1 41743 . . . . 5 ((𝜑𝑡𝐷) → (seq1( · , (𝐹𝑡))‘𝑀) < 𝐸)
16574, 164eqbrtrd 5079 . . . 4 ((𝜑𝑡𝐷) → (𝑍𝑡) < 𝐸)
16632, 165eqbrtrd 5079 . . 3 ((𝜑𝑡𝐷) → (𝑋𝑡) < 𝐸)
167166ex 413 . 2 (𝜑 → (𝑡𝐷 → (𝑋𝑡) < 𝐸))
1681, 167ralrimi 3213 1 (𝜑 → ∀𝑡𝐷 (𝑋𝑡) < 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wnf 1775  wcel 2105  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  wss 3933   cuni 4830   class class class wbr 5057  cmpt 5137  ran crn 5549   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  cr 10524  0cc0 10525  1c1 10526   · cmul 10530   < clt 10663  cle 10664  cn 11626  cuz 12231  +crp 12377  ...cfz 12880  seqcseq 13357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12881  df-fzo 13022  df-seq 13358
This theorem is referenced by:  stoweidlem51  42213
  Copyright terms: Public domain W3C validator