P. 205 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20401-20500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lmodscaf 20401	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ∙ = ( ·sf ‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → ∙ :(𝐾 × 𝐵)⟶𝐵)
Theorem	lmodvsdi 20402	Distributive law for scalar product (left-distributivity). (ax-hvdistr1 30013 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))
Theorem	lmodvsdir 20403	Distributive law for scalar product (right-distributivity). (ax-hvdistr1 30013 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
Theorem	lmodvsass 20404	Associative law for scalar product. (ax-hvmulass 30012 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ × = (.r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
Theorem	lmod0cl 20405	The ring zero in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾)
Theorem	lmod1cl 20406	The ring unity in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod → 1 ∈ 𝐾)
Theorem	lmodvs1 20407	Scalar product with the ring unity. (ax-hvmulid 30011 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋)
Theorem	lmod0vcl 20408	The zero vector is a vector. (ax-hv0cl 30008 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉)
Theorem	lmod0vlid 20409	Left identity law for the zero vector. (hvaddlid 30028 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋)
Theorem	lmod0vrid 20410	Right identity law for the zero vector. (ax-hvaddid 30009 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + 0 ) = 𝑋)
Theorem	lmod0vid 20411	Identity equivalent to the value of the zero vector. Provides a convenient way to compute the value. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑋 + 𝑋) = 𝑋 ↔ 0 = 𝑋))
Theorem	lmod0vs 20412	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30015 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑂 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 )
Theorem	lmodvs0 20413	Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 30029 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾) → (𝑋 · 0 ) = 0 )
Theorem	lmodvsmmulgdi 20414	Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘𝑊)    &   ⊢ 𝐸 = (.g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋))
Theorem	lmodfopnelem1 20415	Lemma 1 for lmodfopne 20417. (Contributed by AV, 2-Oct-2021.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ + = (+𝑓‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾)
Theorem	lmodfopnelem2 20416	Lemma 2 for lmodfopne 20417. (Contributed by AV, 2-Oct-2021.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ + = (+𝑓‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉))
Theorem	lmodfopne 20417	The (functionalized) operations of a left module (over a nonzero ring) cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 2-Oct-2021.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ + = (+𝑓‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 1 ≠ 0 ) → + ≠ · )
Theorem	lcomf 20418	A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐾)    &   ⊢ (𝜑 → 𝐻:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · 𝐻):𝐼⟶𝐵)
Theorem	lcomfsupp 20419	A linear-combination sum is finitely supported if the coefficients are. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by AV, 15-Jul-2019.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐾)    &   ⊢ (𝜑 → 𝐻:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (0g‘𝐹)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 ∘f · 𝐻) finSupp 0 )
Theorem	lmodvnegcl 20420	Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ 𝑉)
Theorem	lmodvnegid 20421	Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + (𝑁‘𝑋)) = 0 )
Theorem	lmodvneg1 20422	Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ 𝑀 = (invg‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1 ) · 𝑋) = (𝑁‘𝑋))
Theorem	lmodvsneg 20423	Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑀 = (invg‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = ((𝑀‘𝑅) · 𝑋))
Theorem	lmodvsubcl 20424	Closure of vector subtraction. (hvsubcl 30022 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉)
Theorem	lmodcom 20425	Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	lmodabl 20426	A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
Theorem	lmodcmn 20427	A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd)
Theorem	lmodnegadd 20428	Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    &   ⊢ 𝑅 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘((𝐴 · 𝑋) + (𝐵 · 𝑌))) = (((𝐼‘𝐴) · 𝑋) + ((𝐼‘𝐵) · 𝑌)))
Theorem	lmod4 20429	Commutative/associative law for left module vector sum. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑍 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉)) → ((𝑋 + 𝑌) + (𝑍 + 𝑈)) = ((𝑋 + 𝑍) + (𝑌 + 𝑈)))
Theorem	lmodvsubadd 20430	Relationship between vector subtraction and addition. (hvsubadd 30082 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	lmodvaddsub4 20431	Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	lmodvpncan 20432	Addition/subtraction cancellation law for vectors. (hvpncan 30044 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Theorem	lmodvnpcan 20433	Cancellation law for vector subtraction (npcan 11419 analog). (Contributed by NM, 19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)
Theorem	lmodvsubval2 20434	Value of vector subtraction in terms of addition. (hvsubval 30021 analog.) (Contributed by NM, 31-Mar-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (invg‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + ((𝑁‘ 1 ) · 𝐵)))
Theorem	lmodsubvs 20435	Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (invg‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 − (𝐴 · 𝑌)) = (𝑋 + ((𝑁‘𝐴) · 𝑌)))
Theorem	lmodsubdi 20436	Scalar multiplication distributive law for subtraction. (hvsubdistr1 30054 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 · (𝑋 − 𝑌)) = ((𝐴 · 𝑋) − (𝐴 · 𝑌)))
Theorem	lmodsubdir 20437	Scalar multiplication distributive law for subtraction. (hvsubdistr2 30055 analog.) (Contributed by NM, 2-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (-g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴𝑆𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋)))
Theorem	lmodsubeq0 20438	If the difference between two vectors is zero, they are equal. (hvsubeq0 30073 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	lmodsubid 20439	Subtraction of a vector from itself. (hvsubid 30031 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉) → (𝐴 − 𝐴) = 0 )
Theorem	lmodvsghm 20440*	Scalar multiplication of the vector space by a fixed scalar is an endomorphism of the additive group of vectors. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥)) ∈ (𝑊 GrpHom 𝑊))
Theorem	lmodprop2d 20441*	If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 20442 also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ 𝐹 = (Scalar‘𝐾)    &   ⊢ 𝐺 = (Scalar‘𝐿)    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(.r‘𝐹)𝑦) = (𝑥(.r‘𝐺)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod))
Theorem	lmodpropd 20442*	If two structures have the same components (properties), one is a left module iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐾))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿))    &   ⊢ 𝑃 = (Base‘𝐹)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod))
Theorem	gsumvsmul 20443*	Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 20045, since every ring is a left module over itself. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) (Revised by AV, 10-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑆 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = (𝑋 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑌))))
Theorem	mptscmfsupp0 20444*	A mapping to a scalar product is finitely supported if the mapping to the scalar is finitely supported. (Contributed by AV, 5-Oct-2019.)
⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ LMod)    &   ⊢ (𝜑 → 𝑅 = (Scalar‘𝑄))    &   ⊢ 𝐾 = (Base‘𝑄)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑆 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑊 ∈ 𝐾)    &   ⊢ 0 = (0g‘𝑄)    &   ⊢ 𝑍 = (0g‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ 𝑆) finSupp 𝑍)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) finSupp 0 )
Theorem	mptscmfsuppd 20445*	A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe 21704. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.) (Proof shortened by AV, 18-Oct-2019.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑆 = (Scalar‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝑃 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 finSupp (0g‘𝑆))    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) · 𝑍)) finSupp (0g‘𝑃))
Theorem	rmodislmodlem 20446*	Lemma for rmodislmod 20447. This is the part of the proof of rmodislmod 20447 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ 𝐹 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))    &   ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))    &   ⊢ 𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ∗ ⟩)    ⇒   ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑎 ∗ (𝑏 ∗ 𝑐)))
Theorem	rmodislmod 20447*	The right module 𝑅 induces a left module 𝐿 by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod 20380 of a left module, see also islmod 20382. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ 𝐹 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))    &   ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))    &   ⊢ 𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ∗ ⟩)    ⇒   ⊢ (𝐹 ∈ CRing → 𝐿 ∈ LMod)
Theorem	rmodislmodOLD 20448*	Obsolete version of rmodislmod 20447 as of 18-Oct-2024. The right module 𝑅 induces a left module 𝐿 by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod 20380 of a left module, see also islmod 20382. (Contributed by AV, 3-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ 𝐹 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))    &   ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠))    &   ⊢ 𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ∗ ⟩)    ⇒   ⊢ (𝐹 ∈ CRing → 𝐿 ∈ LMod)
10.5.2  Subspaces and spans in a left module
Syntax	clss 20449	Extend class notation with linear subspaces of a left module or left vector space.
class LSubSp
Definition	df-lss 20450*	Define the set of linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)
⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})
Theorem	lssset 20451*	The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 15-Jul-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
Theorem	islss 20452*	The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈))
Theorem	islssd 20453*	Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑊))    &   ⊢ (𝜑 → + = (+g‘𝑊))    &   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))    &   ⊢ (𝜑 → 𝑆 = (LSubSp‘𝑊))    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑈 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lssss 20454	A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉)
Theorem	lssel 20455	A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑉)
Theorem	lss1 20456	The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝑆)
Theorem	lssuni 20457	The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → ∪ 𝑆 = 𝑉)
Theorem	lssn0 20458	A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑈 ≠ ∅)
Theorem	00lss 20459	The empty structure has no subspaces (for use with fvco4i 6947). (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ∅ = (LSubSp‘∅)
Theorem	lsscl 20460	Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝑆 ∧ (𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → ((𝑍 · 𝑋) + 𝑌) ∈ 𝑈)
Theorem	lssvsubcl 20461	Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) ∈ 𝑈)
Theorem	lssvancl1 20462	Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 20656. Can it be used along with lspsnne1 20637, lspsnne2 20638 to shorten this proof? (Contributed by NM, 14-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝑋 + 𝑌) ∈ 𝑈)
Theorem	lssvancl2 20463	Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 20-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝑌 + 𝑋) ∈ 𝑈)
Theorem	lss0cl 20464	The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 0 ∈ 𝑈)
Theorem	lsssn0 20465	The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → { 0 } ∈ 𝑆)
Theorem	lss0ss 20466	The zero subspace is included in every subspace. (sh0le 30445 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ 𝑋)
Theorem	lssle0 20467	No subspace is smaller than the zero subspace. (shle0 30447 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑋 ⊆ { 0 } ↔ 𝑋 = { 0 }))
Theorem	lssne0 20468*	A nonzero subspace has a nonzero vector. (shne0i 30453 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑋 ∈ 𝑆 → (𝑋 ≠ { 0 } ↔ ∃𝑦 ∈ 𝑋 𝑦 ≠ 0 ))
Theorem	lssvneln0 20469	A vector 𝑋 which doesn't belong to a subspace 𝑈 is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 19-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 0 )
Theorem	lssneln0 20470	A vector 𝑋 which doesn't belong to a subspace 𝑈 is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 17-Jul-2022.) (Proof shortened by AV, 19-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
Theorem	lssssr 20471*	Conclude subspace ordering from nonzero vector membership. (ssrdv 3953 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈))    ⇒   ⊢ (𝜑 → 𝑇 ⊆ 𝑈)
Theorem	lssvacl 20472	Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ + = (+g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈)
Theorem	lssvscl 20473	Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈)) → (𝑋 · 𝑌) ∈ 𝑈)
Theorem	lssvnegcl 20474	Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (invg‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈)
Theorem	lsssubg 20475	All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊))
Theorem	lsssssubg 20476	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊))
Theorem	islss3 20477	A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)))
Theorem	lsslmod 20478	A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod)
Theorem	lsslss 20479	The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝑋)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑉 ∈ 𝑇 ↔ (𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈)))
Theorem	islss4 20480*	A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ∈ (SubGrp‘𝑊) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝑈 (𝑎 · 𝑏) ∈ 𝑈)))
Theorem	lss1d 20481*	One-dimensional subspace (or zero-dimensional if 𝑋 is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆)
Theorem	lssintcl 20482	The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑆)
Theorem	lssincl 20483	The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ∩ 𝑈) ∈ 𝑆)
Theorem	lssmre 20484	The subspaces of a module comprise a Moore system on the vectors of the module. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (Moore‘𝐵))
Theorem	lssacs 20485	Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵))
Theorem	prdsvscacl 20486*	Pointwise scalar multiplication is closed in products of modules. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶LMod)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Scalar‘(𝑅‘𝑥)) = 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵)
Theorem	prdslmodd 20487*	The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶LMod)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆)    ⇒   ⊢ (𝜑 → 𝑌 ∈ LMod)
Theorem	pwslmod 20488	A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ LMod)
Syntax	clspn 20489	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 20490*	Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)
⊢ LSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
Theorem	lspfval 20491*	The span function for a left vector space (or a left module). (df-span 30314 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝑁 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡}))
Theorem	lspf 20492	The span operator on a left module maps subsets to subsets. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑁:𝒫 𝑉⟶𝑆)
Theorem	lspval 20493*	The span of a set of vectors (in a left module). (spanval 30338 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ 𝑆 ∣ 𝑈 ⊆ 𝑡})
Theorem	lspcl 20494	The span of a set of vectors is a subspace. (spancl 30341 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ∈ 𝑆)
Theorem	lspsncl 20495	The span of a singleton is a subspace (frequently used special case of lspcl 20494). (Contributed by NM, 17-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆)
Theorem	lspprcl 20496	The span of a pair is a subspace (frequently used special case of lspcl 20494). (Contributed by NM, 11-Apr-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆)
Theorem	lsptpcl 20497	The span of an unordered triple is a subspace (frequently used special case of lspcl 20494). (Contributed by NM, 22-May-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌, 𝑍}) ∈ 𝑆)
Theorem	lspsnsubg 20498	The span of a singleton is an additive subgroup (frequently used special case of lspcl 20494). (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊))
Theorem	00lsp 20499	fvco4i 6947 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ∅ = (LSpan‘∅)
Theorem	lspid 20500	The span of a subspace is itself. (spanid 30352 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈)