HomeHome Intuitionistic Logic Explorer
Theorem List (p. 135 of 150)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 13401-13500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremscaffvalg 13401* The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.)
𝐡 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ™ = ( Β·sf β€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    β‡’   (π‘Š ∈ 𝑉 β†’ βˆ™ = (π‘₯ ∈ 𝐾, 𝑦 ∈ 𝐡 ↦ (π‘₯ Β· 𝑦)))
 
Theoremscafvalg 13402 The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ™ = ( Β·sf β€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    β‡’   ((π‘Š ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 βˆ™ π‘Œ) = (𝑋 Β· π‘Œ))
 
Theoremscafeqg 13403 If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ™ = ( Β·sf β€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    β‡’   ((π‘Š ∈ 𝑉 ∧ Β· Fn (𝐾 Γ— 𝐡)) β†’ βˆ™ = Β· )
 
Theoremscaffng 13404 The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ™ = ( Β·sf β€˜π‘Š)    β‡’   (π‘Š ∈ 𝑉 β†’ βˆ™ Fn (𝐾 Γ— 𝐡))
 
Theoremlmodscaf 13405 The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ™ = ( Β·sf β€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ βˆ™ :(𝐾 Γ— 𝐡)⟢𝐡)
 
Theoremlmodvsdi 13406 Distributive law for scalar product (left-distributivity). (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    β‡’   ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉)) β†’ (𝑅 Β· (𝑋 + π‘Œ)) = ((𝑅 Β· 𝑋) + (𝑅 Β· π‘Œ)))
 
Theoremlmodvsdir 13407 Distributive law for scalar product (right-distributivity). (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    ⨣ = (+gβ€˜πΉ)    β‡’   ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋)))
 
Theoremlmodvsass 13408 Associative law for scalar product. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    Γ— = (.rβ€˜πΉ)    β‡’   ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)))
 
Theoremlmod0cl 13409 The ring zero in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝐹 = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    0 = (0gβ€˜πΉ)    β‡’   (π‘Š ∈ LMod β†’ 0 ∈ 𝐾)
 
Theoremlmod1cl 13410 The ring unity in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝐹 = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    1 = (1rβ€˜πΉ)    β‡’   (π‘Š ∈ LMod β†’ 1 ∈ 𝐾)
 
Theoremlmodvs1 13411 Scalar product with the ring unity. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &    1 = (1rβ€˜πΉ)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ( 1 Β· 𝑋) = 𝑋)
 
Theoremlmod0vcl 13412 The zero vector is a vector. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ 0 ∈ 𝑉)
 
Theoremlmod0vlid 13413 Left identity law for the zero vector. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ( 0 + 𝑋) = 𝑋)
 
Theoremlmod0vrid 13414 Right identity law for the zero vector. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑋 + 0 ) = 𝑋)
 
Theoremlmod0vid 13415 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 = 𝑋))
 
Theoremlmod0vs 13416 Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘‚ = (0gβ€˜πΉ)    &    0 = (0gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) = 0 )
 
Theoremlmodvs0 13417 Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝐹 = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    0 = (0gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝐾) β†’ (𝑋 Β· 0 ) = 0 )
 
Theoremlmodvsmmulgdi 13418 Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.)
𝑉 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    ↑ = (.gβ€˜π‘Š)    &   πΈ = (.gβ€˜πΉ)    β‡’   ((π‘Š ∈ LMod ∧ (𝐢 ∈ 𝐾 ∧ 𝑁 ∈ β„•0 ∧ 𝑋 ∈ 𝑉)) β†’ (𝑁 ↑ (𝐢 Β· 𝑋)) = ((𝑁𝐸𝐢) Β· 𝑋))
 
Theoremlmodfopnelem1 13419 Lemma 1 for lmodfopne 13421. (Contributed by AV, 2-Oct-2021.)
Β· = ( Β·sf β€˜π‘Š)    &    + = (+π‘“β€˜π‘Š)    &   π‘‰ = (Baseβ€˜π‘Š)    &   π‘† = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜π‘†)    β‡’   ((π‘Š ∈ LMod ∧ + = Β· ) β†’ 𝑉 = 𝐾)
 
Theoremlmodfopnelem2 13420 Lemma 2 for lmodfopne 13421. (Contributed by AV, 2-Oct-2021.)
Β· = ( Β·sf β€˜π‘Š)    &    + = (+π‘“β€˜π‘Š)    &   π‘‰ = (Baseβ€˜π‘Š)    &   π‘† = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜π‘†)    &    0 = (0gβ€˜π‘†)    &    1 = (1rβ€˜π‘†)    β‡’   ((π‘Š ∈ LMod ∧ + = Β· ) β†’ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉))
 
Theoremlmodfopne 13421 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 ) β†’ + β‰  Β· )
 
Theoremlcomf 13422 A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
𝐹 = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π΅ = (Baseβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝐺:𝐼⟢𝐾)    &   (πœ‘ β†’ 𝐻:𝐼⟢𝐡)    &   (πœ‘ β†’ 𝐼 ∈ 𝑉)    β‡’   (πœ‘ β†’ (𝐺 βˆ˜π‘“ Β· 𝐻):𝐼⟢𝐡)
 
Theoremlmodvnegcl 13423 Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (invgβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜π‘‹) ∈ 𝑉)
 
Theoremlmodvnegid 13424 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 )
 
Theoremlmodvneg1 13425 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 ) Β· 𝑋) = (π‘β€˜π‘‹))
 
Theoremlmodvsneg 13426 Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
𝐡 = (Baseβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘ = (invgβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &   π‘€ = (invgβ€˜πΉ)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    &   (πœ‘ β†’ 𝑅 ∈ 𝐾)    β‡’   (πœ‘ β†’ (π‘β€˜(𝑅 Β· 𝑋)) = ((π‘€β€˜π‘…) Β· 𝑋))
 
Theoremlmodvsubcl 13427 Closure of vector subtraction. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉) β†’ (𝑋 βˆ’ π‘Œ) ∈ 𝑉)
 
Theoremlmodcom 13428 Left module vector sum is commutative. (Contributed by GΓ©rard Lang, 25-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉) β†’ (𝑋 + π‘Œ) = (π‘Œ + 𝑋))
 
Theoremlmodabl 13429 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)
 
Theoremlmodcmn 13430 A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.)
(π‘Š ∈ LMod β†’ π‘Š ∈ CMnd)
 
Theoremlmodnegadd 13431 Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘ = (invgβ€˜π‘Š)    &   π‘… = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜π‘…)    &   πΌ = (invgβ€˜π‘…)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝐴 ∈ 𝐾)    &   (πœ‘ β†’ 𝐡 ∈ 𝐾)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜((𝐴 Β· 𝑋) + (𝐡 Β· π‘Œ))) = (((πΌβ€˜π΄) Β· 𝑋) + ((πΌβ€˜π΅) Β· π‘Œ)))
 
Theoremlmod4 13432 Commutative/associative law for left module vector sum. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ π‘Œ ∈ 𝑉) ∧ (𝑍 ∈ 𝑉 ∧ π‘ˆ ∈ 𝑉)) β†’ ((𝑋 + π‘Œ) + (𝑍 + π‘ˆ)) = ((𝑋 + 𝑍) + (π‘Œ + π‘ˆ)))
 
Theoremlmodvsubadd 13433 Relationship between vector subtraction and addition. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉)) β†’ ((𝐴 βˆ’ 𝐡) = 𝐢 ↔ (𝐡 + 𝐢) = 𝐴))
 
Theoremlmodvaddsub4 13434 Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉) ∧ (𝐢 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) β†’ ((𝐴 + 𝐡) = (𝐢 + 𝐷) ↔ (𝐴 βˆ’ 𝐢) = (𝐷 βˆ’ 𝐡)))
 
Theoremlmodvpncan 13435 Addition/subtraction cancellation law for vectors. (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉) β†’ ((𝐴 + 𝐡) βˆ’ 𝐡) = 𝐴)
 
Theoremlmodvnpcan 13436 Cancellation law for vector subtraction (Contributed by NM, 19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉) β†’ ((𝐴 βˆ’ 𝐡) + 𝐡) = 𝐴)
 
Theoremlmodvsubval2 13437 Value of vector subtraction in terms of addition. (Contributed by NM, 31-Mar-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘ = (invgβ€˜πΉ)    &    1 = (1rβ€˜πΉ)    β‡’   ((π‘Š ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉) β†’ (𝐴 βˆ’ 𝐡) = (𝐴 + ((π‘β€˜ 1 ) Β· 𝐡)))
 
Theoremlmodsubvs 13438 Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &   π‘ = (invgβ€˜πΉ)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝐴 ∈ 𝐾)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ (𝑋 βˆ’ (𝐴 Β· π‘Œ)) = (𝑋 + ((π‘β€˜π΄) Β· π‘Œ)))
 
Theoremlmodsubdi 13439 Scalar multiplication distributive law for subtraction. (Contributed by NM, 2-Jul-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ’ = (-gβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝐴 ∈ 𝐾)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ (𝐴 Β· (𝑋 βˆ’ π‘Œ)) = ((𝐴 Β· 𝑋) βˆ’ (𝐴 Β· π‘Œ)))
 
Theoremlmodsubdir 13440 Scalar multiplication distributive law for subtraction. (Contributed by NM, 2-Jul-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   πΉ = (Scalarβ€˜π‘Š)    &   πΎ = (Baseβ€˜πΉ)    &    βˆ’ = (-gβ€˜π‘Š)    &   π‘† = (-gβ€˜πΉ)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝐴 ∈ 𝐾)    &   (πœ‘ β†’ 𝐡 ∈ 𝐾)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    β‡’   (πœ‘ β†’ ((𝐴𝑆𝐡) Β· 𝑋) = ((𝐴 Β· 𝑋) βˆ’ (𝐡 Β· 𝑋)))
 
Theoremlmodsubeq0 13441 If the difference between two vectors is zero, they are equal. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐡 ∈ 𝑉) β†’ ((𝐴 βˆ’ 𝐡) = 0 ↔ 𝐴 = 𝐡))
 
Theoremlmodsubid 13442 Subtraction of a vector from itself. (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &    0 = (0gβ€˜π‘Š)    &    βˆ’ = (-gβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝐴 ∈ 𝑉) β†’ (𝐴 βˆ’ 𝐴) = 0 )
 
Theoremlmodprop2d 13443* If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 13444 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))
 
Theoremlmodpropd 13444* 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))
 
Theoremrmodislmodlem 13445* Lemma for rmodislmod 13446. This is the part of the proof of rmodislmod 13446 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 ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (π‘Ž βˆ— (𝑏 βˆ— 𝑐)))
 
Theoremrmodislmod 13446* 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 13384 of a left module, see also islmod 13386. (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)
 
7.5.2  Subspaces and spans in a left module
 
Syntaxclss 13447 Extend class notation with linear subspaces of a left module or left vector space.
class LSubSp
 
Definitiondf-lssm 13448* A linear subspace of a left module or left vector space is an inhabited (in contrast to non-empty for non-intuitionistic logic) subset of the base set of the left-module/vector space with a closure condition on vector addition and scalar multiplication. (Contributed by NM, 8-Dec-2013.)
LSubSp = (𝑀 ∈ V ↦ {𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ∣ (βˆƒπ‘— 𝑗 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘€))βˆ€π‘Ž ∈ 𝑠 βˆ€π‘ ∈ 𝑠 ((π‘₯( ·𝑠 β€˜π‘€)π‘Ž)(+gβ€˜π‘€)𝑏) ∈ 𝑠)})
 
Theoremlsssetm 13449* 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β€˜π‘Š)    β‡’   (π‘Š ∈ 𝑋 β†’ 𝑆 = {𝑠 ∈ 𝒫 𝑉 ∣ (βˆƒπ‘— 𝑗 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ž ∈ 𝑠 βˆ€π‘ ∈ 𝑠 ((π‘₯ Β· π‘Ž) + 𝑏) ∈ 𝑠)})
 
