| Metamath
Proof Explorer Theorem List (p. 390 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | equcomi1 38901 | Proof of equcomi 2016 from equid1 38900, avoiding use of ax-5 1910 (the only use of ax-5 1910 is via ax7 2015, so using ax-7 2007 instead would remove dependency on ax-5 1910). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
| Theorem | aecom-o 38902 | Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). Version of aecom 2432 using ax-c11 38888. Unlike axc11nfromc11 38927, this version does not require ax-5 1910 (see comment of equcomi1 38901). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
| Theorem | aecoms-o 38903 | A commutation rule for identical variable specifiers. Version of aecoms 2433 using ax-c11 38888. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
| Theorem | hbae-o 38904 | All variables are effectively bound in an identical variable specifier. Version of hbae 2436 using ax-c11 38888. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
| Theorem | dral1-o 38905 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral1 2444 using ax-c11 38888. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
| Theorem | ax12fromc15 38906 |
Rederivation of Axiom ax-12 2177 from ax-c15 38890, ax-c11 38888 (used through
dral1-o 38905), and other older axioms. See Theorem axc15 2427 for the
derivation of ax-c15 38890 from ax-12 2177.
An open problem is whether we can prove this using ax-c11n 38889 instead of ax-c11 38888. This proof uses newer axioms ax-4 1809 and ax-6 1967, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 38885 and ax-c10 38887. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
| Theorem | ax13fromc9 38907 |
Derive ax-13 2377 from ax-c9 38891 and other older axioms.
This proof uses newer axioms ax-4 1809 and ax-6 1967, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 38885 and ax-c10 38887. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
These theorems were mostly intended to study properties of the older axiom schemes and are not useful outside of this section. They should not be used outside of this section. They may be deleted when they are deemed to no longer be of interest. | ||
| Theorem | ax5ALT 38908* |
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of
the preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(This theorem simply repeats ax-5 1910 so that we can include the following note, which applies only to the obsolete axiomatization.) This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1795, ax-c4 38885, ax-c5 38884, ax-11 2157, ax-c7 38886, ax-7 2007, ax-c9 38891, ax-c10 38887, ax-c11 38888, ax-8 2110, ax-9 2118, ax-c14 38892, ax-c15 38890, and ax-c16 38893: in that system, we can derive any instance of ax-5 1910 not containing wff variables by induction on formula length, using ax5eq 38933 and ax5el 38938 for the basis together with hbn 2295, hbal 2167, and hbim 2299. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) | ||
| Theorem | sps-o 38909 | Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
| Theorem | hbequid 38910 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 38887.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥) | ||
| Theorem | nfequid-o 38911 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof uses only ax-4 1809, ax-7 2007, ax-c9 38891, and ax-gen 1795. This shows that this can be proved without ax6 2389, even though Theorem equid 2011 cannot. A shorter proof using ax6 2389 is obtainable from equid 2011 and hbth 1803.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1968, which is used for the derivation of axc9 2387, unless we consider ax-c9 38891 the starting axiom rather than ax-13 2377. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
| Theorem | axc5c7 38912 | Proof of a single axiom that can replace ax-c5 38884 and ax-c7 38886. See axc5c7toc5 38913 and axc5c7toc7 38914 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑) | ||
| Theorem | axc5c7toc5 38913 | Rederivation of ax-c5 38884 from axc5c7 38912. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | axc5c7toc7 38914 | Rederivation of ax-c7 38886 from axc5c7 38912. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
| Theorem | axc711 38915 | Proof of a single axiom that can replace both ax-c7 38886 and ax-11 2157. See axc711toc7 38917 and axc711to11 38918 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑) | ||
| Theorem | nfa1-o 38916 | 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥∀𝑥𝜑 | ||
| Theorem | axc711toc7 38917 | Rederivation of ax-c7 38886 from axc711 38915. Note that ax-c7 38886 and ax-11 2157 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
| Theorem | axc711to11 38918 | Rederivation of ax-11 2157 from axc711 38915. Note that ax-c7 38886 and ax-11 2157 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
| Theorem | axc5c711 38919 | Proof of a single axiom that can replace ax-c5 38884, ax-c7 38886, and ax-11 2157 in a subsystem that includes these axioms plus ax-c4 38885 and ax-gen 1795 (and propositional calculus). See axc5c711toc5 38920, axc5c711toc7 38921, and axc5c711to11 38922 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 38912. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) | ||
| Theorem | axc5c711toc5 38920 | Rederivation of ax-c5 38884 from axc5c711 38919. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | axc5c711toc7 38921 | Rederivation of ax-c7 38886 from axc5c711 38919. Note that ax-c7 38886 and ax-11 2157 are not used by the rederivation. The use of alimi 1811 (which uses ax-c5 38884) is allowed since we have already proved axc5c711toc5 38920. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
| Theorem | axc5c711to11 38922 | Rederivation of ax-11 2157 from axc5c711 38919. Note that ax-c7 38886 and ax-11 2157 are not used by the rederivation. The use of alimi 1811 (which uses ax-c5 38884) is allowed since we have already proved axc5c711toc5 38920. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
| Theorem | equidqe 38923 | equid 2011 with existential quantifier without using ax-c5 38884 or ax-5 1910. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥 | ||
| Theorem | axc5sp1 38924 | A special case of ax-c5 38884 without using ax-c5 38884 or ax-5 1910. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥) | ||
| Theorem | equidq 38925 | equid 2011 with universal quantifier without using ax-c5 38884 or ax-5 1910. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∀𝑦 𝑥 = 𝑥 | ||
| Theorem | equid1ALT 38926 | Alternate proof of equid 2011 and equid1 38900 from older axioms ax-c7 38886, ax-c10 38887 and ax-c9 38891. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑥 = 𝑥 | ||
| Theorem | axc11nfromc11 38927 |
Rederivation of ax-c11n 38889 from original version ax-c11 38888. See Theorem
axc11 2435 for the derivation of ax-c11 38888 from ax-c11n 38889.
This theorem should not be referenced in any proof. Instead, use ax-c11n 38889 above so that uses of ax-c11n 38889 can be more easily identified, or use aecom-o 38902 when this form is needed for studies involving ax-c11 38888 and omitting ax-5 1910. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
| Theorem | naecoms-o 38928 | A commutation rule for distinct variable specifiers. Version of naecoms 2434 using ax-c11 38888. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
| Theorem | hbnae-o 38929 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2437 using ax-c11 38888. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
| Theorem | dvelimf-o 38930 | Proof of dvelimh 2455 that uses ax-c11 38888 but not ax-c15 38890, ax-c11n 38889, or ax-12 2177. Version of dvelimh 2455 using ax-c11 38888 instead of axc11 2435. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
| Theorem | dral2-o 38931 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral2 2443 using ax-c11 38888. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
| Theorem | aev-o 38932* | A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 38893. Version of aev 2057 using ax-c11 38888. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
| Theorem | ax5eq 38933* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1910 considered as a metatheorem. Do not use it for later proofs - use ax-5 1910 instead, to avoid reference to the redundant axiom ax-c16 38893.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) | ||
| Theorem | dveeq2-o 38934* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2383 using ax-c15 38890. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
| Theorem | axc16g-o 38935* | A generalization of Axiom ax-c16 38893. Version of axc16g 2260 using ax-c11 38888. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
| Theorem | dveeq1-o 38936* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2385 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
| Theorem | dveeq1-o16 38937* | Version of dveeq1 2385 using ax-c16 38893 instead of ax-5 1910. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1910. (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
| Theorem | ax5el 38938* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1910 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | ||
| Theorem | axc11n-16 38939* | This theorem shows that, given ax-c16 38893, we can derive a version of ax-c11n 38889. However, it is weaker than ax-c11n 38889 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
| Theorem | dveel2ALT 38940* | Alternate proof of dveel2 2467 using ax-c16 38893 instead of ax-5 1910. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
| Theorem | ax12f 38941 | Basis step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. We can start with any formula 𝜑 in which 𝑥 is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
| Theorem | ax12eq 38942 | Basis step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) | ||
| Theorem | ax12el 38943 | Basis step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) | ||
| Theorem | ax12indn 38944 | Induction step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))) | ||
| Theorem | ax12indi 38945 | Induction step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))))) | ||
| Theorem | ax12indalem 38946 | Lemma for ax12inda2 38948 and ax12inda 38949. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) | ||
| Theorem | ax12inda2ALT 38947* | Alternate proof of ax12inda2 38948, slightly more direct and not requiring ax-c16 38893. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
| Theorem | ax12inda2 38948* | Induction step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 38949. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
| Theorem | ax12inda 38949* | Induction step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 38948 may be used instead to avoid the dummy variable 𝑤 in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
| Theorem | ax12v2-o 38950* | Rederivation of ax-c15 38890 from ax12v 2178 (without using ax-c15 38890 or the full ax-12 2177). Thus, the hypothesis (ax12v 2178) provides an alternate axiom that can be used in place of ax-c15 38890. See also axc15 2427. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
| Theorem | ax12a2-o 38951* | Derive ax-c15 38890 from a hypothesis in the form of ax-12 2177, without using ax-12 2177 or ax-c15 38890. The hypothesis is weaker than ax-12 2177, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2177, if we also have ax-c11 38888, which this proof uses. As Theorem ax12 2428 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 38889 instead of ax-c11 38888. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
| Theorem | axc11-o 38952 |
Show that ax-c11 38888 can be derived from ax-c11n 38889 and ax-12 2177. An open
problem is whether this theorem can be derived from ax-c11n 38889 and the
others when ax-12 2177 is replaced with ax-c15 38890 or ax12v 2178. See Theorems
axc11nfromc11 38927 for the rederivation of ax-c11n 38889 from axc11 2435.
Normally, axc11 2435 should be used rather than ax-c11 38888 or axc11-o 38952, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
| Theorem | fsumshftd 38953* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15816. The proof demonstrates how this can be derived starting from from fsumshft 15816. (Contributed by NM, 1-Nov-2019.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) | ||
| Axiom | ax-riotaBAD 38954 | Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse 𝐴. See also comments for df-iota 6514. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7388, CONFLICTS WITH (THE NEW) df-riota 7388 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
| ⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴})) | ||
| Theorem | riotaclbgBAD 38955* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)) | ||
| Theorem | riotaclbBAD 38956* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
| Theorem | riotasvd 38957* | Deduction version of riotasv 38960. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶)) | ||
| Theorem | riotasv2d 38958* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5403). Special case of riota2f 7412. (Contributed by NM, 2-Mar-2013.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝐹) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹) | ||
| Theorem | riotasv2s 38959* | The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5403) in the form of a substitution instance. Special case of riota2f 7412. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
| ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶) | ||
| Theorem | riotasv 38960* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5403). Special case of riota2f 7412. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶) | ||
| Theorem | riotasv3d 38961* | A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 5403) also holds for its description binder 𝐷 (in the form of property 𝜃). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜃) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝜒)) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝜃) | ||
| Theorem | elimhyps 38962 | A version of elimhyp 4591 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
| ⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑 | ||
| Theorem | dedths 38963 | A version of weak deduction theorem dedth 4584 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
| ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓 ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | renegclALT 38964 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11572. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
| Theorem | elimhyps2 38965 | Generalization of elimhyps 38962 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
| ⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑 | ||
| Theorem | dedths2 38966 | Generalization of dedths 38963 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
| ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) | ||
| Theorem | nfcxfrdf 38967 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
| Theorem | nfded 38968 | A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g., (Ⅎ𝑥𝐴 → ∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴} = ∪ 𝐴)) that starts from abidnf 3708. The last is assigned to the inference form (e.g., Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2913. (Contributed by NM, 19-Nov-2020.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐶) | ||
| Theorem | nfded2 38969 | A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g., ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 = 〈𝐴, 𝐵〉) for nfopd 4890) that starts from abidnf 3708. The last is assigned to the inference form (e.g., Ⅎ𝑥〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 for nfop 4889) whose hypotheses are satisfied using nfaba1 2913. (Contributed by NM, 19-Nov-2020.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷) & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐷) | ||
| Theorem | nfunidALT2 38970 | Deduction version of nfuni 4914. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
| Theorem | nfunidALT 38971 | Deduction version of nfuni 4914. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
| Theorem | nfopdALT 38972 | Deduction version of bound-variable hypothesis builder nfop 4889. This shows how the deduction version of a not-free theorem such as nfop 4889 can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥〈𝐴, 𝐵〉) | ||
| Theorem | cnaddcom 38973 | Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Theorem | toycom 38974* | Show the commutative law for an operation 𝑂 on a toy structure class 𝐶 of commutative operations on ℂ. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of 𝐶. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.) |
| ⊢ 𝐶 = {𝑔 ∈ Abel ∣ (Base‘𝑔) = ℂ} & ⊢ + = (+g‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Syntax | clsa 38975 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
| class LSAtoms | ||
| Syntax | clsh 38976 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
| class LSHyp | ||
| Definition | df-lsatoms 38977* | Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) |
| ⊢ LSAtoms = (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣}))) | ||
| Definition | df-lshyp 38978* | Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less than the full space. (Contributed by NM, 29-Jun-2014.) |
| ⊢ LSHyp = (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))}) | ||
| Theorem | lshpset 38979* | The set of all hyperplanes of a left module or left vector space. The vector 𝑣 is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐻 = {𝑠 ∈ 𝑆 ∣ (𝑠 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑁‘(𝑠 ∪ {𝑣})) = 𝑉)}) | ||
| Theorem | islshp 38980* | The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑁‘(𝑈 ∪ {𝑣})) = 𝑉))) | ||
| Theorem | islshpsm 38981* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉))) | ||
| Theorem | lshplss 38982 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
| ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
| Theorem | lshpne 38983 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → 𝑈 ≠ 𝑉) | ||
| Theorem | lshpnel 38984 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) | ||
| Theorem | lshpnelb 38985 | The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)) | ||
| Theorem | lshpnel2N 38986 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)) | ||
| Theorem | lshpne0 38987 | The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.) (Proof shortened by AV, 19-Jul-2022.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ≠ 0 ) | ||
| Theorem | lshpdisj 38988 | A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) ⇒ ⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑋})) = { 0 }) | ||
| Theorem | lshpcmp 38989 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
| ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐻) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) | ||
| Theorem | lshpinN 38990 | The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐻) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → ((𝑇 ∩ 𝑈) ∈ 𝐻 ↔ 𝑇 = 𝑈)) | ||
| Theorem | lsatset 38991* | The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) | ||
| Theorem | islsat 38992* | The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥}))) | ||
| Theorem | lsatlspsn2 38993 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 38994 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ 𝐴) | ||
| Theorem | lsatlspsn 38994 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴) | ||
| Theorem | islsati 38995* | A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴) → ∃𝑣 ∈ 𝑉 𝑈 = (𝑁‘{𝑣})) | ||
| Theorem | lsateln0 38996* | A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015.) |
| ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ 𝑈 𝑣 ≠ 0 ) | ||
| Theorem | lsatlss 38997 | The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
| ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝐴 ⊆ 𝑆) | ||
| Theorem | lsatlssel 38998 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
| ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
| Theorem | lsatssv 38999 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑄 ⊆ 𝑉) | ||
| Theorem | lsatn0 39000 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 32364 analog.) (Contributed by NM, 25-Aug-2014.) |
| ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑈 ≠ { 0 }) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |