Home | Metamath
Proof Explorer Theorem List (p. 343 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | axc711toc7 34201 | Rederivation of ax-c7 34170 from axc711 34199. Note that ax-c7 34170 and ax-11 2034 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711to11 34202 | Rederivation of ax-11 2034 from axc711 34199. Note that ax-c7 34170 and ax-11 2034 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | axc5c711 34203 | Proof of a single axiom that can replace ax-c5 34168, ax-c7 34170, and ax-11 2034 in a subsystem that includes these axioms plus ax-c4 34169 and ax-gen 1722 (and propositional calculus). See axc5c711toc5 34204, axc5c711toc7 34205, and axc5c711to11 34206 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 34196. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c711toc5 34204 | Rederivation of ax-c5 34168 from axc5c711 34203. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711toc7 34205 | Rederivation of ax-c7 34170 from axc5c711 34203. Note that ax-c7 34170 and ax-11 2034 are not used by the rederivation. The use of alimi 1739 (which uses ax-c5 34168) is allowed since we have already proved axc5c711toc5 34204. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711to11 34206 | Rederivation of ax-11 2034 from axc5c711 34203. Note that ax-c7 34170 and ax-11 2034 are not used by the rederivation. The use of alimi 1739 (which uses ax-c5 34168) is allowed since we have already proved axc5c711toc5 34204. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | equidqe 34207 | equid 1939 with existential quantifier without using ax-c5 34168 or ax-5 1839. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥 | ||
Theorem | axc5sp1 34208 | A special case of ax-c5 34168 without using ax-c5 34168 or ax-5 1839. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥) | ||
Theorem | equidq 34209 | equid 1939 with universal quantifier without using ax-c5 34168 or ax-5 1839. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑦 𝑥 = 𝑥 | ||
Theorem | equid1ALT 34210 | Alternate proof of equid 1939 and equid1 34184 from older axioms ax-c7 34170, ax-c10 34171 and ax-c9 34175. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | axc11nfromc11 34211 |
Rederivation of ax-c11n 34173 from original version ax-c11 34172. See theorem
axc11 2314 for the derivation of ax-c11 34172 from ax-c11n 34173.
This theorem should not be referenced in any proof. Instead, use ax-c11n 34173 above so that uses of ax-c11n 34173 can be more easily identified, or use aecom-o 34186 when this form is needed for studies involving ax-c11 34172 and omitting ax-5 1839. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | naecoms-o 34212 | A commutation rule for distinct variable specifiers. Version of naecoms 2313 using ax-c11 34172. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbnae-o 34213 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2317 using ax-c11 34172. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | dvelimf-o 34214 | Proof of dvelimh 2336 that uses ax-c11 34172 but not ax-c15 34174, ax-c11n 34173, or ax-12 2047. Version of dvelimh 2336 using ax-c11 34172 instead of axc11 2314. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dral2-o 34215 | 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 2324 using ax-c11 34172. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | aev-o 34216* | A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 34177. Version of aev 1983 using ax-c11 34172. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
Theorem | ax5eq 34217* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1839 considered as a metatheorem. Do not use it for later proofs - use ax-5 1839 instead, to avoid reference to the redundant axiom ax-c16 34177.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) | ||
Theorem | dveeq2-o 34218* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2298 using ax-c15 34174. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | axc16g-o 34219* | A generalization of axiom ax-c16 34177. Version of axc16g 2134 using ax-c11 34172. (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 34220* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2300 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | dveeq1-o16 34221* | Version of dveeq1 2300 using ax-c16 34177 instead of ax-5 1839. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1839. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax5el 34222* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1839 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | ||
Theorem | axc11n-16 34223* | This theorem shows that, given ax-c16 34177, we can derive a version of ax-c11n 34173. However, it is weaker than ax-c11n 34173 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | dveel2ALT 34224* | Alternate proof of dveel2 2371 using ax-c16 34177 instead of ax-5 1839. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | ax12f 34225 | Basis step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. 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 34226 | Basis step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) | ||
Theorem | ax12el 34227 | Basis step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) | ||
Theorem | ax12indn 34228 | Induction step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))) | ||
Theorem | ax12indi 34229 | Induction step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))))) | ||
Theorem | ax12indalem 34230 | Lemma for ax12inda2 34232 and ax12inda 34233. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) | ||
Theorem | ax12inda2ALT 34231* | Alternate proof of ax12inda2 34232, slightly more direct and not requiring ax-c16 34177. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda2 34232* | Induction step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 34233. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda 34233* | Induction step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 34232 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 34234* | Rederivation of ax-c15 34174 from ax12v 2048 (without using ax-c15 34174 or the full ax-12 2047). Thus, the hypothesis (ax12v 2048) provides an alternate axiom that can be used in place of ax-c15 34174. See also axc15 2303. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12a2-o 34235* | Derive ax-c15 34174 from a hypothesis in the form of ax-12 2047, without using ax-12 2047 or ax-c15 34174. The hypothesis is weaker than ax-12 2047, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2047, if we also have ax-c11 34172, which this proof uses. As theorem ax12 2304 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 34173 instead of ax-c11 34172. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | axc11-o 34236 |
Show that ax-c11 34172 can be derived from ax-c11n 34173 and ax-12 2047. An open
problem is whether this theorem can be derived from ax-c11n 34173 and the
others when ax-12 2047 is replaced with ax-c15 34174 or ax12v 2048. See theorem
axc11nfromc11 34211 for the rederivation of ax-c11n 34173 from axc11 2314.
Normally, axc11 2314 should be used rather than ax-c11 34172 or axc11-o 34236, 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 34237* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 14512. The proof demonstrates how this can be derived starting from from fsumshft 14512. (Contributed by NM, 1-Nov-2019.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) | ||
Theorem | fsumshftdOLD 34238* | Obsolete version of fsumshftd 34237 as of 1-Nov-2019. (Contributed by NM, 1-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) | ||
Axiom | ax-riotaBAD 34239 | 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 5851. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6611, CONFLICTS WITH (THE NEW) df-riota 6611 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴})) | ||
Theorem | riotaclbgBAD 34240* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)) | ||
Theorem | riotaclbBAD 34241* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
Theorem | riotasvd 34242* | Deduction version of riotasv 34245. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶)) | ||
Theorem | riotasv2d 34243* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 4874). Special case of riota2f 6632. (Contributed by NM, 2-Mar-2013.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝐹) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹) | ||
Theorem | riotasv2s 34244* | The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 4874) in the form of a substitution instance. Special case of riota2f 6632. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶) | ||
Theorem | riotasv 34245* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 4874). Special case of riota2f 6632. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶) | ||
Theorem | riotasv3d 34246* | A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 4874) 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 34247 | A version of elimhyp 4146 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑 | ||
Theorem | dedths 34248 | A version of weak deduction theorem dedth 4139 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | renegclALT 34249 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 10344. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
Theorem | elimhyps2 34250 | Generalization of elimhyps 34247 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑 | ||
Theorem | dedths2 34251 | Generalization of dedths 34248 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) | ||
Theorem | 19.9alt 34252 | Version of 19.9t 2071 for universal quantifier. (Contributed by NM, 9-Nov-2020.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥𝜑 ↔ 𝜑)) | ||
Theorem | nfcxfrdf 34253 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfded 34254 | 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 3375. The last is assigned to the inference form (e.g. Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2770. (Contributed by NM, 19-Nov-2020.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐶) | ||
Theorem | nfded2 34255 | 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 4419) that starts from abidnf 3375. The last is assigned to the inference form (e.g. Ⅎ𝑥〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 for nfop 4418) whose hypotheses are satisfied using nfaba1 2770. (Contributed by NM, 19-Nov-2020.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷) & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐷) | ||
Theorem | nfunidALT2 34256 | Deduction version of nfuni 4442. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfunidALT 34257 | Deduction version of nfuni 4442. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfopdALT 34258 | Deduction version of bound-variable hypothesis builder nfop 4418. This shows how the deduction version of a not-free theorem such as nfop 4418 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 34259 | 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 34260* | Show the commutative law for an operation 𝑂 on a toy structure class 𝐶 of commuatitive 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 34261 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
class LSAtoms | ||
Syntax | clsh 34262 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
class LSHyp | ||
Definition | df-lsatoms 34263* | 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 34264* | 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 that the full space. (Contributed by NM, 29-Jun-2014.) |
⊢ LSHyp = (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))}) | ||
Theorem | lshpset 34265* | 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 34266* | 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 34267* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉))) | ||
Theorem | lshplss 34268 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | lshpne 34269 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → 𝑈 ≠ 𝑉) | ||
Theorem | lshpnel 34270 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) | ||
Theorem | lshpnelb 34271 | 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 34272 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)) | ||
Theorem | lshpne0 34273 | The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ≠ 0 ) | ||
Theorem | lshpdisj 34274 | 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 34275 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐻) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) | ||
Theorem | lshpinN 34276 | The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐻) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → ((𝑇 ∩ 𝑈) ∈ 𝐻 ↔ 𝑇 = 𝑈)) | ||
Theorem | lsatset 34277* | 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 34278* | 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 34279 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 34280 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ 𝐴) | ||
Theorem | lsatlspsn 34280 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴) | ||
Theorem | islsati 34281* | 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 34282* | 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 34283 | 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 34284 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | lsatssv 34285 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑄 ⊆ 𝑉) | ||
Theorem | lsatn0 34286 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 29204 analog.) (Contributed by NM, 25-Aug-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑈 ≠ { 0 }) | ||
Theorem | lsatspn0 34287 | The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ↔ 𝑋 ≠ 0 )) | ||
Theorem | lsator0sp 34288 | The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ∨ (𝑁‘{𝑋}) = { 0 })) | ||
Theorem | lsatssn0 34289 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑈 ≠ { 0 }) | ||
Theorem | lsatcmp 34290 | If two atoms are comparable, they are equal. (atsseq 29206 analog.) TODO: can lspsncmp 19116 shorten this? (Contributed by NM, 25-Aug-2014.) |
⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) | ||
Theorem | lsatcmp2 34291 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 34290. TODO: can lspsncmp 19116 shorten this? (Contributed by NM, 3-Feb-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐴) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 })) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) | ||
Theorem | lsatel 34292 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → 𝑈 = (𝑁‘{𝑋})) | ||
Theorem | lsatelbN 34293 | A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑈 = (𝑁‘{𝑋}))) | ||
Theorem | lsat2el 34294 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑄) ⇒ ⊢ (𝜑 → 𝑃 = 𝑄) | ||
Theorem | lsmsat 34295* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 35091 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑇 ≠ { 0 }) & ⊢ (𝜑 → 𝑄 ⊆ (𝑇 ⊕ 𝑈)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈))) | ||
Theorem | lsatfixedN 34296* | Show equality with the span of the sum of two vectors, one of which (𝑋) is fixed in advance. Compare lspfixed 19128. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋})) & ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) | ||
Theorem | lsmsatcv 34297 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 28511 analog.) Explicit atom version of lsmcv 19141. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ 𝑄)) → 𝑈 = (𝑇 ⊕ 𝑄)) | ||
Theorem | lssatomic 34298* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 29217 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ≠ { 0 }) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈) | ||
Theorem | lssats 34299* | The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. Hypothesis (shatomistici 29220 analog.) (Contributed by NM, 9-Apr-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) | ||
Theorem | lpssat 34300* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 29222 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ⊊ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |