P. 385 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38401-38500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	irinitoringc 38401	The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> ℤring e. U )   &    |- C = (RingCat ` U )   =>    |- ( ph -> ℤring e. (InitO ` C ) )
Theorem	zrtermoringc 38402	The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (TermO ` C ) )
Theorem	zrninitoringc 38403*	The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   &    |- ( ph -> E. r e. ( Base ` C ) r e. NzRing )   =>    |- ( ph -> Z e/ (InitO ` C ) )
Theorem	nzerooringczr 38404	There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   &    |- ( ph -> ℤring e. U )   =>    |- ( ph -> (ZeroO ` C ) = (/) )
21.33.12.10  Subcategories of the category of rings
Theorem	srhmsubclem1 38405*	Lemma 1 for srhmsubc 38408. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( X e. C -> X e. ( U i^i Ring ) )
Theorem	srhmsubclem2 38406*	Lemma 2 for srhmsubc 38408. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( ( U e. V /\ X e. C ) -> X e. ( Base ` (RingCat ` U ) ) )
Theorem	srhmsubclem3 38407*	Lemma 3 for srhmsubc 38408. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` (RingCat ` U ) ) Y ) )
Theorem	srhmsubc 38408*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	sringcat 38409*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	crhmsubc 38410*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	cringcat 38411*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	drhmsubc 38412*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	drngcat 38413*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	fldcat 38414*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat F ) e. Cat )
Theorem	fldc 38415*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( ( (RingCat ` U ) |`cat J ) |`cat F ) e. Cat )
Theorem	fldhmsubc 38416*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> F e. (Subcat ` ( (RingCat ` U ) |`cat J ) ) )
Theorem	rngcrescrhm 38417	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( C |`cat H ) = ( ( C ↾s R ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rhmsubclem1 38418	Lemma 1 for rhmsubc 38422. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H Fn ( R X. R ) )
Theorem	rhmsubclem2 38419	Lemma 2 for rhmsubc 38422. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )
Theorem	rhmsubclem3 38420*	Lemma 3 for rhmsubc 38422. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ x e. R ) -> ( ( Id ` (RngCat ` U ) ) ` x ) e. ( x H x ) )
Theorem	rhmsubclem4 38421*	Lemma 4 for rhmsubc 38422. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. (comp ` (RngCat ` U ) ) z ) f ) e. ( x H z ) )
Theorem	rhmsubc 38422	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H e. (Subcat ` (RngCat ` U ) ) )
Theorem	rhmsubccat 38423	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( (RngCat ` U ) |`cat H ) e. Cat )
Theorem	srhmsubcALTVlem1 38424*	Lemma 1 for srhmsubcALTV 38427. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( X e. C -> X e. ( U i^i Ring ) )
Theorem	srhmsubcALTVlem2 38425*	Lemma 2 for srhmsubcALTV 38427. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( ( U e. V /\ X e. C ) -> X e. ( Base ` (RingCatALTV ` U ) ) )
Theorem	srhmsubcALTVlem3 38426*	Lemma 3 for srhmsubcALTV 38427. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` (RingCatALTV ` U ) ) Y ) )
Theorem	srhmsubcALTV 38427*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	sringcatALTV 38428*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	crhmsubcALTV 38429*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	cringcatALTV 38430*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	drhmsubcALTV 38431*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	drngcatALTV 38432*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	fldcatALTV 38433*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat F ) e. Cat )
Theorem	fldcALTV 38434*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( ( (RingCatALTV ` U ) |`cat J ) |`cat F ) e. Cat )
Theorem	fldhmsubcALTV 38435*	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> F e. (Subcat ` ( (RingCatALTV ` U ) |`cat J ) ) )
Theorem	rngcrescrhmALTV 38436	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( C |`cat H ) = ( ( C ↾s R ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rhmsubcALTVlem1 38437	Lemma 1 for rhmsubcALTV 38441. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H Fn ( R X. R ) )
Theorem	rhmsubcALTVlem2 38438	Lemma 2 for rhmsubcALTV 38441. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )
Theorem	rhmsubcALTVlem3 38439*	Lemma 3 for rhmsubcALTV 38441. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ x e. R ) -> ( ( Id ` (RngCatALTV ` U ) ) ` x ) e. ( x H x ) )
Theorem	rhmsubcALTVlem4 38440*	Lemma 4 for rhmsubcALTV 38441. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. (comp ` (RngCatALTV ` U ) ) z ) f ) e. ( x H z ) )
Theorem	rhmsubcALTV 38441	According to df-subc 15427, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15455 and subcss2 15458). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H e. (Subcat ` (RngCatALTV ` U ) ) )
Theorem	rhmsubcALTVcat 38442	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( (RngCatALTV ` U ) |`cat H ) e. Cat )
21.33.13  Basic algebraic structures (extension)
21.33.13.1  Auxiliary theorems
Theorem	rabeqsn 38443*	Conditions for a restricted class abstraction to be a singleton. (Contributed by AV, 18-Apr-2019.)
|- ( { x e. V | ph } = { X } <-> A. x ( ( x e. V /\ ph ) <-> x = X ) )
Theorem	rabsssn 38444*	Conditions for a restricted class abstraction to be a subset of a singleton, i.e. to be a singleton or the empty set. (Contributed by AV, 18-Apr-2019.)
|- ( { x e. V | ph } C_ { X } <-> A. x e. V ( ph -> x = X ) )
Theorem	xpprsng 38445	The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.)
|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( { A , B } X. { C } ) = { <. A , C >. , <. B , C >. } )
Theorem	opeliun2xp 38446	Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 4877. (Contributed by AV, 30-Mar-2019.)
|- ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> ( y e. B /\ C e. A ) )
Theorem	eliunxp2 38447*	Membership in a union of Cartesian products over its second component, analogous to eliunxp 4963. (Contributed by AV, 30-Mar-2019.)
|- ( C e. U_ y e. B ( A X. { y } ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
Theorem	mpt2mptx2 38448*	Express a two-argument function as a one-argument function, or vice-versa. In this version A ( y ) is not assumed to be constant w.r.t y, analogous to mpt2mptx 6376. (Contributed by AV, 30-Mar-2019.)
|- ( z = <. x , y >. -> C = D )   =>    |- ( z e. U_ y e. B ( A X. { y } ) |-> C ) = ( x e. A , y e. B |-> D )
Theorem	cbvmpt2x2 38449*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 6359 allows A to be a function of y, analogous to cbvmpt2x 6358. (Contributed by AV, 30-Mar-2019.)
|- F/_ z A   &    |- F/_ y D   &    |- F/_ z C   &    |- F/_ w C   &    |- F/_ x E   &    |- F/_ y E   &    |- ( y = z -> A = D )   &    |- ( ( y = z /\ x = w ) -> C = E )   =>    |- ( x e. A , y e. B |-> C ) = ( w e. D , z e. B |-> E )
Theorem	dmmpt2ssx2 38450*	The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpt2ssx 6851. (Contributed by AV, 30-Mar-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- dom F C_ U_ y e. B ( A X. { y } )
Theorem	mpt2exxg2 38451*	Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpt2exxg 6860. (Contributed by AV, 30-Mar-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( B e. R /\ A. y e. B A e. S ) -> F e. _V )
Theorem	ovmpt2rdxf 38452*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 6411. (Contributed by AV, 30-Mar-2019.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ y = B ) -> C = L )   &    |- ( ph -> A e. L )   &    |- ( ph -> B e. D )   &    |- ( ph -> S e. X )   &    |- F/ x ph   &    |- F/ y ph   &    |- F/_ y A   &    |- F/_ x B   &    |- F/_ x S   &    |- F/_ y S   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2rdx 38453*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 6411. (Contributed by AV, 30-Mar-2019.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ y = B ) -> C = L )   &    |- ( ph -> A e. L )   &    |- ( ph -> B e. D )   &    |- ( ph -> S e. X )   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2x2 38454*	The value of an operation class abstraction. Variant of ovmpt2ga 6415 which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- ( y = B -> C = L )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. L /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	fdmdifeqresdif 38455*	The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019.)
|- F = ( x e. D |-> if ( x = Y , X , ( G ` x ) ) )   =>    |- ( G : ( D \ { Y } ) --> R -> G = ( F |` ( D \ { Y } ) ) )
Theorem	offvalfv 38456*	The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   =>    |- ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )
Theorem	ofaddmndmap 38457	The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019.)
|- R = ( Base ` M )   &    |- .+ = ( +g ` M )   =>    |- ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF .+ B ) e. ( R ^m V ) )
Theorem	mapsnop 38458	A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.)
|- F = { <. X , Y >. }   =>    |- ( ( X e. V /\ Y e. R /\ R e. W ) -> F e. ( R ^m { X } ) )
Theorem	mapprop 38459	An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.)
|- F = { <. X , A >. , <. Y , B >. }   =>    |- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> F e. ( R ^m { X , Y } ) )
Theorem	ztprmneprm 38460	A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.)
|- ( ( Z e. ZZ /\ A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) )
Theorem	2t6m3t4e0 38461	2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.)
|- ( ( 2 x. 6 ) - ( 3 x. 4 ) ) = 0
Theorem	ssnn0ssfz 38462*	For any finite subset of NN0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 28058. (Contributed by AV, 30-Sep-2019.)
|- ( A e. ( ~P NN0 i^i Fin ) -> E. n e. NN0 A C_ ( 0 ... n ) )
Theorem	nn0sumltlt 38463	If the sum of two nonnegative integers is less than a third integer, then one of the summands is already less than this third integer. (Contributed by AV, 19-Oct-2019.)
|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( ( a + b ) < c -> b < c ) )
21.33.13.2  The binomial coefficient operation (extension)
Theorem	bcpascm1 38464	Pascal's rule for the binomial coefficient, generalized to all integers K, shifted down by 1. (Contributed by AV, 8-Sep-2019.)
|- ( ( N e. NN /\ K e. ZZ ) -> ( ( ( N - 1 ) _C K ) + ( ( N - 1 ) _C ( K - 1 ) ) ) = ( N _C K ) )
Theorem	altgsumbc 38465*	The sum of binomial coefficients for a fixed positive N with alternating signs is zero. Notice that this is not valid for N = 0 (since ( ( -u 1 ^ 0 ) x. ( 0 _C 0 ) ) = ( 1 x. 1 ) = 1). For a proof using Pascal's rule (bcpascm1 38464) instead of the binomial theorem (binom 13795) , see altgsumbcALT 38466. (Contributed by AV, 13-Sep-2019.)
|- ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = 0 )
Theorem	altgsumbcALT 38466*	Alternate proof of altgsumbc 38465, using Pascal's rule (bcpascm1 38464) instead of the binomial theorem (binom 13795). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = 0 )
21.33.13.3  The ` ZZ `-module ` ZZ X. ZZ `
Theorem	zlmodzxzlmod 38467	The ZZ-module ZZ X. ZZ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   =>    |- ( Z e. LMod /\ ℤring = (Scalar ` Z ) )
Theorem	zlmodzxzel 38468	An element of the (base set of the) ZZ-module ZZ X. ZZ. (Contributed by AV, 21-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   =>    |- ( ( A e. ZZ /\ B e. ZZ ) -> { <. 0 , A >. , <. 1 , B >. } e. ( Base ` Z ) )
Theorem	zlmodzxz0 38469	The 0 of the ZZ-module ZZ X. ZZ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }   =>    |- .0. = ( 0g ` Z )
Theorem	zlmodzxzscm 38470	The scalar multiplication of the ZZ-module ZZ X. ZZ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .xb = ( .s ` Z )   =>    |- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A .xb { <. 0 , B >. , <. 1 , C >. } ) = { <. 0 , ( A x. B ) >. , <. 1 , ( A x. C ) >. } )
Theorem	zlmodzxzadd 38471	The addition of the ZZ-module ZZ X. ZZ. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .+ = ( +g ` Z )   =>    |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .+ { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A + B ) >. , <. 1 , ( C + D ) >. } )
Theorem	zlmodzxzsubm 38472	The subtraction of the ZZ-module ZZ X. ZZ expressed as addition. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .- = ( -g ` Z )   =>    |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = ( { <. 0 , A >. , <. 1 , C >. } ( +g ` Z ) ( -u 1 ( .s ` Z ) { <. 0 , B >. , <. 1 , D >. } ) ) )
Theorem	zlmodzxzsub 38473	The subtraction of the ZZ-module ZZ X. ZZ. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .- = ( -g ` Z )   =>    |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .- { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A - B ) >. , <. 1 , ( C - D ) >. } )
21.33.13.4  Ordered group sum operation (extension)
Theorem	gsumpr 38474*	Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( k = M -> A = C )   &    |- ( k = N -> A = D )   =>    |- ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsumg ( k e. { M , N } |-> A ) ) = ( C .+ D ) )
Theorem	mgpsumunsn 38475*	Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (Contributed by AV, 29-Dec-2018.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> I e. N )   &    |- ( ( ph /\ k e. N ) -> A e. ( Base ` R ) )   &    |- ( ph -> X e. ( Base ` R ) )   &    |- ( k = I -> A = X )   =>    |- ( ph -> ( M gsumg ( k e. N |-> A ) ) = ( ( M gsumg ( k e. ( N \ { I } ) |-> A ) ) .x. X ) )
Theorem	mgpsumz 38476*	If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> I e. N )   &    |- ( ( ph /\ k e. N ) -> A e. ( Base ` R ) )   &    |- .0. = ( 0g ` R )   &    |- ( k = I -> A = .0. )   =>    |- ( ph -> ( M gsumg ( k e. N |-> A ) ) = .0. )
Theorem	mgpsumn 38477*	If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (Contributed by AV, 29-Dec-2018.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> I e. N )   &    |- ( ( ph /\ k e. N ) -> A e. ( Base ` R ) )   &    |- .1. = ( 1r ` R )   &    |- ( k = I -> A = .1. )   =>    |- ( ph -> ( M gsumg ( k e. N |-> A ) ) = ( M gsumg ( k e. ( N \ { I } ) |-> A ) ) )
Theorem	gsumsplit2f 38478*	Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.)
|- F/ k ph   &    |- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> A = ( C u. D ) )   =>    |- ( ph -> ( G gsumg ( k e. A |-> X ) ) = ( ( G gsumg ( k e. C |-> X ) ) .+ ( G gsumg ( k e. D |-> X ) ) ) )
Theorem	gsumdifsndf 38479*	Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.)
|- F/_ k Y   &    |- F/ k ph   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. W )   &    |- ( ph -> ( k e. A |-> X ) finSupp ( 0g ` G ) )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> M e. A )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k = M ) -> X = Y )   =>    |- ( ph -> ( G gsumg ( k e. A |-> X ) ) = ( ( G gsumg ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )
21.33.13.5  Symmetric groups (extension)
Theorem	nn0le2is012 38480	A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019.)
|- ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
Theorem	exple2lt6 38481	A nonnegative integer to the power of itself is less than 6 if it is less than or equal to 2. (Contributed by AV, 16-Mar-2019.)
|- ( ( N e. NN0 /\ N <_ 2 ) -> ( N ^ N ) < 6 )
Theorem	pgrple2abl 38482	Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.)
|- G = ( SymGrp ` A )   =>    |- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> G e. Abel )
Theorem	pgrpgt2nabl 38483	Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.)
|- G = ( SymGrp ` A )   =>    |- ( ( A e. V /\ 2 < ( # ` A ) ) -> G e/ Abel )
21.33.13.6  Divisibility (extension)
Theorem	invginvrid 38484	Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( N ` Y ) .x. ( ( I ` ( N ` Y ) ) .x. X ) ) = X )
21.33.13.7  The support of functions (extension)
Theorem	rmsupp0 38485*	The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) = (/) )
Theorem	domnmsuppn0 38486*	The support of a mapping of a multiplication of a nonzero constant with a function into a (ring theoretic) domain equals the support of the function. (Contributed by AV, 11-Apr-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) = ( A supp ( 0g ` M ) ) )
Theorem	rmsuppss 38487*	The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) )
Theorem	mndpsuppss 38488	The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) C_ ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) )
Theorem	scmsuppss 38489*	The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.)
|- S = (Scalar ` M )   &    |- R = ( Base ` S )   =>    |- ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` S ) ) )
21.33.13.8  Finitely supported functions (extension)
Theorem	rmsuppfi 38490*	The support of a mapping of a multiplication of a constant with a function into a ring is finite if the support of the function is finite. (Contributed by AV, 11-Apr-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin )
Theorem	rmfsupp 38491*	A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by AV, 9-Jun-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` M ) ) -> ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) finSupp ( 0g ` M ) )
Theorem	mndpsuppfi 38492	The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin )
Theorem	mndpfsupp 38493	A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.)
|- R = ( Base ` M )   =>    |- ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> ( A oF ( +g ` M ) B ) finSupp ( 0g ` M ) )
Theorem	scmsuppfi 38494*	The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.)
|- S = (Scalar ` M )   &    |- R = ( Base ` S )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` S ) ) e. Fin ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) e. Fin )
Theorem	scmfsupp 38495*	A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.)
|- S = (Scalar ` M )   &    |- R = ( Base ` S )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
Theorem	suppmptcfin 38496*	The support of a mapping with value 0 except of one is finite. (Contributed by AV, 27-Apr-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- F = ( x e. V |-> if ( x = X , .1. , .0. ) )   =>    |- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F supp .0. ) e. Fin )
Theorem	mptcfsupp 38497*	A mapping with value 0 except of one is finitely supported. (Contributed by AV, 9-Jun-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- F = ( x e. V |-> if ( x = X , .1. , .0. ) )   =>    |- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> F finSupp .0. )
Theorem	fsuppmptdmf 38498*	A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.)
|- F/ x ph   &    |- F = ( x e. A |-> Y )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> Y e. V )   &    |- ( ph -> Z e. W )   =>    |- ( ph -> F finSupp Z )
21.33.13.9  Left modules (extension)
Theorem	lmodvsmdi 38499	Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .^ = (.g ` W )   &    |- E = (.g ` F )   =>    |- ( ( W e. LMod /\ ( R e. K /\ N e. NN0 /\ X e. V ) ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) )
Theorem	gsumlsscl 38500*	Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- S = ( LSubSp ` M )   &    |- R = (Scalar ` M )   &    |- B = ( Base ` R )   =>    |- ( ( M e. LMod /\ Z e. S /\ V C_ Z ) -> ( ( F e. ( B ^m V ) /\ F finSupp ( 0g ` R ) ) -> ( M gsumg ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. Z ) )