P. 148 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ringunitap 14701	Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- # = ( #r ` R )   =>    |- ( R e. Ring -> ( X e. U <-> ( X e. B /\ X # .0. ) ) )
Theorem	ringunitsap0 14702*	The set of units of a ring. If R is a local ring, # is an apartness and this theorem states that the units of a ring are those elements apart from zero (see aprlring 14708). Given the definition of #r this theorem holds even if # is not an apartness, however. (Contributed by Jim Kingdon, 31-May-2026.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- # = ( #r ` R )   =>    |- ( R e. Ring -> { x e. B | x # .0. } = (Unit ` R ) )
Theorem	aprirr 14703	The apartness relation given by df-apr 14698 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> # = ( #r ` R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )   =>    |- ( ph -> -. X # X )
Theorem	aprsym 14704	The apartness relation given by df-apr 14698 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> # = ( #r ` R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X # Y -> Y # X ) )
Theorem	aprcotr 14705	The apartness relation given by df-apr 14698 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> # = ( #r ` R ) )   &    |- ( ph -> R e. LRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X # Y -> ( X # Z \/ Y # Z ) ) )
Theorem	aprap 14706	The relation given by df-apr 14698 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.)
|- ( R e. LRing -> ( #r ` R ) Ap ( Base ` R ) )
Theorem	aprnzr 14707	If the relation given by df-apr 14698 on a ring is an apartness relation, then the ring is a nonzero ring. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ( R e. Ring /\ ( #r ` R ) Ap ( Base ` R ) ) -> R e. NzRing )
Theorem	aprlring 14708	A ring is a local ring if and only if the relation given by df-apr 14698 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.)
|- ( R e. Ring -> ( R e. LRing <-> ( #r ` R ) Ap ( Base ` R ) ) )
Theorem	aprprop 14709	If two structures have the same ring components (properties), df-apr 14698 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 14710	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 14711	Class of fields.
class Field
Definition	df-drngap 14712	Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14698 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
|- DivRing = { r e. Ring | ( #r ` r ) TAp ( Base ` r ) }
Definition	df-field 14713	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- Field = ( DivRing i^i CRing )
Theorem	isdrngtap 14714	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 14715	A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
|- ( R e. DivRing -> R e. LRing )
Theorem	drngunitap 14716	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 14717*	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 14718	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Ring )
Theorem	drngringd 14719	A division ring is a ring. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. DivRing )   =>    |- ( ph -> R e. Ring )
Theorem	drnggrpd 14720	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. DivRing )   =>    |- ( ph -> R e. Grp )
Theorem	drnggrp 14721	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Grp )
Theorem	isfld 14722	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 14723	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
|- ( ph -> R e. Field )   =>    |- ( ph -> R e. DivRing )
Theorem	fldcrngd 14724	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
|- ( ph -> R e. Field )   =>    |- ( ph -> R e. CRing )
Theorem	drngprop 14725	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 14726	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 14727	A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. DivRing -> R e. NzRing )
Theorem	opprdrng 14728	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 14729	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 14365, and semirings, see srg1zr 14397. (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 14730	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 14367, and semirings, see srgen1zr0 14398. (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 14731	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 14732	The functionalization of the scalar multiplication operation.
class .sf
Definition	df-lmod 14733*	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 14734*	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 14735*	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 14736	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 14737*	Properties that determine a left module. See note in isgrpd2 13884 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 14738	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 14739	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 14740	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 14741	A left module is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> W e. LMod )   =>    |- ( ph -> W e. Grp )
Theorem	lmodbn0 14742	The base set of a left module is nonempty. It is also inhabited (by lmod0vcl 14762). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- B = ( Base ` W )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodacl 14743	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 14744	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 14745	The set of scalars in a left module is nonempty. It is also inhabited, by lmod0cl 14759. (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 14746	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 14747	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 14748	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 14749	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 14750	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 14751*	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 14752	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 14753	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 14754	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 14755	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 14756	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 14757	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 14758	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 14759	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 14760	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 14761	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 14762	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 14763	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 14764	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 14765	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 14766	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 14767	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 14768	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 14769	Lemma 1 for lmodfopne 14771. (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 14770	Lemma 2 for lmodfopne 14771. (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 14771	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 14772	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 14773	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 14774	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 14775	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 14776	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 14777	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 14778	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 14779	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 14780	A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.)
|- ( W e. LMod -> W e. CMnd )
Theorem	lmodnegadd 14781	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 14782	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 14783	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 14784	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 14785	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 14786	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 14787	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 14788	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 14789	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 14790	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 14791	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 14792	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 14793*	If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 14794 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 14794*	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 14795*	Lemma for rmodislmod 14796. This is the part of the proof of rmodislmod 14796 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 14796*	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 14733 of a left module, see also islmod 14735. (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 14797	Extend class notation with linear subspaces of a left module or left vector space.
class LSubSp
Definition	df-lssm 14798*	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 14799	Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.)
|- ( W e. V -> ( LSubSp ` W ) e. _V )
Theorem	lssmex 14800	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 )