Theoremislssm 13450* 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β€˜π‘Š)    β‡’   (π‘Š ∈ 𝑋 β†’ (π‘ˆ ∈ 𝑆 ↔ (π‘ˆ βŠ† 𝑉 ∧ βˆƒπ‘— 𝑗 ∈ π‘ˆ ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ž ∈ π‘ˆ βˆ€π‘ ∈ π‘ˆ ((π‘₯ Β· π‘Ž) + 𝑏) ∈ π‘ˆ)))
 
Theoremislssmd 13451* 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β€˜π‘Š))    &   (πœ‘ β†’ π‘ˆ βŠ† 𝑉)    &   (πœ‘ β†’ βˆƒπ‘— 𝑗 ∈ π‘ˆ)    &   ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ž ∈ π‘ˆ ∧ 𝑏 ∈ π‘ˆ)) β†’ ((π‘₯ Β· π‘Ž) + 𝑏) ∈ π‘ˆ)    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ π‘ˆ ∈ 𝑆)
 
Theoremlssssg 13452 A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ 𝑋 ∧ π‘ˆ ∈ 𝑆) β†’ π‘ˆ βŠ† 𝑉)
 
Theoremlsselg 13453 A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ 𝐢 ∧ π‘ˆ ∈ 𝑆 ∧ 𝑋 ∈ π‘ˆ) β†’ 𝑋 ∈ 𝑉)
 
Theoremlss1 13454 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 β†’ 𝑉 ∈ 𝑆)
 
Theoremlssuni 13455 The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    β‡’   (πœ‘ β†’ βˆͺ 𝑆 = 𝑉)
 
Theoremlssclg 13456 Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
𝐹 = (Scalarβ€˜π‘Š)    &   π΅ = (Baseβ€˜πΉ)    &    + = (+gβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ 𝐢 ∧ π‘ˆ ∈ 𝑆 ∧ (𝑍 ∈ 𝐡 ∧ 𝑋 ∈ π‘ˆ ∧ π‘Œ ∈ π‘ˆ)) β†’ ((𝑍 Β· 𝑋) + π‘Œ) ∈ π‘ˆ)
 
Theoremlssvsubcl 13457 Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
βˆ’ = (-gβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   (((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) ∧ (𝑋 ∈ π‘ˆ ∧ π‘Œ ∈ π‘ˆ)) β†’ (𝑋 βˆ’ π‘Œ) ∈ π‘ˆ)
 
Theoremlssvancl1 13458 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, 14-May-2015.)
𝑉 = (Baseβ€˜π‘Š)    &    + = (+gβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ π‘ˆ ∈ 𝑆)    &   (πœ‘ β†’ 𝑋 ∈ π‘ˆ)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    &   (πœ‘ β†’ Β¬ π‘Œ ∈ π‘ˆ)    β‡’   (πœ‘ β†’ Β¬ (𝑋 + π‘Œ) ∈ π‘ˆ)
 
Theoremlssvancl2 13459 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)    &   (πœ‘ β†’ π‘ˆ ∈ 𝑆)    &   (πœ‘ β†’ 𝑋 ∈ π‘ˆ)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    &   (πœ‘ β†’ Β¬ π‘Œ ∈ π‘ˆ)    β‡’   (πœ‘ β†’ Β¬ (π‘Œ + 𝑋) ∈ π‘ˆ)
 
Theoremlss0cl 13460 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 ∈ π‘ˆ)
 
Theoremlsssn0 13461 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 } ∈ 𝑆)
 
Theoremlss0ss 13462 The zero subspace is included in every subspace. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
0 = (0gβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑆) β†’ { 0 } βŠ† 𝑋)
 
Theoremlssle0 13463 No subspace is smaller than the zero subspace. (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
0 = (0gβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑆) β†’ (𝑋 βŠ† { 0 } ↔ 𝑋 = { 0 }))
 
Theoremlssvneln0 13464 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 )
 
Theoremlssneln0 13465 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 }))
 
