P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axc5c711toc7 38901	Rederivation of ax-c7 38866 from axc5c711 38899. Note that ax-c7 38866 and ax-11 2154 are not used by the rederivation. The use of alimi 1807 (which uses ax-c5 38864) is allowed since we have already proved axc5c711toc5 38900. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c711to11 38902	Rederivation of ax-11 2154 from axc5c711 38899. Note that ax-c7 38866 and ax-11 2154 are not used by the rederivation. The use of alimi 1807 (which uses ax-c5 38864) is allowed since we have already proved axc5c711toc5 38900. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	equidqe 38903	equid 2008 with existential quantifier without using ax-c5 38864 or ax-5 1907. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥
Theorem	axc5sp1 38904	A special case of ax-c5 38864 without using ax-c5 38864 or ax-5 1907. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
Theorem	equidq 38905	equid 2008 with universal quantifier without using ax-c5 38864 or ax-5 1907. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑦 𝑥 = 𝑥
Theorem	equid1ALT 38906	Alternate proof of equid 2008 and equid1 38880 from older axioms ax-c7 38866, ax-c10 38867 and ax-c9 38871. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	axc11nfromc11 38907	Rederivation of ax-c11n 38869 from original version ax-c11 38868. See Theorem axc11 2432 for the derivation of ax-c11 38868 from ax-c11n 38869. This theorem should not be referenced in any proof. Instead, use ax-c11n 38869 above so that uses of ax-c11n 38869 can be more easily identified, or use aecom-o 38882 when this form is needed for studies involving ax-c11 38868 and omitting ax-5 1907. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	naecoms-o 38908	A commutation rule for distinct variable specifiers. Version of naecoms 2431 using ax-c11 38868. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbnae-o 38909	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2434 using ax-c11 38868. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	dvelimf-o 38910	Proof of dvelimh 2452 that uses ax-c11 38868 but not ax-c15 38870, ax-c11n 38869, or ax-12 2174. Version of dvelimh 2452 using ax-c11 38868 instead of axc11 2432. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dral2-o 38911	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 2440 using ax-c11 38868. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	aev-o 38912*	A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 38873. Version of aev 2054 using ax-c11 38868. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	ax5eq 38913*	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1907 considered as a metatheorem. Do not use it for later proofs - use ax-5 1907 instead, to avoid reference to the redundant axiom ax-c16 38873.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
Theorem	dveeq2-o 38914*	Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2380 using ax-c15 38870. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	axc16g-o 38915*	A generalization of Axiom ax-c16 38873. Version of axc16g 2257 using ax-c11 38868. (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 38916*	Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2382 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	dveeq1-o16 38917*	Version of dveeq1 2382 using ax-c16 38873 instead of ax-5 1907. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1907. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax5el 38918*	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1907 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)
Theorem	axc11n-16 38919*	This theorem shows that, given ax-c16 38873, we can derive a version of ax-c11n 38869. However, it is weaker than ax-c11n 38869 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
Theorem	dveel2ALT 38920*	Alternate proof of dveel2 2464 using ax-c16 38873 instead of ax-5 1907. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	ax12f 38921	Basis step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. 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 38922	Basis step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
Theorem	ax12el 38923	Basis step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
Theorem	ax12indn 38924	Induction step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑))))
Theorem	ax12indi 38925	Induction step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))))
Theorem	ax12indalem 38926	Lemma for ax12inda2 38928 and ax12inda 38929. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
Theorem	ax12inda2ALT 38927*	Alternate proof of ax12inda2 38928, slightly more direct and not requiring ax-c16 38873. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda2 38928*	Induction step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 38929. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda 38929*	Induction step for constructing a substitution instance of ax-c15 38870 without using ax-c15 38870. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 38928 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 38930*	Rederivation of ax-c15 38870 from ax12v 2175 (without using ax-c15 38870 or the full ax-12 2174). Thus, the hypothesis (ax12v 2175) provides an alternate axiom that can be used in place of ax-c15 38870. See also axc15 2424. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12a2-o 38931*	Derive ax-c15 38870 from a hypothesis in the form of ax-12 2174, without using ax-12 2174 or ax-c15 38870. The hypothesis is weaker than ax-12 2174, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2174, if we also have ax-c11 38868, which this proof uses. As Theorem ax12 2425 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 38869 instead of ax-c11 38868. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	axc11-o 38932	Show that ax-c11 38868 can be derived from ax-c11n 38869 and ax-12 2174. An open problem is whether this theorem can be derived from ax-c11n 38869 and the others when ax-12 2174 is replaced with ax-c15 38870 or ax12v 2175. See Theorems axc11nfromc11 38907 for the rederivation of ax-c11n 38869 from axc11 2432. Normally, axc11 2432 should be used rather than ax-c11 38868 or axc11-o 38932, 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 38933*	Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15812. The proof demonstrates how this can be derived starting from from fsumshft 15812. (Contributed by NM, 1-Nov-2019.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵)
Axiom	ax-riotaBAD 38934	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 6515. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7387, CONFLICTS WITH (THE NEW) df-riota 7387 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.
⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))
Theorem	riotaclbgBAD 38935*	Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴))
Theorem	riotaclbBAD 38936*	Closure of restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasvd 38937*	Deduction version of riotasv 38940. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶))
Theorem	riotasv2d 38938*	Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5408). Special case of riota2f 7411. (Contributed by NM, 2-Mar-2013.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐹)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹)
Theorem	riotasv2s 38939*	The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5408) in the form of a substitution instance. Special case of riota2f 7411. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶)
Theorem	riotasv 38940*	Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5408). Special case of riota2f 7411. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶)
Theorem	riotasv3d 38941*	A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 5408) also holds for its description binder 𝐷 (in the form of property 𝜃). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜃)    &   ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝜒))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝜃)
21.28.4  Experiments with weak deduction theorem
Theorem	elimhyps 38942	A version of elimhyp 4595 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
⊢ [𝐵 / 𝑥]𝜑    ⇒   ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑
Theorem	dedths 38943	A version of weak deduction theorem dedth 4588 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	renegclALT 38944	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11569. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
Theorem	elimhyps2 38945	Generalization of elimhyps 38942 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.)
⊢ [𝐵 / 𝑥]𝜑    ⇒   ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑
Theorem	dedths2 38946	Generalization of dedths 38943 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.)
⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)
Theorem	nfcxfrdf 38947	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfded 38948	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 3710. The last is assigned to the inference form (e.g., Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2910. (Contributed by NM, 19-Nov-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐶)
Theorem	nfded2 38949	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 4894) that starts from abidnf 3710. The last is assigned to the inference form (e.g., Ⅎ𝑥⟨{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}⟩ for nfop 4893) whose hypotheses are satisfied using nfaba1 2910. (Contributed by NM, 19-Nov-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷)    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐷)
Theorem	nfunidALT2 38950	Deduction version of nfuni 4918. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfunidALT 38951	Deduction version of nfuni 4918. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfopdALT 38952	Deduction version of bound-variable hypothesis builder nfop 4893. This shows how the deduction version of a not-free theorem such as nfop 4893 can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⟨𝐴, 𝐵⟩)
21.28.5  Miscellanea
Theorem	cnaddcom 38953	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 38954*	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‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
21.28.6  Atoms, hyperplanes, and covering in a left vector space (or module)
Syntax	clsa 38955	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 38956	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 38957*	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 38958*	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 38959*	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 38960*	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 38961*	Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉)))
Theorem	lshplss 38962	A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lshpne 38963	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ≠ 𝑉)
Theorem	lshpnel 38964	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
Theorem	lshpnelb 38965	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 38966	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉))
Theorem	lshpne0 38967	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 38968	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 38969	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lshpinN 38970	The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → ((𝑇 ∩ 𝑈) ∈ 𝐻 ↔ 𝑇 = 𝑈))
Theorem	lsatset 38971*	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 38972*	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 38973	The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 38974 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	lsatlspsn 38974	The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	islsati 38975*	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 38976*	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 38977	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 38978	An atom is a subspace. (Contributed by NM, 25-Aug-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lsatssv 38979	An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑄 ⊆ 𝑉)
Theorem	lsatn0 38980	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 32373 analog.) (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatspn0 38981	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 38982	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 38983	A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatcmp 38984	If two atoms are comparable, they are equal. (atsseq 32375 analog.) TODO: can lspsncmp 21135 shorten this? (Contributed by NM, 25-Aug-2014.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatcmp2 38985	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 38984. TODO: can lspsncmp 21135 shorten this? (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 }))    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatel 38986	A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑈 = (𝑁‘{𝑋}))
Theorem	lsatelbN 38987	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 38988	Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝑃 = 𝑄)
Theorem	lsmsat 38989*	Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 39787 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ≠ { 0 })    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)))
Theorem	lsatfixedN 38990*	Show equality with the span of the sum of two vectors, one of which (𝑋) is fixed in advance. Compare lspfixed 21147. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}))
Theorem	lsmsatcv 38991	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 31680 analog.) Explicit atom version of lsmcv 21160. (Contributed by NM, 29-Oct-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ 𝑄)) → 𝑈 = (𝑇 ⊕ 𝑄))
Theorem	lssatomic 38992*	The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 32386 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ { 0 })    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈)
Theorem	lssats 38993*	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 32389 analog.) (Contributed by NM, 9-Apr-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}))
Theorem	lpssat 38994*	Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 32391 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇))
Theorem	lrelat 38995*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32392 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊊ (𝑇 ⊕ 𝑞) ∧ (𝑇 ⊕ 𝑞) ⊆ 𝑈))
Theorem	lssatle 38996*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 32399 analog.) (Contributed by NM, 29-Oct-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈)))
Theorem	lssat 38997*	Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. (chpssati 32391 analog.) (Contributed by NM, 9-Apr-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆) ∧ 𝑈 ⊊ 𝑉) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈))
Theorem	islshpat 38998*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 38961. (Contributed by NM, 11-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ 𝐴 (𝑈 ⊕ 𝑞) = 𝑉)))
Syntax	clcv 38999	Extend class notation with the covering relation for a left module or left vector space.
class ⋖L
Definition	df-lcv 39000*	Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation 𝐴( ⋖L ‘𝑊)𝐵 is read "𝐵 covers 𝐴 " or "𝐴 is covered by 𝐵 " , and it means that 𝐵 is larger than 𝐴 and there is nothing in between. See lcvbr 39002 for binary relation. (df-cv 32307 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ ⋖L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})