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	ax12indalem 38901	Lemma for ax12inda2 38903 and ax12inda 38904. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
Theorem	ax12inda2ALT 38902*	Alternate proof of ax12inda2 38903, slightly more direct and not requiring ax-c16 38848. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda2 38903*	Induction step for constructing a substitution instance of ax-c15 38845 without using ax-c15 38845. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 38904. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda 38904*	Induction step for constructing a substitution instance of ax-c15 38845 without using ax-c15 38845. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 38903 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 38905*	Rederivation of ax-c15 38845 from ax12v 2179 (without using ax-c15 38845 or the full ax-12 2178). Thus, the hypothesis (ax12v 2179) provides an alternate axiom that can be used in place of ax-c15 38845. See also axc15 2430. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12a2-o 38906*	Derive ax-c15 38845 from a hypothesis in the form of ax-12 2178, without using ax-12 2178 or ax-c15 38845. The hypothesis is weaker than ax-12 2178, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2178, if we also have ax-c11 38843, which this proof uses. As Theorem ax12 2431 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 38844 instead of ax-c11 38843. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	axc11-o 38907	Show that ax-c11 38843 can be derived from ax-c11n 38844 and ax-12 2178. An open problem is whether this theorem can be derived from ax-c11n 38844 and the others when ax-12 2178 is replaced with ax-c15 38845 or ax12v 2179. See Theorems axc11nfromc11 38882 for the rederivation of ax-c11n 38844 from axc11 2438. Normally, axc11 2438 should be used rather than ax-c11 38843 or axc11-o 38907, 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 38908*	Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15828. The proof demonstrates how this can be derived starting from from fsumshft 15828. (Contributed by NM, 1-Nov-2019.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵)
Axiom	ax-riotaBAD 38909	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 6525. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7404, CONFLICTS WITH (THE NEW) df-riota 7404 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.
⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))
Theorem	riotaclbgBAD 38910*	Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴))
Theorem	riotaclbBAD 38911*	Closure of restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasvd 38912*	Deduction version of riotasv 38915. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶))
Theorem	riotasv2d 38913*	Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5421). Special case of riota2f 7429. (Contributed by NM, 2-Mar-2013.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐹)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹)
Theorem	riotasv2s 38914*	The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5421) in the form of a substitution instance. Special case of riota2f 7429. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶)
Theorem	riotasv 38915*	Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5421). Special case of riota2f 7429. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶)
Theorem	riotasv3d 38916*	A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 5421) 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 38917	A version of elimhyp 4613 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
⊢ [𝐵 / 𝑥]𝜑    ⇒   ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑
Theorem	dedths 38918	A version of weak deduction theorem dedth 4606 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	renegclALT 38919	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11599. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
Theorem	elimhyps2 38920	Generalization of elimhyps 38917 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.)
⊢ [𝐵 / 𝑥]𝜑    ⇒   ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑
Theorem	dedths2 38921	Generalization of dedths 38918 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.)
⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)
Theorem	nfcxfrdf 38922	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfded 38923	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 3724. The last is assigned to the inference form (e.g., Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2916. (Contributed by NM, 19-Nov-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐶)
Theorem	nfded2 38924	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 4914) that starts from abidnf 3724. The last is assigned to the inference form (e.g., Ⅎ𝑥⟨{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}⟩ for nfop 4913) whose hypotheses are satisfied using nfaba1 2916. (Contributed by NM, 19-Nov-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷)    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐷)
Theorem	nfunidALT2 38925	Deduction version of nfuni 4938. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfunidALT 38926	Deduction version of nfuni 4938. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfopdALT 38927	Deduction version of bound-variable hypothesis builder nfop 4913. This shows how the deduction version of a not-free theorem such as nfop 4913 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 38928	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 38929*	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 38930	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 38931	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 38932*	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 38933*	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 38934*	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 38935*	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 38936*	Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉)))
Theorem	lshplss 38937	A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lshpne 38938	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ≠ 𝑉)
Theorem	lshpnel 38939	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
Theorem	lshpnelb 38940	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 38941	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉))
Theorem	lshpne0 38942	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 38943	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 38944	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lshpinN 38945	The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → ((𝑇 ∩ 𝑈) ∈ 𝐻 ↔ 𝑇 = 𝑈))
Theorem	lsatset 38946*	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 38947*	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 38948	The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 38949 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	lsatlspsn 38949	The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	islsati 38950*	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 38951*	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 38952	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 38953	An atom is a subspace. (Contributed by NM, 25-Aug-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lsatssv 38954	An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑄 ⊆ 𝑉)
Theorem	lsatn0 38955	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 32377 analog.) (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatspn0 38956	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 38957	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 38958	A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatcmp 38959	If two atoms are comparable, they are equal. (atsseq 32379 analog.) TODO: can lspsncmp 21141 shorten this? (Contributed by NM, 25-Aug-2014.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatcmp2 38960	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 38959. TODO: can lspsncmp 21141 shorten this? (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 }))    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatel 38961	A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑈 = (𝑁‘{𝑋}))
Theorem	lsatelbN 38962	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 38963	Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝑃 = 𝑄)
Theorem	lsmsat 38964*	Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 39762 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ≠ { 0 })    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)))
Theorem	lsatfixedN 38965*	Show equality with the span of the sum of two vectors, one of which (𝑋) is fixed in advance. Compare lspfixed 21153. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋}))    &   ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌}))    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)}))
Theorem	lsmsatcv 38966	Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 31684 analog.) Explicit atom version of lsmcv 21166. (Contributed by NM, 29-Oct-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ 𝑄)) → 𝑈 = (𝑇 ⊕ 𝑄))
Theorem	lssatomic 38967*	The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 32390 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ { 0 })    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈)
Theorem	lssats 38968*	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 32393 analog.) (Contributed by NM, 9-Apr-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}))
Theorem	lpssat 38969*	Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 32395 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇))
Theorem	lrelat 38970*	Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32396 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊊ (𝑇 ⊕ 𝑞) ∧ (𝑇 ⊕ 𝑞) ⊆ 𝑈))
Theorem	lssatle 38971*	The ordering of two subspaces is determined by the atoms under them. (chrelat3 32403 analog.) (Contributed by NM, 29-Oct-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈)))
Theorem	lssat 38972*	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 32395 analog.) (Contributed by NM, 9-Apr-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆) ∧ 𝑈 ⊊ 𝑉) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈))
Theorem	islshpat 38973*	Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 38936. (Contributed by NM, 11-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ 𝐴 (𝑈 ⊕ 𝑞) = 𝑉)))
Syntax	clcv 38974	Extend class notation with the covering relation for a left module or left vector space.
class ⋖L
Definition	df-lcv 38975*	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 38977 for binary relation. (df-cv 32311 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ ⋖L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})
Theorem	lcvfbr 38976*	The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐶 = {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})
Theorem	lcvbr 38977*	The covers relation for a left vector space (or a left module). (cvbr 32314 analog.) (Contributed by NM, 9-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈))))
Theorem	lcvbr2 38978*	The covers relation for a left vector space (or a left module). (cvbr2 32315 analog.) (Contributed by NM, 9-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 ((𝑇 ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈))))
Theorem	lcvbr3 38979*	The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 ((𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈) → (𝑠 = 𝑇 ∨ 𝑠 = 𝑈)))))
Theorem	lcvpss 38980	The covers relation implies proper subset. (cvpss 32317 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇𝐶𝑈)    ⇒   ⊢ (𝜑 → 𝑇 ⊊ 𝑈)
Theorem	lcvnbtwn 38981	The covers relation implies no in-betweenness. (cvnbtwn 32318 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    ⇒   ⊢ (𝜑 → ¬ (𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇))
Theorem	lcvntr 38982	The covers relation is not transitive. (cvntr 32324 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    &   ⊢ (𝜑 → 𝑇𝐶𝑈)    ⇒   ⊢ (𝜑 → ¬ 𝑅𝐶𝑈)
Theorem	lcvnbtwn2 38983	The covers relation implies no in-betweenness. (cvnbtwn2 32319 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    &   ⊢ (𝜑 → 𝑅 ⊊ 𝑈)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑇)    ⇒   ⊢ (𝜑 → 𝑈 = 𝑇)
Theorem	lcvnbtwn3 38984	The covers relation implies no in-betweenness. (cvnbtwn3 32320 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅𝐶𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝑈 ⊊ 𝑇)    ⇒   ⊢ (𝜑 → 𝑈 = 𝑅)
Theorem	lsmcv2 38985	Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 32325 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ (𝑁‘{𝑋}) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈𝐶(𝑈 ⊕ (𝑁‘{𝑋})))
Theorem	lcvat 38986*	If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 32398 analog.) (Contributed by NM, 11-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇𝐶𝑈)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊕ 𝑞) = 𝑈)
Theorem	lsatcv0 38987	An atom covers the zero subspace. (atcv0 32374 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → { 0 }𝐶𝑄)
Theorem	lsatcveq0 38988	A subspace covered by an atom must be the zero subspace. (atcveq0 32380 analog.) (Contributed by NM, 7-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑈𝐶𝑄 ↔ 𝑈 = { 0 }))
Theorem	lsat0cv 38989	A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ↔ { 0 }𝐶𝑈))
Theorem	lcvexchlem1 38990	Lemma for lcvexch 38995. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑇 ⊊ (𝑇 ⊕ 𝑈) ↔ (𝑇 ∩ 𝑈) ⊊ 𝑈))
Theorem	lcvexchlem2 38991	Lemma for lcvexch 38995. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ∩ 𝑈) = 𝑅)
Theorem	lcvexchlem3 38992	Lemma for lcvexch 38995. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → ((𝑅 ∩ 𝑈) ⊕ 𝑇) = 𝑅)
Theorem	lcvexchlem4 38993	Lemma for lcvexch 38995. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇𝐶(𝑇 ⊕ 𝑈))    ⇒   ⊢ (𝜑 → (𝑇 ∩ 𝑈)𝐶𝑈)
Theorem	lcvexchlem5 38994	Lemma for lcvexch 38995. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈)𝐶𝑈)    ⇒   ⊢ (𝜑 → 𝑇𝐶(𝑇 ⊕ 𝑈))
Theorem	lcvexch 38995	Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 32401 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑇 ∩ 𝑈)𝐶𝑈 ↔ 𝑇𝐶(𝑇 ⊕ 𝑈)))
Theorem	lcvp 38996	Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32407 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑈 ∩ 𝑄) = { 0 } ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))
Theorem	lcv1 38997	Covering property of a subspace plus an atom. (chcv1 32387 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))
Theorem	lcv2 38998	Covering property of a subspace plus an atom. (chcv2 32388 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ 𝐶 = ( ⋖L ‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑈 ⊊ (𝑈 ⊕ 𝑄) ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))
Theorem	lsatexch 38999	The atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem was originally proved by Hermann Grassmann in 1862. (atexch 32413 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ (𝑈 ⊕ 𝑅))    &   ⊢ (𝜑 → (𝑈 ∩ 𝑄) = { 0 })    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (𝑈 ⊕ 𝑄))
Theorem	lsatnle 39000	The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 32408 analog.) (Contributed by NM, 10-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ (𝑈 ∩ 𝑄) = { 0 }))