Theoremlssvacl 13466 Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
+ = (+gβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   (((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) ∧ (𝑋 ∈ π‘ˆ ∧ π‘Œ ∈ π‘ˆ)) β†’ (𝑋 + π‘Œ) ∈ π‘ˆ)
 
Theoremlssvscl 13467 Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝐹 = (Scalarβ€˜π‘Š)    &    Β· = ( ·𝑠 β€˜π‘Š)    &   π΅ = (Baseβ€˜πΉ)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   (((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ π‘ˆ)) β†’ (𝑋 Β· π‘Œ) ∈ π‘ˆ)
 
Theoremlssvnegcl 13468 Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    &   π‘ = (invgβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆 ∧ 𝑋 ∈ π‘ˆ) β†’ (π‘β€˜π‘‹) ∈ π‘ˆ)
 
Theoremlsssubg 13469 All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) β†’ π‘ˆ ∈ (SubGrpβ€˜π‘Š))
 
Theoremlsssssubg 13470 All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
𝑆 = (LSubSpβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ 𝑆 βŠ† (SubGrpβ€˜π‘Š))
 
Theoremislss3 13471 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)))
 
Theoremlsslmod 13472 A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
𝑋 = (π‘Š β†Ύs π‘ˆ)    &   π‘† = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) β†’ 𝑋 ∈ LMod)
 
Theoremlsslss 13473 The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
𝑋 = (π‘Š β†Ύs π‘ˆ)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘‡ = (LSubSpβ€˜π‘‹)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) β†’ (𝑉 ∈ 𝑇 ↔ (𝑉 ∈ 𝑆 ∧ 𝑉 βŠ† π‘ˆ)))
 
Theoremislss4 13474* 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β€˜π‘Š) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ π‘ˆ (π‘Ž Β· 𝑏) ∈ π‘ˆ)))
 
Theoremlss1d 13475* 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 ∧ 𝑋 ∈ 𝑉) β†’ {𝑣 ∣ βˆƒπ‘˜ ∈ 𝐾 𝑣 = (π‘˜ Β· 𝑋)} ∈ 𝑆)
 
Theoremlssintclm 13476* The intersection of an inhabited set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝐴 βŠ† 𝑆 ∧ βˆƒπ‘€ 𝑀 ∈ 𝐴) β†’ ∩ 𝐴 ∈ 𝑆)
 
Theoremlssincl 13477 The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ π‘ˆ ∈ 𝑆) β†’ (𝑇 ∩ π‘ˆ) ∈ 𝑆)
 
Syntaxclspn 13478 Extend class notation with span of a set of vectors.
class LSpan
 
Definitiondf-lsp 13479* 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β€˜π‘€) ∣ 𝑠 βŠ† 𝑑}))
 
Theoremlspfval 13480* The span function for a left vector space (or a left module). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   (π‘Š ∈ 𝑋 β†’ 𝑁 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑑 ∈ 𝑆 ∣ 𝑠 βŠ† 𝑑}))
 
Theoremlspf 13481 The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   (π‘Š ∈ LMod β†’ 𝑁:𝒫 π‘‰βŸΆπ‘†)
 
Theoremlspval 13482* The span of a set of vectors (in a left module). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ βŠ† 𝑉) β†’ (π‘β€˜π‘ˆ) = ∩ {𝑑 ∈ 𝑆 ∣ π‘ˆ βŠ† 𝑑})
 
Theoremlspcl 13483 The span of a set of vectors is a subspace. (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ βŠ† 𝑉) β†’ (π‘β€˜π‘ˆ) ∈ 𝑆)
 
Theoremlspsncl 13484 The span of a singleton is a subspace (frequently used special case of lspcl 13483). (Contributed by NM, 17-Jul-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜{𝑋}) ∈ 𝑆)
 
Theoremlspprcl 13485 The span of a pair is a subspace (frequently used special case of lspcl 13483). (Contributed by NM, 11-Apr-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜{𝑋, π‘Œ}) ∈ 𝑆)
 
