P. 147 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aprprop 14601	If two structures have the same ring components (properties), df-apr 14590 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   &    |- ( .r ` K ) = ( .r ` L )   =>    |- ( K e. Ring -> (#r ` K ) = (#r ` L ) )
7.4.2  Definition and basic properties
Syntax	cdr 14602	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 14603	Class of fields.
class Field
Definition	df-drngap 14604	Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14590 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
Definition	df-field 14605	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- Field = ( DivRing i^i CRing )
Theorem	isdrngtap 14606	The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.)
|- B = ( Base ` R )   &    |- # = (#r ` R )   =>    |- ( R e. DivRing <-> ( R e. Ring /\ # TAp B ) )
Theorem	drnglring 14607	A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
|- ( R e. DivRing -> R e. LRing )
Theorem	drngunitap 14608	Elementhood in the set of units when R is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- # = (#r ` R )   =>    |- ( R e. DivRing -> ( X e. U <-> ( X e. B /\ X # .0. ) ) )
Theorem	drnguiap 14609*	The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- # = (#r ` R )   =>    |- ( R e. DivRing -> { x e. B | x # .0. } = (Unit ` R ) )
Theorem	drngring 14610	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Ring )
Theorem	drngringd 14611	A division ring is a ring. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. DivRing )   =>    |- ( ph -> R e. Ring )
Theorem	drnggrpd 14612	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. DivRing )   =>    |- ( ph -> R e. Grp )
Theorem	drnggrp 14613	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Grp )
Theorem	isfld 14614	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
Theorem	flddrngd 14615	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
|- ( ph -> R e. Field )   =>    |- ( ph -> R e. DivRing )
Theorem	fldcrngd 14616	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
|- ( ph -> R e. Field )   =>    |- ( ph -> R e. CRing )
Theorem	drngprop 14617	If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 28-Dec-2014.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   &    |- ( .r ` K ) = ( .r ` L )   =>    |- ( K e. DivRing <-> L e. DivRing )
Theorem	drngunz 14618	A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011.)
|- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. DivRing -> .1. =/= .0. )
Theorem	drngnzr 14619	A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. DivRing -> R e. NzRing )
Theorem	opprdrng 14620	The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.)
|- O = (oppr ` R )   =>    |- ( R e. DivRing <-> O e. DivRing )
Theorem	ring1zr 14621	The only unital ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rng1zr 14259, and semirings, see srg1zr 14291. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 7-Feb-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	ringen1zr0 14622	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14261, and semirings, see srgen1zr0 14292. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- Z = ( 0g ` R )   =>    |- ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
7.5  Left modules
7.5.1  Definition and basic properties
Syntax	clmod 14623	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 14624	The functionalization of the scalar multiplication operation.
class .sf
Definition	df-lmod 14625*	Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.)
|- LMod = { g e. Grp | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) ) }
Definition	df-scaf 14626*	Define the functionalization of the .s operator. This restricts the value of .s to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
Theorem	islmod 14627*	The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   &    |- .X. = ( .r ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( W e. LMod <-> ( W e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) ) )
Theorem	lmodlema 14628	Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   &    |- .X. = ( .r ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( ( W e. LMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) )
Theorem	islmodd 14629*	Properties that determine a left module. See note in isgrpd2 13826 regarding the ph on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)
|- ( ph -> V = ( Base ` W ) )   &    |- ( ph -> .+ = ( +g ` W ) )   &    |- ( ph -> F = (Scalar ` W ) )   &    |- ( ph -> .x. = ( .s ` W ) )   &    |- ( ph -> B = ( Base ` F ) )   &    |- ( ph -> .+^ = ( +g ` F ) )   &    |- ( ph -> .X. = ( .r ` F ) )   &    |- ( ph -> .1. = ( 1r ` F ) )   &    |- ( ph -> F e. Ring )   &    |- ( ph -> W e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. V ) -> ( x .x. y ) e. V )   &    |- ( ( ph /\ ( x e. B /\ y e. V /\ z e. V ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )   &    |- ( ( ph /\ x e. V ) -> ( .1. .x. x ) = x )   =>    |- ( ph -> W e. LMod )
Theorem	lmodgrp 14630	A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
|- ( W e. LMod -> W e. Grp )
Theorem	lmodring 14631	The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   =>    |- ( W e. LMod -> F e. Ring )
Theorem	lmodfgrp 14632	The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   =>    |- ( W e. LMod -> F e. Grp )
Theorem	lmodgrpd 14633	A left module is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> W e. LMod )   =>    |- ( ph -> W e. Grp )
Theorem	lmodbn0 14634	The base set of a left module is nonempty. It is also inhabited (by lmod0vcl 14654). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- B = ( Base ` W )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodacl 14635	Closure of ring addition for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .+ = ( +g ` F )   =>    |- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )
Theorem	lmodmcl 14636	Closure of ring multiplication for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .r ` F )   =>    |- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K )
Theorem	lmodsn0 14637	The set of scalars in a left module is nonempty. It is also inhabited, by lmod0cl 14651. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodvacl 14638	Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (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	lmodass 14639	Left module vector sum is associative. (Contributed by NM, 10-Jan-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 ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	lmodlcan 14640	Left cancellation law for vector sum. (Contributed by NM, 12-Jan-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 ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) <-> X = Y ) )
Theorem	lmodvscl 14641	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	lmodvscld 14642	Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> R e. K )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( R .x. X ) e. V )
Theorem	scaffvalg 14643*	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 14644	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 14645	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 14646	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 14647	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 14648	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 14649	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 14650	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 14651	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 14652	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 14653	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 14654	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 14655	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 14656	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 14657	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 14658	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 14659	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 14660	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 14661	Lemma 1 for lmodfopne 14663. (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 14662	Lemma 2 for lmodfopne 14663. (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 14663	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 14664	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 14665	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 14666	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 14667	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 14668	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 14669	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 14670	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 14671	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 14672	A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.)
|- ( W e. LMod -> W e. CMnd )
Theorem	lmodnegadd 14673	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 14674	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 14675	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 14676	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 14677	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 14678	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 14679	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 14680	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 14681	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 14682	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 14683	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 14684	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 14685*	If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 14686 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 14686*	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 14687*	Lemma for rmodislmod 14688. This is the part of the proof of rmodislmod 14688 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 14688*	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 14625 of a left module, see also islmod 14627. (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 14689	Extend class notation with linear subspaces of a left module or left vector space.
class LSubSp
Definition	df-lssm 14690*	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 14691	Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.)
|- ( W e. V -> ( LSubSp ` W ) e. _V )
Theorem	lssmex 14692	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 14693*	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 14694*	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 14695*	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 14694 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 14696*	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 14697	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 14698	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 14699	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 14700	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 )