P. 139 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13801-13900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lmodvscl 13801	Closure of scalar product for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )
Theorem	scaffvalg 13802*	The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- ( W e. V -> .xb = ( x e. K , y e. B |-> ( x .x. y ) ) )
Theorem	scafvalg 13803	The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. V /\ X e. K /\ Y e. B ) -> ( X .xb Y ) = ( X .x. Y ) )
Theorem	scafeqg 13804	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.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. V /\ .x. Fn ( K X. B ) ) -> .xb = .x. )
Theorem	scaffng 13805	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   =>    |- ( W e. V -> .xb Fn ( K X. B ) )
Theorem	lmodscaf 13806	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   =>    |- ( W e. LMod -> .xb : ( K X. B ) --> B )
Theorem	lmodvsdi 13807	Distributive law for scalar product (left-distributivity). (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. LMod /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )
Theorem	lmodvsdir 13808	Distributive law for scalar product (right-distributivity). (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   =>    |- ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .+^ R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )
Theorem	lmodvsass 13809	Associative law for scalar product. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .X. = ( .r ` F )   =>    |- ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
Theorem	lmod0cl 13810	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.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .0. = ( 0g ` F )   =>    |- ( W e. LMod -> .0. e. K )
Theorem	lmod1cl 13811	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.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( W e. LMod -> .1. e. K )
Theorem	lmodvs1 13812	Scalar product with the ring unity. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- .1. = ( 1r ` F )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( .1. .x. X ) = X )
Theorem	lmod0vcl 13813	The zero vector is a vector. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( W e. LMod -> .0. e. V )
Theorem	lmod0vlid 13814	Left identity law for the zero vector. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( .0. .+ X ) = X )
Theorem	lmod0vrid 13815	Right identity law for the zero vector. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( X .+ .0. ) = X )
Theorem	lmod0vid 13816	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.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( ( X .+ X ) = X <-> .0. = X ) )
Theorem	lmod0vs 13817	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.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- O = ( 0g ` F )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) = .0. )
Theorem	lmodvs0 13818	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.)
|- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. K ) -> ( X .x. .0. ) = .0. )
Theorem	lmodvsmmulgdi 13819	Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .^ = (.g ` W )   &    |- E = (.g ` F )   =>    |- ( ( W e. LMod /\ ( C e. K /\ N e. NN0 /\ X e. V ) ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) )
Theorem	lmodfopnelem1 13820	Lemma 1 for lmodfopne 13822. (Contributed by AV, 2-Oct-2021.)
|- .x. = ( .sf ` W )   &    |- .+ = ( +f ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   =>    |- ( ( W e. LMod /\ .+ = .x. ) -> V = K )
Theorem	lmodfopnelem2 13821	Lemma 2 for lmodfopne 13822. (Contributed by AV, 2-Oct-2021.)
|- .x. = ( .sf ` W )   &    |- .+ = ( +f ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- .1. = ( 1r ` S )   =>    |- ( ( W e. LMod /\ .+ = .x. ) -> ( .0. e. V /\ .1. e. V ) )
Theorem	lmodfopne 13822	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.)
|- .x. = ( .sf ` W )   &    |- .+ = ( +f ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- .1. = ( 1r ` S )   =>    |- ( ( W e. LMod /\ .1. =/= .0. ) -> .+ =/= .x. )
Theorem	lcomf 13823	A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- B = ( Base ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> G : I --> K )   &    |- ( ph -> H : I --> B )   &    |- ( ph -> I e. V )   =>    |- ( ph -> ( G oF .x. H ) : I --> B )
Theorem	lmodvnegcl 13824	Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( invg ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` X ) e. V )
Theorem	lmodvnegid 13825	Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( invg ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( X .+ ( N ` X ) ) = .0. )
Theorem	lmodvneg1 13826	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.)
|- V = ( Base ` W )   &    |- N = ( invg ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- .1. = ( 1r ` F )   &    |- M = ( invg ` F )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( ( M ` .1. ) .x. X ) = ( N ` X ) )
Theorem	lmodvsneg 13827	Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` W )   &    |- K = ( Base ` F )   &    |- M = ( invg ` F )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. B )   &    |- ( ph -> R e. K )   =>    |- ( ph -> ( N ` ( R .x. X ) ) = ( ( M ` R ) .x. X ) )
Theorem	lmodvsubcl 13828	Closure of vector subtraction. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V )
Theorem	lmodcom 13829	Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	lmodabl 13830	A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
|- ( W e. LMod -> W e. Abel )
Theorem	lmodcmn 13831	A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.)
|- ( W e. LMod -> W e. CMnd )
Theorem	lmodnegadd 13832	Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` W )   &    |- R = (Scalar ` W )   &    |- K = ( Base ` R )   &    |- I = ( invg ` R )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( ( I ` A ) .x. X ) .+ ( ( I ` B ) .x. Y ) ) )
Theorem	lmod4 13833	Commutative/associative law for left module vector sum. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. LMod /\ ( X e. V /\ Y e. V ) /\ ( Z e. V /\ U e. V ) ) -> ( ( X .+ Y ) .+ ( Z .+ U ) ) = ( ( X .+ Z ) .+ ( Y .+ U ) ) )
Theorem	lmodvsubadd 13834	Relationship between vector subtraction and addition. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( B .+ C ) = A ) )
Theorem	lmodvaddsub4 13835	Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) = ( C .+ D ) <-> ( A .- C ) = ( D .- B ) ) )
Theorem	lmodvpncan 13836	Addition/subtraction cancellation law for vectors. (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( ( A .+ B ) .- B ) = A )
Theorem	lmodvnpcan 13837	Cancellation law for vector subtraction (Contributed by NM, 19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( ( A .- B ) .+ B ) = A )
Theorem	lmodvsubval2 13838	Value of vector subtraction in terms of addition. (Contributed by NM, 31-Mar-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( N ` .1. ) .x. B ) ) )
Theorem	lmodsubvs 13839	Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- N = ( invg ` F )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( X .- ( A .x. Y ) ) = ( X .+ ( ( N ` A ) .x. Y ) ) )
Theorem	lmodsubdi 13840	Scalar multiplication distributive law for subtraction. (Contributed by NM, 2-Jul-2014.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .- = ( -g ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( A .x. ( X .- Y ) ) = ( ( A .x. X ) .- ( A .x. Y ) ) )
Theorem	lmodsubdir 13841	Scalar multiplication distributive law for subtraction. (Contributed by NM, 2-Jul-2014.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .- = ( -g ` W )   &    |- S = ( -g ` F )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( A S B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )
Theorem	lmodsubeq0 13842	If the difference between two vectors is zero, they are equal. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( ( A .- B ) = .0. <-> A = B ) )
Theorem	lmodsubid 13843	Subtraction of a vector from itself. (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. LMod /\ A e. V ) -> ( A .- A ) = .0. )
Theorem	lmodprop2d 13844*	If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 13845 also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- F = (Scalar ` K )   &    |- G = (Scalar ` L )   &    |- ( ph -> P = ( Base ` F ) )   &    |- ( ph -> P = ( Base ` G ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .r ` F ) y ) = ( x ( .r ` G ) y ) )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   =>    |- ( ph -> ( K e. LMod <-> L e. LMod ) )
Theorem	lmodpropd 13845*	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.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ph -> F = (Scalar ` K ) )   &    |- ( ph -> F = (Scalar ` L ) )   &    |- P = ( Base ` F )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   =>    |- ( ph -> ( K e. LMod <-> L e. LMod ) )
Theorem	rmodislmodlem 13846*	Lemma for rmodislmod 13847. This is the part of the proof of rmodislmod 13847 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.)
|- V = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .s ` R )   &    |- F = (Scalar ` R )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   &    |- .X. = ( .r ` F )   &    |- .1. = ( 1r ` F )   &    |- ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) )   &    |- .* = ( s e. K , v e. V |-> ( v .x. s ) )   &    |- L = ( R sSet <. ( .s ` ndx ) , .* >. )   =>    |- ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( a .* ( b .* c ) ) )
Theorem	rmodislmod 13847*	The right module R induces a left module L 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 13785 of a left module, see also islmod 13787. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)
|- V = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .s ` R )   &    |- F = (Scalar ` R )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   &    |- .X. = ( .r ` F )   &    |- .1. = ( 1r ` F )   &    |- ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) )   &    |- .* = ( s e. K , v e. V |-> ( v .x. s ) )   &    |- L = ( R sSet <. ( .s ` ndx ) , .* >. )   =>    |- ( F e. CRing -> L e. LMod )
7.5.2  Subspaces and spans in a left module
Syntax	clss 13848	Extend class notation with linear subspaces of a left module or left vector space.
class LSubSp
Definition	df-lssm 13849*	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 = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s ) } )
Theorem	lssex 13850	Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.)
|- ( W e. V -> ( LSubSp ` W ) e. _V )
Theorem	lssmex 13851	If a linear subspace is inhabited, the class it is built from is a set. (Contributed by Jim Kingdon, 28-Apr-2025.)
|- S = ( LSubSp ` W )   =>    |- ( U e. S -> W e. _V )
Theorem	lsssetm 13852*	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.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. X -> S = { s e. ~P V | ( E. j j e. s /\ A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s ) } )
Theorem	islssm 13853*	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.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( U e. S <-> ( U C_ V /\ E. j j e. U /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
Theorem	islssmg 13854*	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.) Use islssm 13853 instead. (New usage is discouraged.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. X -> ( U e. S <-> ( U C_ V /\ E. j j e. U /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) ) )
Theorem	islssmd 13855*	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.)
|- ( ph -> F = (Scalar ` W ) )   &    |- ( ph -> B = ( Base ` F ) )   &    |- ( ph -> V = ( Base ` W ) )   &    |- ( ph -> .+ = ( +g ` W ) )   &    |- ( ph -> .x. = ( .s ` W ) )   &    |- ( ph -> S = ( LSubSp ` W ) )   &    |- ( ph -> U C_ V )   &    |- ( ph -> E. j j e. U )   &    |- ( ( ph /\ ( x e. B /\ a e. U /\ b e. U ) ) -> ( ( x .x. a ) .+ b ) e. U )   &    |- ( ph -> W e. X )   =>    |- ( ph -> U e. S )
Theorem	lssssg 13856	A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. X /\ U e. S ) -> U C_ V )
Theorem	lsselg 13857	A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. C /\ U e. S /\ X e. U ) -> X e. V )
Theorem	lss1 13858	The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> V e. S )
Theorem	lssuni 13859	The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> U. S = V )
Theorem	lssclg 13860	Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. C /\ U e. S /\ ( Z e. B /\ X e. U /\ Y e. U ) ) -> ( ( Z .x. X ) .+ Y ) e. U )
Theorem	lssvacl 13861	Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .+ = ( +g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .+ Y ) e. U )
Theorem	lssvsubcl 13862	Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .- = ( -g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .- Y ) e. U )
Theorem	lssvancl1 13863	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.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. V )   &    |- ( ph -> -. Y e. U )   =>    |- ( ph -> -. ( X .+ Y ) e. U )
Theorem	lssvancl2 13864	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.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. V )   &    |- ( ph -> -. Y e. U )   =>    |- ( ph -> -. ( Y .+ X ) e. U )
Theorem	lss0cl 13865	The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> .0. e. U )
Theorem	lsssn0 13866	The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> { .0. } e. S )
Theorem	lss0ss 13867	The zero subspace is included in every subspace. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ X e. S ) -> { .0. } C_ X )
Theorem	lssle0 13868	No subspace is smaller than the zero subspace. (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ X e. S ) -> ( X C_ { .0. } <-> X = { .0. } ) )
Theorem	lssvneln0 13869	A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 19-Jul-2022.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> X =/= .0. )
Theorem	lssneln0 13870	A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 17-Jul-2022.) (Proof shortened by AV, 19-Jul-2022.)
|- .0. = ( 0g ` W )   &    |- S = ( LSubSp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. S )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> X e. ( V \ { .0. } ) )
Theorem	lssvscl 13871	Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- B = ( Base ` F )   &    |- S = ( LSubSp ` W )   =>    |- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( X .x. Y ) e. U )
Theorem	lssvnegcl 13872	Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( invg ` W )   =>    |- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` X ) e. U )
Theorem	lsssubg 13873	All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.)
|- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> U e. (SubGrp ` W ) )
Theorem	lsssssubg 13874	All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> S C_ (SubGrp ` W ) )
Theorem	islss3 13875	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.)
|- X = ( W ↾s U )   &    |- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> ( U e. S <-> ( U C_ V /\ X e. LMod ) ) )
Theorem	lsslmod 13876	A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> X e. LMod )
Theorem	lsslss 13877	The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- T = ( LSubSp ` X )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( V e. T <-> ( V e. S /\ V C_ U ) ) )
Theorem	islss4 13878*	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.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- S = ( LSubSp ` W )   =>    |- ( W e. LMod -> ( U e. S <-> ( U e. (SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) )
Theorem	lss1d 13879*	One-dimensional subspace (or zero-dimensional if X is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } e. S )
Theorem	lssintclm 13880*	The intersection of an inhabited set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ A C_ S /\ E. w w e. A ) -> |^| A e. S )
Theorem	lssincl 13881	The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- S = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S )
Syntax	clspn 13882	Extend class notation with span of a set of vectors.
class LSpan
Definition	df-lsp 13883*	Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)
|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
Theorem	lspfval 13884*	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.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. X -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
Theorem	lspf 13885	The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> N : ~P V --> S )
Theorem	lspval 13886*	The span of a set of vectors (in a left module). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. S | U C_ t } )
Theorem	lspcl 13887	The span of a set of vectors is a subspace. (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) e. S )
Theorem	lspsncl 13888	The span of a singleton is a subspace (frequently used special case of lspcl 13887). (Contributed by NM, 17-Jul-2014.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S )
Theorem	lspprcl 13889	The span of a pair is a subspace (frequently used special case of lspcl 13887). (Contributed by NM, 11-Apr-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { X , Y } ) e. S )
Theorem	lsptpcl 13890	The span of an unordered triple is a subspace (frequently used special case of lspcl 13887). (Contributed by NM, 22-May-2015.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( N ` { X , Y , Z } ) e. S )
Theorem	lspex 13891	Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( W e. X -> ( LSpan ` W ) e. _V )
Theorem	lspsnsubg 13892	The span of a singleton is an additive subgroup (frequently used special case of lspcl 13887). (Contributed by Mario Carneiro, 21-Apr-2016.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. (SubGrp ` W ) )
Theorem	lspid 13893	The span of a subspace is itself. (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )
Theorem	lspssv 13894	A span is a set of vectors. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) C_ V )
Theorem	lspss 13895	Span preserves subset ordering. (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> ( N ` T ) C_ ( N ` U ) )
Theorem	lspssid 13896	A set of vectors is a subset of its span. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> U C_ ( N ` U ) )
Theorem	lspidm 13897	The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U C_ V ) -> ( N ` ( N ` U ) ) = ( N ` U ) )
Theorem	lspun 13898	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.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ T C_ V /\ U C_ V ) -> ( N ` ( T u. U ) ) = ( N ` ( ( N ` T ) u. ( N ` U ) ) ) )
Theorem	lspssp 13899	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.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S /\ T C_ U ) -> ( N ` T ) C_ U )
Theorem	lspsnss 13900	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.)
|- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` { X } ) C_ U )