![]() |
Metamath
Proof Explorer Theorem List (p. 369 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | poimirlem9 36801* | Lemma for poimir 36825, 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 36802* | Lemma for poimir 36825 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 36803* | Lemma for poimir 36825 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 36804* | Lemma for poimir 36825 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 36805* | Lemma for poimir 36825- 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 36806* | Lemma for poimir 36825- 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 36807* | Lemma for poimir 36825, that the face in poimirlem22 36814 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 36808* | Lemma for poimir 36825 establishing the vertices of the simplex of poimirlem17 36809. (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 36809* | Lemma for poimir 36825 establishing existence for poimirlem18 36810. (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 36810* | Lemma for poimir 36825 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 36811* | Lemma for poimir 36825 establishing the vertices of the simplex in poimirlem20 36812. (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 36812* | Lemma for poimir 36825 establishing existence for poimirlem21 36813. (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 36813* | Lemma for poimir 36825 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 36814* | Lemma for poimir 36825, 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 36815* | Lemma for poimir 36825, 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 36816* | Lemma for poimir 36825, 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 36817* | Lemma for poimir 36825 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 36818* | Lemma for poimir 36825 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 36819* | Lemma for poimir 36825 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 36820* | Lemma for poimir 36825, 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 36821* | Lemma for poimir 36825 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 36822* | Lemma for poimir 36825 combining poimirlem29 36821 with bwth 23135. (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 36823* | Lemma for poimir 36825, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 36822 and poimirlem28 36820. 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 36824* | Lemma for poimir 36825, combining poimirlem28 36820, poimirlem30 36822, and poimirlem31 36823 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 36825* | 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 36826* | 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 36827 | 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 36828* | Lemma for ismblfin 36833; could also be used to shorten proof of opnmbllem 25351. (Contributed by Brendan Leahy, 13-Jul-2018.) |
⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴) | ||
Theorem | mblfinlem1 36829* | Lemma for ismblfin 36833, 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 36830* | Lemma for ismblfin 36833, 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 36831* | The difference between two sets measurable by the criterion in ismblfin 36833 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 36832* | Backward direction of ismblfin 36833. (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 36833* | 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 36834* | ovoliun 25255 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
⊢ ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, < )) ⇒ ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | ex-ovoliunnfl 36835* | Demonstration of ovoliunnfl 36834. (Contributed by Brendan Leahy, 21-Nov-2017.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | voliunnfl 36836* | voliun 25304 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 36837* | volsup 25306 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.) |
⊢ ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ⇒ ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ) | ||
Theorem | mbfresfi 36838* | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) & ⊢ (𝜑 → ∪ 𝑆 = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | mbfposadd 36839* | 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 36840 | 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 36841 | Lemma for dvtan 36842- 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 36842 | Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.) |
⊢ (ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2)) | ||
Theorem | itg2addnclem 36843* | 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 36844* | Lemma for itg2addnc 36846. 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 36845* | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 36846. (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 36846 | Alternate proof of itg2add 25510 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 25459, 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 10433, 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 36847* | itg2gt0 25511 holds on functions continuous on an open interval in the absence of ax-cc 10433. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.) |
⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥)) & ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) ⇒ ⊢ (𝜑 → 0 < (∫2‘𝐹)) | ||
Theorem | ibladdnclem 36848* | Lemma for ibladdnc 36849; cf ibladdlem 25570, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 36846. (Contributed by Brendan Leahy, 31-Oct-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ) & ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ) ⇒ ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ) | ||
Theorem | ibladdnc 36849* | Choice-free analogue of itgadd 25575. A measurability hypothesis is necessitated by the loss of mbfadd 25411; 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 36850* | Lemma for itgaddnc 36852; cf. itgaddlem1 25573. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) | ||
Theorem | itgaddnclem2 36851* | Lemma for itgaddnc 36852; cf. itgaddlem2 25574. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) | ||
Theorem | itgaddnc 36852* | Choice-free analogue of itgadd 25575. (Contributed by Brendan Leahy, 11-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) | ||
Theorem | iblsubnc 36853* | Choice-free analogue of iblsub 25572. (Contributed by Brendan Leahy, 11-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝐿1) | ||
Theorem | itgsubnc 36854* | Choice-free analogue of itgsub 25576. (Contributed by Brendan Leahy, 11-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn) ⇒ ⊢ (𝜑 → ∫𝐴(𝐵 − 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 − ∫𝐴𝐶 d𝑥)) | ||
Theorem | iblabsnclem 36855* | Lemma for iblabsnc 36856; cf. iblabslem 25578. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ)) | ||
Theorem | iblabsnc 36856* | Choice-free analogue of iblabs 25579. As with ibladdnc 36849, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1) | ||
Theorem | iblmulc2nc 36857* | Choice-free analogue of iblmulc2 25581. (Contributed by Brendan Leahy, 17-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1) | ||
Theorem | itgmulc2nclem1 36858* | Lemma for itgmulc2nc 36860; cf. itgmulc2lem1 25582. (Contributed by Brendan Leahy, 17-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2nclem2 36859* | Lemma for itgmulc2nc 36860; cf. itgmulc2lem2 25583. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2nc 36860* | Choice-free analogue of itgmulc2 25584. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgabsnc 36861* | Choice-free analogue of itgabs 25585. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) & ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((∗‘∫𝐴𝐵 d𝑥) · ⦋𝑦 / 𝑥⦌𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥) | ||
Theorem | itggt0cn 36862* | itggt0 25594 holds for continuous functions in the absence of ax-cc 10433. (Contributed by Brendan Leahy, 16-Nov-2017.) |
⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) ⇒ ⊢ (𝜑 → 0 < ∫(𝑋(,)𝑌)𝐵 d𝑥) | ||
Theorem | ftc1cnnclem 36863* | Lemma for ftc1cnnc 36864; cf. ftc1lem4 25789. The stronger assumptions of ftc1cn 25793 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝑐 ∈ (𝐴(,)𝐵)) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑋 − 𝑐)) < 𝑅) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑌 − 𝑐)) < 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) < 𝐸) | ||
Theorem | ftc1cnnc 36864* | Choice-free proof of ftc1cn 25793. (Contributed by Brendan Leahy, 20-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) ⇒ ⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) | ||
Theorem | ftc1anclem1 36865 | Lemma for ftc1anc 36873- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 25408, but this proof avoids ax-cc 10433. (Contributed by Brendan Leahy, 18-Jun-2018.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (abs ∘ 𝐹) ∈ MblFn) | ||
Theorem | ftc1anclem2 36866* | Lemma for ftc1anc 36873- restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018.) (Revised by Brendan Leahy, 8-Aug-2018.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ 𝐺 ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) | ||
Theorem | ftc1anclem3 36867 | Lemma for ftc1anc 36873- the absolute value of the sum of a simple function and i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘f + ((ℝ × {i}) ∘f · 𝐺))) ∈ dom ∫1) | ||
Theorem | ftc1anclem4 36868* | Lemma for ftc1anc 36873. (Contributed by Brendan Leahy, 17-Jun-2018.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ) | ||
Theorem | ftc1anclem5 36869* | Lemma for ftc1anc 36873, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌) | ||
Theorem | ftc1anclem6 36870* | Lemma for ftc1anc 36873- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued 𝐹. (Contributed by Brendan Leahy, 31-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌) | ||
Theorem | ftc1anclem7 36871* | Lemma for ftc1anc 36873. (Contributed by Brendan Leahy, 13-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2))) | ||
Theorem | ftc1anclem8 36872* | Lemma for ftc1anc 36873. (Contributed by Brendan Leahy, 29-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦) | ||
Theorem | ftc1anc 36873* | ftc1a 25787 holds for functions that obey the triangle inequality in the absence of ax-cc 10433. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) | ||
Theorem | ftc2nc 36874* | Choice-free proof of ftc2 25794. (Contributed by Brendan Leahy, 19-Jun-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
Theorem | asindmre 36875 | Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⇒ ⊢ (𝐷 ∩ ℝ) = (-1(,)1) | ||
Theorem | dvasin 36876* | Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⇒ ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | dvacos 36877* | Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⇒ ⊢ (ℂ D (arccos ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | dvreasin 36878 | Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
⊢ (ℝ D (arcsin ↾ (-1(,)1))) = (𝑥 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | dvreacos 36879 | Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
⊢ (ℝ D (arccos ↾ (-1(,)1))) = (𝑥 ∈ (-1(,)1) ↦ (-1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | areacirclem1 36880* | Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) | ||
Theorem | areacirclem2 36881* | Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) | ||
Theorem | areacirclem3 36882* | Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿1) | ||
Theorem | areacirclem4 36883* | Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) | ||
Theorem | areacirclem5 36884* | Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⇒ ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) | ||
Theorem | areacirc 36885* | The area of a circle of radius 𝑅 is π · 𝑅↑2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⇒ ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2))) | ||
Theorem | unirep 36886* | Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011.) |
⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶) | ||
Theorem | cover2 36887* | Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐵 ∈ V & ⊢ 𝐴 = ∪ 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) | ||
Theorem | cover2g 36888* | Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010.) |
⊢ 𝐴 = ∪ 𝐵 ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))) | ||
Theorem | brabg2 36889* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} & ⊢ (𝜒 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | opelopab3 36890* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | cocanfo 36891 | Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → 𝐺 = 𝐻) | ||
Theorem | brresi2 36892 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ↾ 𝐶)𝐵 → 𝐴𝑅𝐵) | ||
Theorem | fnopabeqd 36893* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}) | ||
Theorem | fvopabf4g 36894* | Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑m 𝐷) ↦ 𝐵) ⇒ ⊢ ((𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝐴:𝐷⟶𝑅) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fnopabco 36895* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} & ⊢ 𝐺 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐻‘𝐵))} ⇒ ⊢ (𝐻 Fn 𝐶 → 𝐺 = (𝐻 ∘ 𝐹)) | ||
Theorem | opropabco 36896* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑅) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑆) & ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = ⟨𝐵, 𝐶⟩)} & ⊢ 𝐺 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐵𝑀𝐶))} ⇒ ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹)) | ||
Theorem | cocnv 36897 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ((𝐹 ∘ 𝐺) ∘ ◡𝐺) = (𝐹 ↾ ran 𝐺)) | ||
Theorem | f1ocan1fv 36898 | Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝐹 ∘ 𝐺)‘(◡𝐺‘𝑋)) = (𝐹‘𝑋)) | ||
Theorem | f1ocan2fv 36899 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ ◡𝐺)‘(𝐺‘𝑋)) = (𝐹‘𝑋)) | ||
Theorem | inixp 36900* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) = X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |