P. 142 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14101-14200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subrgring 14101	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 14102	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 14103	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> R e. Ring )
Theorem	subrgsubg 14104	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrg0 14105	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 14106	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 14107	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 14108	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 14109	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 14110	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 14111	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 14112	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 14113	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 14114	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 14115	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 14116	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 14117	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 14118*	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 14119	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 14120*	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 14121	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 14122	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 14123	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 14124	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 14125	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 14126	Restriction of the codomain of a (ring) homomorphism. resghm2b 13713 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 14127	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 14128	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 14129	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 14130*	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 14131*	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 14132	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 14133	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 14134	Class of integral domains.
class IDomn
Definition	df-rlreg 14135*	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 14136*	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 14137	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- IDomn = ( CRing i^i Domn )
Theorem	rrgmex 14138	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 14139*	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 14140*	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 14141	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 14142	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 14143	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 14144	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 14145	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 14146*	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 14147	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. NzRing )
Theorem	domnring 14148	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. Ring )
Theorem	domneq0 14149	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 14150	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 14151	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 14152. (Contributed by SN, 15-Jun-2015.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. Domn <-> O e. Domn ) )
Theorem	opprdomn 14152	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 14153	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 14154	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
|- ( ph -> R e. IDomn )   =>    |- ( ph -> R e. Domn )
Theorem	idomcringd 14155	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 14156	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 14157	Extend class notation with ring apartness.
class #r
Definition	df-apr 14158*	The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14163. (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 14159	Expand Definition df-apr 14158. (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 14160	The apartness relation given by df-apr 14158 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 14161	The apartness relation given by df-apr 14158 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 14162	The apartness relation given by df-apr 14158 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 14163	The relation given by df-apr 14158 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 14164	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 14165	The functionalization of the scalar multiplication operation.
class .sf
Definition	df-lmod 14166*	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 14167*	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 14168*	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 14169	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 14170*	Properties that determine a left module. See note in isgrpd2 13468 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 14171	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 14172	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 14173	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 14174	A left module is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> W e. LMod )   =>    |- ( ph -> W e. Grp )
Theorem	lmodbn0 14175	The base set of a left module is nonempty. It is also inhabited (by lmod0vcl 14194). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- B = ( Base ` W )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodacl 14176	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 14177	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 14178	The set of scalars in a left module is nonempty. It is also inhabited, by lmod0cl 14191. (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 14179	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 14180	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 14181	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 14182	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 14183*	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 14184	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 14185	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 14186	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 14187	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 14188	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 14189	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 14190	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 14191	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 14192	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 14193	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 14194	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 14195	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 14196	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 14197	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 14198	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 14199	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 14200	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 ) )