P. 146 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14501-14600   *Has distinct variable group(s)

Type	Label	Description
Statement
7.3.12  Left regular elements and domains
Syntax	crlreg 14501	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 14502	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 14503	Class of integral domains.
class IDomn
Definition	df-rlreg 14504*	Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
Definition	df-domn 14505*	A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- Domn = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }
Definition	df-idom 14506	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- IDomn = ( CRing i^i Domn )
Theorem	rrgmex 14507	A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
|- E = (RLReg ` R )   =>    |- ( A e. E -> R e. _V )
Theorem	rrgval 14508*	Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- E = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }
Theorem	isrrg 14509*	Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( X e. E <-> ( X e. B /\ A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) ) )
Theorem	rrgeq0i 14510	Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> Y = .0. ) )
Theorem	rrgeq0 14511	Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )
Theorem	rrgsupp 14512	Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Revised by AV, 20-Jul-2019.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y : I --> B )   =>    |- ( ph -> ( ( ( I X. { X } ) oF .x. Y ) supp .0. ) = ( Y supp .0. ) )
Theorem	rrgss 14513	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   =>    |- E C_ B
Theorem	unitrrg 14514	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- U = (Unit ` R )   =>    |- ( R e. Ring -> U C_ E )
Theorem	rrgnz 14515	In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025.)
|- E = (RLReg ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. NzRing -> -. .0. e. E )
Theorem	isdomn 14516*	Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Domn <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
Theorem	domnnzr 14517	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. NzRing )
Theorem	domnring 14518	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. Ring )
Theorem	domneq0 14519	In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
Theorem	domnmuln0 14520	In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )
Theorem	opprdomnbg 14521	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 14522. (Contributed by SN, 15-Jun-2015.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. Domn <-> O e. Domn ) )
Theorem	opprdomn 14522	The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- O = (oppr ` R )   =>    |- ( R e. Domn -> O e. Domn )
Theorem	isidom 14523	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
Theorem	idomdomd 14524	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
|- ( ph -> R e. IDomn )   =>    |- ( ph -> R e. Domn )
Theorem	idomcringd 14525	An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) (Proof shortened by SN, 14-May-2025.)
|- ( ph -> R e. IDomn )   =>    |- ( ph -> R e. CRing )
Theorem	idomringd 14526	An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
|- ( ph -> R e. IDomn )   =>    |- ( ph -> R e. Ring )
7.4  Division rings and fields
7.4.1  Ring apartness
Syntax	capr 14527	Extend class notation with ring apartness.
class #r
Definition	df-apr 14528*	The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14536. (Contributed by Jim Kingdon, 13-Feb-2025.)
|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
Theorem	aprval 14529	Expand Definition df-apr 14528. (Contributed by Jim Kingdon, 17-Feb-2025.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> # = (#r ` R ) )   &    |- ( ph -> .- = ( -g ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X # Y <-> ( X .- Y ) e. U ) )
Theorem	aprunit 14530	The df-apr 14528 relation with zero expresses whether a ring element is a unit. That is, the difference of an element of a ring and zero is invertible iff the element is a unit. (Contributed by Jim Kingdon, 29-May-2026.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (Unit ` R )   &    |- # = (#r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X # .0. <-> X e. U ) )
Theorem	ringunitap 14531	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 14532*	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 14538). 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 14533	The apartness relation given by df-apr 14528 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 14534	The apartness relation given by df-apr 14528 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 14535	The apartness relation given by df-apr 14528 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 14536	The relation given by df-apr 14528 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 14537	If the relation given by df-apr 14528 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 14538	A ring is a local ring if and only if the relation given by df-apr 14528 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.)
|- ( R e. Ring -> ( R e. LRing <-> (#r ` R ) Ap ( Base ` R ) ) )
Theorem	aprprop 14539	If two structures have the same ring components (properties), df-apr 14528 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 14540	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 14541	Class of fields.
class Field
Definition	df-drngap 14542	Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14528 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
Definition	df-field 14543	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- Field = ( DivRing i^i CRing )
Theorem	isdrngtap 14544	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 14545	A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
|- ( R e. DivRing -> R e. LRing )
Theorem	drngunitap 14546	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 14547*	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 14548	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Ring )
Theorem	drngringd 14549	A division ring is a ring. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. DivRing )   =>    |- ( ph -> R e. Ring )
Theorem	drnggrpd 14550	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. DivRing )   =>    |- ( ph -> R e. Grp )
Theorem	drnggrp 14551	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Grp )
Theorem	isfld 14552	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 14553	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
|- ( ph -> R e. Field )   =>    |- ( ph -> R e. DivRing )
Theorem	fldcrngd 14554	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
|- ( ph -> R e. Field )   =>    |- ( ph -> R e. CRing )
Theorem	drngprop 14555	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 14556	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 14557	A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. DivRing -> R e. NzRing )
Theorem	opprdrng 14558	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 14559	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 14199, and semirings, see srg1zr 14230. (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 14560	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 14201, and semirings, see srgen1zr0 14231. (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 14561	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 14562	The functionalization of the scalar multiplication operation.
class .sf
Definition	df-lmod 14563*	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 14564*	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 14565*	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 14566	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 14567*	Properties that determine a left module. See note in isgrpd2 13776 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 14568	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 14569	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 14570	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 14571	A left module is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> W e. LMod )   =>    |- ( ph -> W e. Grp )
Theorem	lmodbn0 14572	The base set of a left module is nonempty. It is also inhabited (by lmod0vcl 14591). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- B = ( Base ` W )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodacl 14573	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 14574	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 14575	The set of scalars in a left module is nonempty. It is also inhabited, by lmod0cl 14588. (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 14576	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 14577	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 14578	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 14579	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 14580*	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 14581	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 14582	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 14583	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 14584	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 14585	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 14586	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 14587	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 14588	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 14589	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 14590	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 14591	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 14592	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 14593	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 14594	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 14595	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 14596	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 14597	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 14598	Lemma 1 for lmodfopne 14600. (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 14599	Lemma 2 for lmodfopne 14600. (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 14600	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. )