Theoremlsptpcl 13486 The span of an unordered triple is a subspace (frequently used special case of lspcl 13483). (Contributed by NM, 22-May-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    &   (πœ‘ β†’ 𝑍 ∈ 𝑉)    β‡’   (πœ‘ β†’ (π‘β€˜{𝑋, π‘Œ, 𝑍}) ∈ 𝑆)
 
Theoremlspsnsubg 13487 The span of a singleton is an additive subgroup (frequently used special case of lspcl 13483). (Contributed by Mario Carneiro, 21-Apr-2016.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (π‘β€˜{𝑋}) ∈ (SubGrpβ€˜π‘Š))
 
Theoremlspid 13488 The span of a subspace is itself. (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆) β†’ (π‘β€˜π‘ˆ) = π‘ˆ)
 
Theoremlspssv 13489 A span is a set of vectors. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ βŠ† 𝑉) β†’ (π‘β€˜π‘ˆ) βŠ† 𝑉)
 
Theoremlspss 13490 Span preserves subset ordering. (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ βŠ† 𝑉 ∧ 𝑇 βŠ† π‘ˆ) β†’ (π‘β€˜π‘‡) βŠ† (π‘β€˜π‘ˆ))
 
Theoremlspssid 13491 A set of vectors is a subset of its span. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ βŠ† 𝑉) β†’ π‘ˆ βŠ† (π‘β€˜π‘ˆ))
 
Theoremlspidm 13492 The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ βŠ† 𝑉) β†’ (π‘β€˜(π‘β€˜π‘ˆ)) = (π‘β€˜π‘ˆ))
 
Theoremlspun 13493 The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑇 βŠ† 𝑉 ∧ π‘ˆ βŠ† 𝑉) β†’ (π‘β€˜(𝑇 βˆͺ π‘ˆ)) = (π‘β€˜((π‘β€˜π‘‡) βˆͺ (π‘β€˜π‘ˆ))))
 
Theoremlspssp 13494 If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆 ∧ 𝑇 βŠ† π‘ˆ) β†’ (π‘β€˜π‘‡) βŠ† π‘ˆ)
 
Theoremlspsnss 13495 The span of the singleton of a subspace member is included in the subspace. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝑆 ∧ 𝑋 ∈ π‘ˆ) β†’ (π‘β€˜{𝑋}) βŠ† π‘ˆ)
 
Theoremlspsnel3 13496 A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 4-Jul-2014.)
𝑆 = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ π‘ˆ ∈ 𝑆)    &   (πœ‘ β†’ 𝑋 ∈ π‘ˆ)    &   (πœ‘ β†’ π‘Œ ∈ (π‘β€˜{𝑋}))    β‡’   (πœ‘ β†’ π‘Œ ∈ π‘ˆ)
 
Theoremlspprss 13497 The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015.)
𝑆 = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ π‘ˆ ∈ 𝑆)    &   (πœ‘ β†’ 𝑋 ∈ π‘ˆ)    &   (πœ‘ β†’ π‘Œ ∈ π‘ˆ)    β‡’   (πœ‘ β†’ (π‘β€˜{𝑋, π‘Œ}) βŠ† π‘ˆ)
 
Theoremlspsnid 13498 A vector belongs to the span of its singleton. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝑋 ∈ (π‘β€˜{𝑋}))
 
Theoremlspsnel6 13499 Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ π‘ˆ ∈ 𝑆)    β‡’   (πœ‘ β†’ (𝑋 ∈ π‘ˆ ↔ (𝑋 ∈ 𝑉 ∧ (π‘β€˜{𝑋}) βŠ† π‘ˆ)))
 
Theoremlspsnel5 13500 Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.)
𝑉 = (Baseβ€˜π‘Š)    &   π‘† = (LSubSpβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘Š)    &   (πœ‘ β†’ π‘Š ∈ LMod)    &   (πœ‘ β†’ π‘ˆ ∈ 𝑆)    &   (πœ‘ β†’ 𝑋 ∈ 𝑉)    β‡’   (πœ‘ β†’ (𝑋 ∈ π‘ˆ ↔ (π‘β€˜{𝑋}) βŠ† π‘ˆ))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-14917
  Copyright terms: Public domain < Previous  Next >