![]() |
Metamath
Proof Explorer Theorem List (p. 361 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wl-equsalcom 36001 | This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑)) | ||
Theorem | wl-equsal1i 36002 | The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.) |
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑) & ⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | wl-sb6rft 36003 | A specialization of wl-equsal1t 36000. Closed form of sb6rf 2466. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (Ⅎ𝑥𝜑 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))) | ||
Theorem | wl-cbvalsbi 36004* | Change bounded variables in a special case. The reverse direction seems to involve ax-11 2154. My hope is that I will in some future be able to prove mo3 2562 with reversed quantifiers not using ax-11 2154. See also the remark in mo4 2564, which lead me to this effort. (Contributed by Wolf Lammen, 5-Mar-2024.) |
⊢ (∀𝑥𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | wl-sbrimt 36005 | Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2300. (Contributed by Wolf Lammen, 26-Jul-2019.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | wl-sblimt 36006 | Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2300. (Contributed by Wolf Lammen, 26-Jul-2019.) |
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))) | ||
Theorem | wl-sb8t 36007 | Substitution of variable in universal quantifier. Closed form of sb8 2519. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8et 36008 | Substitution of variable in universal quantifier. Closed form of sb8e 2520. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sbhbt 36009 | Closed form of sbhb 2523. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | wl-sbnf1 36010 | Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2354. Note: This theorem shows that sbnf2 2354 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | wl-equsb3 36011 | equsb3 2101 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧)) | ||
Theorem | wl-equsb4 36012 | Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable condition. (Contributed by Wolf Lammen, 26-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑦 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧)) | ||
Theorem | wl-2sb6d 36013 | Version of 2sb6 2089 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.) |
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥) & ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤) & ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧) & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓))) | ||
Theorem | wl-sbcom2d-lem1 36014* | Lemma used to prove wl-sbcom2d 36016. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.) |
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))) | ||
Theorem | wl-sbcom2d-lem2 36015* | Lemma used to prove wl-sbcom2d 36016. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑))) | ||
Theorem | wl-sbcom2d 36016 | Version of sbcom2 2161 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.) |
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤) & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧) & ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦) ⇒ ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)) | ||
Theorem | wl-sbalnae 36017 | A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal1 36018* | A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 15-May-1993.) Proof is based on wl-sbalnae 36017 now. See also sbal1 2531. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal2 36019* | Move quantifier in and out of substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 2-Jan-2002.) Proof is based on wl-sbalnae 36017 now. See also sbal2 2532. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-2spsbbi 36020 | spsbbi 2076 applied twice. (Contributed by Wolf Lammen, 5-Aug-2023.) |
⊢ (∀𝑎∀𝑏(𝜑 ↔ 𝜓) → ([𝑦 / 𝑏][𝑥 / 𝑎]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜓)) | ||
Theorem | wl-lem-exsb 36021* | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | wl-lem-nexmo 36022 | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧)) | ||
Theorem | wl-lem-moexsb 36023* |
The antecedent ∀𝑥(𝜑 → 𝑥 = 𝑧) relates to ∃*𝑥𝜑, but is
better suited for usage in proofs. Note that no distinct variable
restriction is placed on 𝜑.
This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → (∃𝑥𝜑 ↔ [𝑧 / 𝑥]𝜑)) | ||
Theorem | wl-alanbii 36024 | This theorem extends alanimi 1818 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | wl-mo2df 36025 | Version of mof 2561 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) & ⊢ (𝜑 → Ⅎ𝑦𝜓) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo2tf 36026 | Closed form of mof 2561 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-eudf 36027 | Version of eu6 2572 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) & ⊢ (𝜑 → Ⅎ𝑦𝜓) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-eutf 36028 | Closed form of eu6 2572 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-euequf 36029 | euequ 2595 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦) | ||
Theorem | wl-mo2t 36030* | Closed form of mof 2561. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo3t 36031* | Closed form of mo3 2562. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | wl-sb8eut 36032 | Substitution of variable in universal quantifier. Closed form of sb8eu 2598. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8mot 36033 |
Substitution of variable in universal quantifier. Closed form of
sb8mo 2599.
This theorem relates to wl-mo3t 36031, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2261 and sbco 2509. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 36031 in a simple fashion, unfortunately only if 𝑥 and 𝑦 are known to be distinct. To avoid any hassle with distinctors, we prefer to derive this theorem independently, ignoring the close connection between both theorems. From an educational standpoint, one would assume wl-mo3t 36031 to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-issetft 36034 | A closed form of issetf 3459. The proof here is a modification of a subproof in vtoclgft 3509, where it could be used to shorten the proof. (Contributed by Wolf Lammen, 25-Jan-2025.) |
⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)) | ||
Theorem | wl-axc11rc11 36035 |
Proving axc11r 2364 from axc11 2428. The hypotheses are two instances of
axc11 2428 used in the proof here. Some systems
introduce axc11 2428 as an
axiom, see for example System S2 in
https://us.metamath.org/downloads/finiteaxiom.pdf 2428.
By contrast, this database sees the variant axc11r 2364, directly derived from ax-12 2171, as foundational. Later axc11 2428 is proven somewhat trickily, requiring ax-10 2137 and ax-13 2370, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.) |
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)) & ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-wl-11v 36036* | Version of ax-11 2154 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2154. It will later be converted into a theorem directly based on ax-11 2154. (Contributed by Wolf Lammen, 28-Jun-2019.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | wl-ax11-lem1 36037 | A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧)) | ||
Theorem | wl-ax11-lem2 36038* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem3 36039* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem4 36040* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-ax11-lem5 36041 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem6 36042* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem7 36043 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem8 36044* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem9 36045 | The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem10 36046* | We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 191 can be used in conjunction with wl-ax11-lem9 36045 to eliminate the second antecedent. Missing is something along the lines of ax-6 1971, so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑦 𝑦 = 𝑢 → (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑))) | ||
Theorem | wl-clabv 36047* |
Variant of df-clab 2714, 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 2707,
df-clel 2814 and df-cleq 2728. 𝑥 ∈ 𝐴 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 2108, ax-9 2116, or df-clel 2814. Theorem cleljust 2115 shows that a possible choice does not matter. The original df-clab 2714 can be rederived, see wl-dfclab 36048. 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 36048 | Rederive df-clab 2714 from wl-clabv 36047. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | ||
Theorem | wl-clabtv 36049* | Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 36050. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | wl-clabt 36050 | Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 36049. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | rabiun 36051* | Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.) |
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | iundif1 36052* | Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶) | ||
Theorem | imadifss 36053 | The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵)) | ||
Theorem | cureq 36054 | Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵) | ||
Theorem | unceq 36055 | Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵) | ||
Theorem | curf 36056 | Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) | ||
Theorem | uncf 36057 | Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) | ||
Theorem | curfv 36058 | Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | uncov 36059 | Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵)) | ||
Theorem | curunc 36060 | Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) | ||
Theorem | unccur 36061 | Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹) | ||
Theorem | phpreu 36062* | Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | finixpnum 36063* | A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card) | ||
Theorem | fin2solem 36064* | Lemma for fin2so 36065. (Contributed by Brendan Leahy, 29-Jun-2019.) |
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) | ||
Theorem | fin2so 36065 | 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 36066 | Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ 𝐴 < -(⌊‘-𝐵))) | ||
Theorem | leceifl 36067 | Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (⌊‘𝐵))) | ||
Theorem | sin2h 36068 | Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.) |
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2))) | ||
Theorem | cos2h 36069 | Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2))) | ||
Theorem | tan2h 36070 | Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))) | ||
Theorem | lindsadd 36071 | 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 36072 | 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 36073 | 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 36074 | One direction of matunitlindf 36076. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅))) | ||
Theorem | matunitlindflem2 36075 | One direction of matunitlindf 36076. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)) | ||
Theorem | matunitlindf 36076 | 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 36077* | 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 36078* | 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 36079* | Lemma for poimir 36111- 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 36080* | Lemma for poimir 36111- 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 36081* | Lemma for poimir 36111 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 36082* | Lemma for poimir 36111 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 36083* | Lemma for poimir 36111 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 36084* | Lemma for poimir 36111 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 36085* | Lemma for poimir 36111, similar to poimirlem6 36084, 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 36086* | Lemma for poimir 36111, establishing that away from the opposite vertex the walks in poimirlem9 36087 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 36087* | Lemma for poimir 36111, 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 36088* | Lemma for poimir 36111 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 36089* | Lemma for poimir 36111 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 36090* | Lemma for poimir 36111 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 36091* | Lemma for poimir 36111- 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 36092* | Lemma for poimir 36111- 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 36093* | Lemma for poimir 36111, that the face in poimirlem22 36100 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 36094* | Lemma for poimir 36111 establishing the vertices of the simplex of poimirlem17 36095. (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 36095* | Lemma for poimir 36111 establishing existence for poimirlem18 36096. (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 36096* | Lemma for poimir 36111 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 36097* | Lemma for poimir 36111 establishing the vertices of the simplex in poimirlem20 36098. (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 36098* | Lemma for poimir 36111 establishing existence for poimirlem21 36099. (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 36099* | Lemma for poimir 36111 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 36100* | Lemma for poimir 36111, 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 𝐹(𝑝‘𝑛) ≠ 𝐾) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |