![]() |
Metamath
Proof Explorer Theorem List (p. 374 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30846) |
![]() (30847-32369) |
![]() (32370-48587) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wl-clabv 37301* |
Variant of df-clab 2704, where the element 𝑥 is required to be
disjoint from the class it is taken from. This restriction meets
similar ones found in other definitions and axioms like ax-ext 2697,
df-clel 2803 and df-cleq 2718. 𝑥 ∈ 𝐴 with 𝐴 depending on 𝑥 can
be the source of side effects, that you rather want to be aware of. So
here we eliminate one possible way of letting this slip in instead.
An expression 𝑥 ∈ 𝐴 with 𝑥, 𝐴 not disjoint, is now only introduced either via ax-8 2101, ax-9 2109, or df-clel 2803. Theorem cleljust 2108 shows that a possible choice does not matter. The original df-clab 2704 can be rederived, see wl-dfclab 37302. In an implementation this theorem is the only user of df-clab. (Contributed by NM, 26-May-1993.) Element and class are disjoint. (Revised by Wolf Lammen, 31-May-2023.) |
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | ||
Theorem | wl-dfclab 37302 | Rederive df-clab 2704 from wl-clabv 37301. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | ||
Theorem | wl-clabtv 37303* | Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 37304. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | wl-clabt 37304 | Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 37303. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | rabiun 37305* | Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.) |
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | iundif1 37306* | Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶) | ||
Theorem | imadifss 37307 | The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵)) | ||
Theorem | cureq 37308 | Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵) | ||
Theorem | unceq 37309 | Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵) | ||
Theorem | curf 37310 | Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) | ||
Theorem | uncf 37311 | Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) | ||
Theorem | curfv 37312 | Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | uncov 37313 | Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵)) | ||
Theorem | curunc 37314 | Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) | ||
Theorem | unccur 37315 | Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹) | ||
Theorem | phpreu 37316* | Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | finixpnum 37317* | A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card) | ||
Theorem | fin2solem 37318* | Lemma for fin2so 37319. (Contributed by Brendan Leahy, 29-Jun-2019.) |
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) | ||
Theorem | fin2so 37319 | Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.) |
⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin) | ||
Theorem | ltflcei 37320 | Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ 𝐴 < -(⌊‘-𝐵))) | ||
Theorem | leceifl 37321 | Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (⌊‘𝐵))) | ||
Theorem | sin2h 37322 | Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.) |
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2))) | ||
Theorem | cos2h 37323 | Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2))) | ||
Theorem | tan2h 37324 | Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))) | ||
Theorem | lindsadd 37325 | In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023.) |
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊)) | ||
Theorem | lindsdom 37326 | A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼) | ||
Theorem | lindsenlbs 37327 | A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → 𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼))) | ||
Theorem | matunitlindflem1 37328 | One direction of matunitlindf 37330. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅))) | ||
Theorem | matunitlindflem2 37329 | One direction of matunitlindf 37330. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)) | ||
Theorem | matunitlindf 37330 | A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) | ||
Theorem | ptrest 37331* | Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))) | ||
Theorem | ptrecube 37332* | Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) | ||
Theorem | poimirlem1 37333* | Lemma for poimir 37365- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) ⇒ ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) | ||
Theorem | poimirlem2 37334* | Lemma for poimir 37365- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉})) ⇒ ⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)) | ||
Theorem | poimirlem3 37335* | Lemma for poimir 37365 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < 𝑁) & ⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾)) & ⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀)) ⇒ ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (〈(𝑇 ∪ {〈(𝑀 + 1), 0〉}), (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})〉 ∈ (((0..^𝐾) ↑m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘f + ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1))))) | ||
Theorem | poimirlem4 37336* | Lemma for poimir 37365 connecting the admissible faces on the back face of the (𝑀 + 1)-cube to admissible simplices in the 𝑀-cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → {𝑠 ∈ (((0..^𝐾) ↑m (1...𝑀)) × {𝑓 ∣ 𝑓:(1...𝑀)–1-1-onto→(1...𝑀)}) ∣ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵} ≈ {𝑠 ∈ (((0..^𝐾) ↑m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∣ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((1st ‘𝑠)‘(𝑀 + 1)) = 0 ∧ ((2nd ‘𝑠)‘(𝑀 + 1)) = (𝑀 + 1))}) | ||
Theorem | poimirlem5 37337* | Lemma for poimir 37365 to establish that, for the simplices defined by a walk along the edges of an 𝑁-cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 0 < (2nd ‘𝑇)) ⇒ ⊢ (𝜑 → (𝐹‘0) = (1st ‘(1st ‘𝑇))) | ||
Theorem | poimirlem6 37338* | Lemma for poimir 37365 establishing, for a face of a simplex defined by a walk along the edges of an 𝑁-cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 ∈ (1...((2nd ‘𝑇) − 1))) ⇒ ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀)) | ||
Theorem | poimirlem7 37339* | Lemma for poimir 37365, similar to poimirlem6 37338, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 ∈ ((((2nd ‘𝑇) + 1) + 1)...𝑁)) ⇒ ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀)) | ||
Theorem | poimirlem8 37340* | Lemma for poimir 37365, establishing that away from the opposite vertex the walks in poimirlem9 37341 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((2nd ‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd ‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | ||
Theorem | poimirlem9 37341* | Lemma for poimir 37365, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘(1st ‘𝑈)) ≠ (2nd ‘(1st ‘𝑇))) ⇒ ⊢ (𝜑 → (2nd ‘(1st ‘𝑈)) = ((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))))) | ||
Theorem | poimirlem10 37342* | Lemma for poimir 37365 establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) ⇒ ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘f − ((1...𝑁) × {1})) = (1st ‘(1st ‘𝑇))) | ||
Theorem | poimirlem11 37343* | Lemma for poimir 37365 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑈) = 0) & ⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀))) | ||
Theorem | poimirlem12 37344* | Lemma for poimir 37365 connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑈) = 𝑁) & ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1))) ⇒ ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀))) | ||
Theorem | poimirlem13 37345* | Lemma for poimir 37365- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) ⇒ ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) | ||
Theorem | poimirlem14 37346* | Lemma for poimir 37365- for at most one simplex associated with a shared face is the opposite vertex last on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) ⇒ ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) | ||
Theorem | poimirlem15 37347* | Lemma for poimir 37365, that the face in poimirlem22 37354 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) ⇒ ⊢ (𝜑 → 〈〈(1st ‘(1st ‘𝑇)), ((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))))〉, (2nd ‘𝑇)〉 ∈ 𝑆) | ||
Theorem | poimirlem16 37348* | Lemma for poimir 37365 establishing the vertices of the simplex of poimirlem17 37349. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) ⇒ ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st ‘𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))) | ||
Theorem | poimirlem17 37349* | Lemma for poimir 37365 establishing existence for poimirlem18 37350. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) | ||
Theorem | poimirlem18 37350* | Lemma for poimir 37365 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) | ||
Theorem | poimirlem19 37351* | Lemma for poimir 37365 establishing the vertices of the simplex in poimirlem20 37352. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) & ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st ‘𝑇))‘𝑁), 1, 0))) ∘f + (((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) | ||
Theorem | poimirlem20 37352* | Lemma for poimir 37365 establishing existence for poimirlem21 37353. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) & ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) | ||
Theorem | poimirlem21 37353* | Lemma for poimir 37365 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) & ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) | ||
Theorem | poimirlem22 37354* | Lemma for poimir 37365, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) | ||
Theorem | poimirlem23 37355* | Lemma for poimir 37365, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾)) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ (𝜑 → 𝑉 ∈ (0...𝑁)) ⇒ ⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))) | ||
Theorem | poimirlem24 37356* | Lemma for poimir 37365, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑝 = ((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾)) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ (𝜑 → 𝑉 ∈ (0...𝑁)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))) | ||
Theorem | poimirlem25 37357* | Lemma for poimir 37365 stating that for a given simplex such that no vertex maps to 𝑁, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑝 = ((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾)) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ≠ ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶) ⇒ ⊢ (𝜑 → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋〈𝑇, 𝑈〉 / 𝑠⦌𝐶})) | ||
Theorem | poimirlem26 37358* | Lemma for poimir 37365 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑝 = ((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) ⇒ ⊢ (𝜑 → 2 ∥ ((♯‘{𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd ‘𝑡)})𝑖 = ⦋(1st ‘𝑡) / 𝑠⦌𝐶}) − (♯‘{𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶}))) | ||
Theorem | poimirlem27 37359* | Lemma for poimir 37365 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑝 = ((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 0)) → 𝐵 < 𝑛) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1)) ⇒ ⊢ (𝜑 → 2 ∥ ((♯‘{𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd ‘𝑡)})𝑖 = ⦋(1st ‘𝑡) / 𝑠⦌𝐶}) − (♯‘{𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ (0...(𝑁 − 1))𝑖 = 𝐶 ∧ ((1st ‘𝑠)‘𝑁) = 0 ∧ ((2nd ‘𝑠)‘𝑁) = 𝑁)}))) | ||
Theorem | poimirlem28 37360* | Lemma for poimir 37365, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝑝 = ((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 0)) → 𝐵 < 𝑛) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶) | ||
Theorem | poimirlem29 37361* | Lemma for poimir 37365 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁)) & ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) & ⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛) & ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) & ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) ⇒ ⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) | ||
Theorem | poimirlem30 37362* | Lemma for poimir 37365 combining poimirlem29 37361 with bwth 23400. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁)) & ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) & ⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛) & ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) & ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) | ||
Theorem | poimirlem31 37363* | Lemma for poimir 37365, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 37362 and poimirlem28 37360. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁)) & ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0) & ⊢ 𝑃 = ((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) & ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) & ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )) ⇒ ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘f / ((1...𝑁) × {𝑘})))‘𝑛)) | ||
Theorem | poimirlem32 37364* | Lemma for poimir 37365, combining poimirlem28 37360, poimirlem30 37362, and poimirlem31 37363 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁)) & ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) | ||
Theorem | poimir 37365* | Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁)) & ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0) & ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 (𝐹‘𝑐) = ((1...𝑁) × {0})) | ||
Theorem | broucube 37366* | Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁)) & ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)) | ||
Theorem | heicant 37367 | Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.) (Proof shortened by AV, 27-Sep-2020.) |
⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → (MetOpen‘𝐶) ∈ Comp) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷))) | ||
Theorem | opnmbllem0 37368* | Lemma for ismblfin 37373; could also be used to shorten proof of opnmbllem 25616. (Contributed by Brendan Leahy, 13-Jul-2018.) |
⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴) | ||
Theorem | mblfinlem1 37369* | Lemma for ismblfin 37373, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in 𝐴. (Contributed by Brendan Leahy, 13-Jul-2018.) |
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) | ||
Theorem | mblfinlem2 37370* | Lemma for ismblfin 37373, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different definition of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑀 ∈ ℝ ∧ 𝑀 < (vol*‘𝐴)) → ∃𝑠 ∈ (Clsd‘(topGen‘ran (,)))(𝑠 ⊆ 𝐴 ∧ 𝑀 < (vol*‘𝑠))) | ||
Theorem | mblfinlem3 37371* | The difference between two sets measurable by the criterion in ismblfin 37373 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) ∧ ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) ∧ (vol*‘𝐵) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐵 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))) → sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ (𝐴 ∖ 𝐵) ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) = (vol*‘(𝐴 ∖ 𝐵))) | ||
Theorem | mblfinlem4 37372* | Backward direction of ismblfin 37373. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ 𝐴 ∈ dom vol) → (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) | ||
Theorem | ismblfin 37373* | Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.) |
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐴 ∈ dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))) | ||
Theorem | ovoliunnfl 37374* | ovoliun 25520 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
⊢ ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, < )) ⇒ ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | ex-ovoliunnfl 37375* | Demonstration of ovoliunnfl 37374. (Contributed by Brendan Leahy, 21-Nov-2017.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | voliunnfl 37376* | voliun 25569 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.) |
⊢ 𝑆 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) & ⊢ ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < )) ⇒ ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | volsupnfl 37377* | volsup 25571 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.) |
⊢ ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ⇒ ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | mbfresfi 37378* | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) & ⊢ (𝜑 → ∪ 𝑆 = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfposadd 37379* | If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn) | ||
Theorem | cnambfre 37380 | A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn) | ||
Theorem | dvtanlem 37381 | Lemma for dvtan 37382- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (◡cos “ (ℂ ∖ {0})) ∈ (TopOpen‘ℂfld) | ||
Theorem | dvtan 37382 | Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.) |
⊢ (ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2)) | ||
Theorem | itg2addnclem 37383* | An alternate expression for the ∫2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.) |
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔‘𝑧) = 0, 0, ((𝑔‘𝑧) + 𝑦))) ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))} ⇒ ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < )) | ||
Theorem | itg2addnclem2 37384* | Lemma for itg2addnc 37386. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) ⇒ ⊢ (((𝜑 ∧ ℎ ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹‘𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (ℎ‘𝑥) ∧ (ℎ‘𝑥) ≠ 0), (((⌊‘((𝐹‘𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (ℎ‘𝑥))) ∈ dom ∫1) | ||
Theorem | itg2addnclem3 37385* | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 37386. (Contributed by Brendan Leahy, 11-Mar-2018.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ) ⇒ ⊢ (𝜑 → (∃ℎ ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((ℎ‘𝑧) = 0, 0, ((ℎ‘𝑧) + 𝑦))) ∘r ≤ (𝐹 ∘f + 𝐺) ∧ 𝑠 = (∫1‘ℎ)) → ∃𝑡∃𝑢(∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1((∃𝑐 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑓‘𝑧) = 0, 0, ((𝑓‘𝑧) + 𝑐))) ∘r ≤ 𝐹 ∧ 𝑡 = (∫1‘𝑓)) ∧ (∃𝑑 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔‘𝑧) = 0, 0, ((𝑔‘𝑧) + 𝑑))) ∘r ≤ 𝐺 ∧ 𝑢 = (∫1‘𝑔))) ∧ 𝑠 = (𝑡 + 𝑢)))) | ||
Theorem | itg2addnc 37386 | Alternate proof of itg2add 25775 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 25724, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 10467, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.) |
⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞)) & ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ) ⇒ ⊢ (𝜑 → (∫2‘(𝐹 ∘f + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺))) | ||
Theorem | itg2gt0cn 37387* | itg2gt0 25776 holds on functions continuous on an open interval in the absence of ax-cc 10467. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.) |
⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥)) & ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) ⇒ ⊢ (𝜑 → 0 < (∫2‘𝐹)) | ||
Theorem | ibladdnclem 37388* | Lemma for ibladdnc 37389; cf ibladdlem 25835, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 37386. (Contributed by Brendan Leahy, 31-Oct-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ) & ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ) ⇒ ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ) | ||
Theorem | ibladdnc 37389* | Choice-free analogue of itgadd 25840. A measurability hypothesis is necessitated by the loss of mbfadd 25676; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1) | ||
Theorem | itgaddnclem1 37390* | Lemma for itgaddnc 37392; cf. itgaddlem1 25838. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) | ||
Theorem | itgaddnclem2 37391* | Lemma for itgaddnc 37392; cf. itgaddlem2 25839. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) | ||
Theorem | itgaddnc 37392* | Choice-free analogue of itgadd 25840. (Contributed by Brendan Leahy, 11-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) | ||
Theorem | iblsubnc 37393* | Choice-free analogue of iblsub 25837. (Contributed by Brendan Leahy, 11-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝐿1) | ||
Theorem | itgsubnc 37394* | Choice-free analogue of itgsub 25841. (Contributed by Brendan Leahy, 11-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 − 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 − ∫𝐴𝐶 d𝑥)) | ||
Theorem | iblabsnclem 37395* | Lemma for iblabsnc 37396; cf. iblabslem 25843. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ)) | ||
Theorem | iblabsnc 37396* | Choice-free analogue of iblabs 25844. As with ibladdnc 37389, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1) | ||
Theorem | iblmulc2nc 37397* | Choice-free analogue of iblmulc2 25846. (Contributed by Brendan Leahy, 17-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1) | ||
Theorem | itgmulc2nclem1 37398* | Lemma for itgmulc2nc 37400; cf. itgmulc2lem1 25847. (Contributed by Brendan Leahy, 17-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2nclem2 37399* | Lemma for itgmulc2nc 37400; cf. itgmulc2lem2 25848. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2nc 37400* | Choice-free analogue of itgmulc2 25849. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |