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 40834
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 3761 . . . . 5 ((𝜑𝑡𝐷) → 𝑡𝑇)
4 stoweidlem48.1 . . . . . 6 𝑖𝜑
5 stoweidlem48.3 . . . . . . 7 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
6 nfra1 3088 . . . . . . . 8 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
7 nfcv 2907 . . . . . . . 8 𝑡𝐴
86, 7nfrab 3271 . . . . . . 7 𝑡{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
95, 8nfcxfr 2905 . . . . . 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 2836 . . . . . . . . 9 (𝑓𝑌𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
18 fveq1 6374 . . . . . . . . . . . . 13 ( = 𝑓 → (𝑡) = (𝑓𝑡))
1918breq2d 4821 . . . . . . . . . . . 12 ( = 𝑓 → (0 ≤ (𝑡) ↔ 0 ≤ (𝑓𝑡)))
2018breq1d 4819 . . . . . . . . . . . 12 ( = 𝑓 → ((𝑡) ≤ 1 ↔ (𝑓𝑡) ≤ 1))
2119, 20anbi12d 624 . . . . . . . . . . 11 ( = 𝑓 → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2221ralbidv 3133 . . . . . . . . . 10 ( = 𝑓 → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2322elrab 3519 . . . . . . . . 9 (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↔ (𝑓𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2417, 23sylbb 210 . . . . . . . 8 (𝑓𝑌 → (𝑓𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑓𝑡) ∧ (𝑓𝑡) ≤ 1)))
2524simpld 488 . . . . . . 7 (𝑓𝑌𝑓𝐴)
26 stoweidlem48.15 . . . . . . 7 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
2725, 26sylan2 586 . . . . . 6 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
28 eqid 2765 . . . . . . 7 (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) = (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))
29 stoweidlem48.16 . . . . . . 7 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
301, 5, 28, 26, 29stoweidlem16 40802 . . . . . 6 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
314, 9, 10, 11, 12, 13, 14, 15, 16, 27, 30fmuldfeq 40385 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
323, 31syldan 585 . . . 4 ((𝜑𝑡𝐷) → (𝑋𝑡) = (𝑍𝑡))
33 elnnuz 11924 . . . . . . . . 9 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
3415, 33sylib 209 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘1))
3534adantr 472 . . . . . . 7 ((𝜑𝑡𝐷) → 𝑀 ∈ (ℤ‘1))
36 nfv 2009 . . . . . . . . . . . 12 𝑖 𝑡𝑇
374, 36nfan 1998 . . . . . . . . . . 11 𝑖(𝜑𝑡𝑇)
3816ffvelrnda 6549 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
39 fveq1 6374 . . . . . . . . . . . . . . . . . . . 20 ( = (𝑈𝑖) → (𝑡) = ((𝑈𝑖)‘𝑡))
4039breq2d 4821 . . . . . . . . . . . . . . . . . . 19 ( = (𝑈𝑖) → (0 ≤ (𝑡) ↔ 0 ≤ ((𝑈𝑖)‘𝑡)))
4139breq1d 4819 . . . . . . . . . . . . . . . . . . 19 ( = (𝑈𝑖) → ((𝑡) ≤ 1 ↔ ((𝑈𝑖)‘𝑡) ≤ 1))
4240, 41anbi12d 624 . . . . . . . . . . . . . . . . . 18 ( = (𝑈𝑖) → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4342ralbidv 3133 . . . . . . . . . . . . . . . . 17 ( = (𝑈𝑖) → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4443, 5elrab2 3523 . . . . . . . . . . . . . . . 16 ((𝑈𝑖) ∈ 𝑌 ↔ ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4538, 44sylib 209 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
4645simpld 488 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝐴)
47 simpl 474 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
4847, 46jca 507 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝐴))
49 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑈𝑖) → (𝑓𝐴 ↔ (𝑈𝑖) ∈ 𝐴))
5049anbi2d 622 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝐴) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝐴)))
51 feq1 6204 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
5250, 51imbi12d 335 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ)))
5352, 26vtoclg 3418 . . . . . . . . . . . . . 14 ((𝑈𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ))
5446, 48, 53sylc 65 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5554adantlr 706 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
56 simplr 785 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
5755, 56ffvelrnd 6550 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
58 eqid 2765 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
5937, 57, 58fmptdf 6577 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ)
60 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑡𝑇)
61 ovex 6874 . . . . . . . . . . . . 13 (1...𝑀) ∈ V
62 mptexg 6677 . . . . . . . . . . . . 13 ((1...𝑀) ∈ V → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
6361, 62mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
6412fvmpt2 6480 . . . . . . . . . . . 12 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6560, 63, 64syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6665feq1d 6208 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐹𝑡):(1...𝑀)⟶ℝ ↔ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ))
6759, 66mpbird 248 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐹𝑡):(1...𝑀)⟶ℝ)
683, 67syldan 585 . . . . . . . 8 ((𝜑𝑡𝐷) → (𝐹𝑡):(1...𝑀)⟶ℝ)
6968ffvelrnda 6549 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
70 remulcl 10274 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑘 · 𝑗) ∈ ℝ)
7170adantl 473 . . . . . . 7 (((𝜑𝑡𝐷) ∧ (𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑘 · 𝑗) ∈ ℝ)
7235, 69, 71seqcl 13028 . . . . . 6 ((𝜑𝑡𝐷) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
7313fvmpt2 6480 . . . . . 6 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
743, 72, 73syl2anc 579 . . . . 5 ((𝜑𝑡𝐷) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
75 nfcv 2907 . . . . . . . . 9 𝑖𝑇
76 nfmpt1 4906 . . . . . . . . 9 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
7775, 76nfmpt 4905 . . . . . . . 8 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
7812, 77nfcxfr 2905 . . . . . . 7 𝑖𝐹
79 nfcv 2907 . . . . . . 7 𝑖𝑡
8078, 79nffv 6385 . . . . . 6 𝑖(𝐹𝑡)
81 nfv 2009 . . . . . . 7 𝑖 𝑡𝐷
824, 81nfan 1998 . . . . . 6 𝑖(𝜑𝑡𝐷)
83 nfcv 2907 . . . . . 6 𝑗seq1( · , (𝐹𝑡))
84 eqid 2765 . . . . . 6 seq1( · , (𝐹𝑡)) = seq1( · , (𝐹𝑡))
8515adantr 472 . . . . . 6 ((𝜑𝑡𝐷) → 𝑀 ∈ ℕ)
86 simpll 783 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑)
87 simpr 477 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
883adantr 472 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
8945simprd 489 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1))
9089r19.21bi 3079 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1))
9190simpld 488 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → 0 ≤ ((𝑈𝑖)‘𝑡))
9286, 87, 88, 91syl21anc 866 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝑈𝑖)‘𝑡))
9365fveq1d 6377 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
9486, 88, 93syl2anc 579 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
9586, 88, 87, 57syl21anc 866 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
9658fvmpt2 6480 . . . . . . . . 9 ((𝑖 ∈ (1...𝑀) ∧ ((𝑈𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
9787, 95, 96syl2anc 579 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
9894, 97eqtrd 2799 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡))
9992, 98breqtrrd 4837 . . . . . 6 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝐹𝑡)‘𝑖))
10090simprd 489 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → ((𝑈𝑖)‘𝑡) ≤ 1)
10186, 87, 88, 100syl21anc 866 . . . . . . 7 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ≤ 1)
10298, 101eqbrtrd 4831 . . . . . 6 (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ≤ 1)
103 stoweidlem48.17 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
104103adantr 472 . . . . . 6 ((𝜑𝑡𝐷) → 𝐸 ∈ ℝ+)
105 stoweidlem48.11 . . . . . . . . . . 11 (𝜑𝐷 ran 𝑊)
106105sselda 3761 . . . . . . . . . 10 ((𝜑𝑡𝐷) → 𝑡 ran 𝑊)
107 eluni 4597 . . . . . . . . . 10 (𝑡 ran 𝑊 ↔ ∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊))
108106, 107sylib 209 . . . . . . . . 9 ((𝜑𝑡𝐷) → ∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊))
109 stoweidlem48.9 . . . . . . . . . . . . . . . 16 (𝜑𝑊:(1...𝑀)⟶𝑉)
110 ffn 6223 . . . . . . . . . . . . . . . 16 (𝑊:(1...𝑀)⟶𝑉𝑊 Fn (1...𝑀))
111 fvelrnb 6432 . . . . . . . . . . . . . . . 16 (𝑊 Fn (1...𝑀) → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤))
112109, 110, 1113syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤))
113112biimpa 468 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤)
114113adantrl 707 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤)
115 simplr 785 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → 𝑡𝑤)
116 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → (𝑊𝑗) = 𝑤)
117115, 116eleqtrrd 2847 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑤) ∧ (𝑊𝑗) = 𝑤) → 𝑡 ∈ (𝑊𝑗))
118117ex 401 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑤) → ((𝑊𝑗) = 𝑤𝑡 ∈ (𝑊𝑗)))
119118reximdv 3162 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑤) → (∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
120119adantrr 708 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → (∃𝑗 ∈ (1...𝑀)(𝑊𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
121114, 120mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗))
122121ex 401 . . . . . . . . . . 11 (𝜑 → ((𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
123122exlimdv 2028 . . . . . . . . . 10 (𝜑 → (∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
124123adantr 472 . . . . . . . . 9 ((𝜑𝑡𝐷) → (∃𝑤(𝑡𝑤𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗)))
125108, 124mpd 15 . . . . . . . 8 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗))
126 simplll 791 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝜑)
127 simplr 785 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝑗 ∈ (1...𝑀))
128 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → 𝑡 ∈ (𝑊𝑗))
129 nfv 2009 . . . . . . . . . . . . . 14 𝑖 𝑗 ∈ (1...𝑀)
130 nfv 2009 . . . . . . . . . . . . . 14 𝑖 𝑡 ∈ (𝑊𝑗)
1314, 129, 130nf3an 2000 . . . . . . . . . . . . 13 𝑖(𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗))
132 nfv 2009 . . . . . . . . . . . . 13 𝑖((𝑈𝑗)‘𝑡) < 𝐸
133131, 132nfim 1995 . . . . . . . . . . . 12 𝑖((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
134 eleq1 2832 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑖 ∈ (1...𝑀) ↔ 𝑗 ∈ (1...𝑀)))
135 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → (𝑊𝑖) = (𝑊𝑗))
136135eleq2d 2830 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑡 ∈ (𝑊𝑖) ↔ 𝑡 ∈ (𝑊𝑗)))
137134, 1363anbi23d 1563 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) ↔ (𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗))))
138 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → (𝑈𝑖) = (𝑈𝑗))
139138fveq1d 6377 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → ((𝑈𝑖)‘𝑡) = ((𝑈𝑗)‘𝑡))
140139breq1d 4819 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝑈𝑖)‘𝑡) < 𝐸 ↔ ((𝑈𝑗)‘𝑡) < 𝐸))
141137, 140imbi12d 335 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸) ↔ ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)))
142 stoweidlem48.13 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < 𝐸)
143142r19.21bi 3079 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
1441433impa 1136 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
145133, 141, 144chvar 2368 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
146126, 127, 128, 145syl3anc 1490 . . . . . . . . . 10 ((((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑗)) → ((𝑈𝑗)‘𝑡) < 𝐸)
147146ex 401 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (𝑡 ∈ (𝑊𝑗) → ((𝑈𝑗)‘𝑡) < 𝐸))
148147reximdva 3163 . . . . . . . 8 ((𝜑𝑡𝐷) → (∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊𝑗) → ∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸))
149125, 148mpd 15 . . . . . . 7 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸)
15082, 129nfan 1998 . . . . . . . . . . . 12 𝑖((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀))
151 nfcv 2907 . . . . . . . . . . . . . 14 𝑖𝑗
15280, 151nffv 6385 . . . . . . . . . . . . 13 𝑖((𝐹𝑡)‘𝑗)
153152nfeq1 2921 . . . . . . . . . . . 12 𝑖((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡)
154150, 153nfim 1995 . . . . . . . . . . 11 𝑖(((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))
155134anbi2d 622 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀))))
156 fveq2 6375 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑗))
157156, 139eqeq12d 2780 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡) ↔ ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡)))
158155, 157imbi12d 335 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((((𝜑𝑡𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡)) ↔ (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))))
159154, 158, 98chvar 2368 . . . . . . . . . 10 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑗) = ((𝑈𝑗)‘𝑡))
160159breq1d 4819 . . . . . . . . 9 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝐹𝑡)‘𝑗) < 𝐸 ↔ ((𝑈𝑗)‘𝑡) < 𝐸))
161160biimprd 239 . . . . . . . 8 (((𝜑𝑡𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝑈𝑗)‘𝑡) < 𝐸 → ((𝐹𝑡)‘𝑗) < 𝐸))
162161reximdva 3163 . . . . . . 7 ((𝜑𝑡𝐷) → (∃𝑗 ∈ (1...𝑀)((𝑈𝑗)‘𝑡) < 𝐸 → ∃𝑗 ∈ (1...𝑀)((𝐹𝑡)‘𝑗) < 𝐸))
163149, 162mpd 15 . . . . . 6 ((𝜑𝑡𝐷) → ∃𝑗 ∈ (1...𝑀)((𝐹𝑡)‘𝑗) < 𝐸)
16480, 82, 83, 84, 85, 68, 99, 102, 104, 163fmul01lt1 40388 . . . . 5 ((𝜑𝑡𝐷) → (seq1( · , (𝐹𝑡))‘𝑀) < 𝐸)
16574, 164eqbrtrd 4831 . . . 4 ((𝜑𝑡𝐷) → (𝑍𝑡) < 𝐸)
16632, 165eqbrtrd 4831 . . 3 ((𝜑𝑡𝐷) → (𝑋𝑡) < 𝐸)
167166ex 401 . 2 (𝜑 → (𝑡𝐷 → (𝑋𝑡) < 𝐸))
1681, 167ralrimi 3104 1 (𝜑 → ∀𝑡𝐷 (𝑋𝑡) < 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wnf 1878  wcel 2155  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  wss 3732   cuni 4594   class class class wbr 4809  cmpt 4888  ran crn 5278   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  cr 10188  0cc0 10189  1c1 10190   · cmul 10194   < clt 10328  cle 10329  cn 11274  cuz 11886  +crp 12028  ...cfz 12533  seqcseq 13008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fzo 12674  df-seq 13009
This theorem is referenced by:  stoweidlem51  40837
  Copyright terms: Public domain W3C validator