P. 140 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13901-14000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	issubrg 13901	The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( A e. (SubRing ` R ) <-> ( ( R e. Ring /\ ( R ↾s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) )
Theorem	subrgss 13902	A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRing ` R ) -> A C_ B )
Theorem	subrgid 13903	Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. (SubRing ` R ) )
Theorem	subrgring 13904	A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> S e. Ring )
Theorem	subrgcrng 13905	A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- S = ( R ↾s A )   =>    |- ( ( R e. CRing /\ A e. (SubRing ` R ) ) -> S e. CRing )
Theorem	subrgrcl 13906	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> R e. Ring )
Theorem	subrgsubg 13907	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrg0 13908	A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   &    |- .0. = ( 0g ` R )   =>    |- ( A e. (SubRing ` R ) -> .0. = ( 0g ` S ) )
Theorem	subrg1cl 13909	A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- .1. = ( 1r ` R )   =>    |- ( A e. (SubRing ` R ) -> .1. e. A )
Theorem	subrgbas 13910	Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> A = ( Base ` S ) )
Theorem	subrg1 13911	A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   &    |- .1. = ( 1r ` R )   =>    |- ( A e. (SubRing ` R ) -> .1. = ( 1r ` S ) )
Theorem	subrgacl 13912	A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- .+ = ( +g ` R )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )
Theorem	subrgmcl 13913	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- .x. = ( .r ` R )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )
Theorem	subrgsubm 13914	A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- M = (mulGrp ` R )   =>    |- ( A e. (SubRing ` R ) -> A e. (SubMnd ` M ) )
Theorem	subrgdvds 13915	If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- .|| = ( ||r ` R )   &    |- E = ( ||r ` S )   =>    |- ( A e. (SubRing ` R ) -> E C_ .|| )
Theorem	subrguss 13916	A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- U = (Unit ` R )   &    |- V = (Unit ` S )   =>    |- ( A e. (SubRing ` R ) -> V C_ U )
Theorem	subrginv 13917	A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- I = ( invr ` R )   &    |- U = (Unit ` S )   &    |- J = ( invr ` S )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. U ) -> ( I ` X ) = ( J ` X ) )
Theorem	subrgdv 13918	A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- ./ = (/r ` R )   &    |- U = (Unit ` S )   &    |- E = (/r ` S )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ./ Y ) = ( X E Y ) )
Theorem	subrgunit 13919	An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- U = (Unit ` R )   &    |- V = (Unit ` S )   &    |- I = ( invr ` R )   =>    |- ( A e. (SubRing ` R ) -> ( X e. V <-> ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) )
Theorem	subrgugrp 13920	The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- U = (Unit ` R )   &    |- V = (Unit ` S )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( A e. (SubRing ` R ) -> V e. (SubGrp ` G ) )
Theorem	issubrg2 13921*	Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( A e. (SubRing ` R ) <-> ( A e. (SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )
Theorem	subrgnzr 13922	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- S = ( R ↾s A )   =>    |- ( ( R e. NzRing /\ A e. (SubRing ` R ) ) -> S e. NzRing )
Theorem	subrgintm 13923*	The intersection of an inhabited collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- ( ( S C_ (SubRing ` R ) /\ E. w w e. S ) -> |^| S e. (SubRing ` R ) )
Theorem	subrgin 13924	The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- ( ( A e. (SubRing ` R ) /\ B e. (SubRing ` R ) ) -> ( A i^i B ) e. (SubRing ` R ) )
Theorem	subsubrg 13925	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> ( B e. (SubRing ` S ) <-> ( B e. (SubRing ` R ) /\ B C_ A ) ) )
Theorem	subsubrg2 13926	The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> (SubRing ` S ) = ( (SubRing ` R ) i^i ~P A ) )
Theorem	issubrg3 13927	A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- M = (mulGrp ` R )   =>    |- ( R e. Ring -> ( S e. (SubRing ` R ) <-> ( S e. (SubGrp ` R ) /\ S e. (SubMnd ` M ) ) ) )
Theorem	resrhm 13928	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- U = ( S ↾s X )   =>    |- ( ( F e. ( S RingHom T ) /\ X e. (SubRing ` S ) ) -> ( F |` X ) e. ( U RingHom T ) )
Theorem	resrhm2b 13929	Restriction of the codomain of a (ring) homomorphism. resghm2b 13516 analog. (Contributed by SN, 7-Feb-2025.)
|- U = ( T ↾s X )   =>    |- ( ( X e. (SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( S RingHom T ) <-> F e. ( S RingHom U ) ) )
Theorem	rhmeql 13930	The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. (SubRing ` S ) )
Theorem	rhmima 13931	The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( M RingHom N ) /\ X e. (SubRing ` M ) ) -> ( F " X ) e. (SubRing ` N ) )
Theorem	rnrhmsubrg 13932	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
|- ( F e. ( M RingHom N ) -> ran F e. (SubRing ` N ) )
Theorem	subrgpropd 13933*	If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-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 /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> (SubRing ` K ) = (SubRing ` L ) )
Theorem	rhmpropd 13934*	Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` J ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` M ) y ) )   =>    |- ( ph -> ( J RingHom K ) = ( L RingHom M ) )
7.3.12  Left regular elements and domains
Syntax	crlreg 13935	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 13936	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 13937	Class of integral domains.
class IDomn
Definition	df-rlreg 13938*	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 13939*	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 13940	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- IDomn = ( CRing i^i Domn )
Theorem	rrgmex 13941	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 13942*	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 13943*	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 13944	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 13945	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	rrgss 13946	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 13947	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 13948	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 13949*	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 13950	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. NzRing )
Theorem	domnring 13951	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. Ring )
Theorem	domneq0 13952	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 13953	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 13954	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 13955. (Contributed by SN, 15-Jun-2015.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. Domn <-> O e. Domn ) )
Theorem	opprdomn 13955	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 13956	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 13957	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
|- ( ph -> R e. IDomn )   =>    |- ( ph -> R e. Domn )
Theorem	idomcringd 13958	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 13959	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 13960	Extend class notation with ring apartness.
class #r
Definition	df-apr 13961*	The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 13966. (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 13962	Expand Definition df-apr 13961. (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	aprirr 13963	The apartness relation given by df-apr 13961 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 13964	The apartness relation given by df-apr 13961 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 13965	The apartness relation given by df-apr 13961 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 13966	The relation given by df-apr 13961 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.)
|- ( R e. LRing -> (#r ` R ) Ap ( Base ` R ) )
7.5  Left modules
7.5.1  Definition and basic properties
Syntax	clmod 13967	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 13968	The functionalization of the scalar multiplication operation.
class .sf
Definition	df-lmod 13969*	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 13970*	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 13971*	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 13972	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 13973*	Properties that determine a left module. See note in isgrpd2 13271 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 13974	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 13975	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 13976	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 13977	A left module is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> W e. LMod )   =>    |- ( ph -> W e. Grp )
Theorem	lmodbn0 13978	The base set of a left module is nonempty. It is also inhabited (by lmod0vcl 13997). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- B = ( Base ` W )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodacl 13979	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 13980	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 13981	The set of scalars in a left module is nonempty. It is also inhabited, by lmod0cl 13994. (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 13982	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 13983	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 13984	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 13985	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 13986*	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 13987	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 13988	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 13989	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 13990	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 13991	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 13992	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 13993	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 13994	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 13995	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 13996	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 13997	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 13998	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 13999	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 14000	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 ) )