P. 152 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15101-15200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	znidomb 15101	The ℤ/nℤ structure is a domain precisely when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN -> ( Y e. IDomn <-> N e. Prime ) )
Theorem	znunit 15102	The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- U = (Unit ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) e. U <-> ( A gcd N ) = 1 ) )
Theorem	znrrg 15103	The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for N = 0, where all nonzero integers are regular, but only pm 1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- U = (Unit ` Y )   &    |- E = (RLReg ` Y )   =>    |- ( N e. NN -> E = U )
PART 8  BASIC LINEAR ALGEBRA According to Wikipedia ("Linear algebra", 03-Mar-2019, https://en.wikipedia.org/wiki/Linear_algebra) "Linear algebra is the branch of mathematics concerning linear equations [...], linear functions [...] and their representations through matrices and vector spaces." Or according to the Merriam-Webster dictionary ("linear algebra", 12-Mar-2019, https://www.merriam-webster.com/dictionary/linear%20algebra) "Definition of linear algebra: a branch of mathematics that is concerned with mathematical structures closed under the operations of addition and scalar multiplication and that includes the theory of systems of linear equations, matrices, determinants, vector spaces, and linear transformations." Dealing with modules (over rings) instead of vector spaces (over fields) allows for a more unified approach. Therefore, linear equations, matrices, determinants, are usually regarded as "over a ring" in this part. Unless otherwise stated, the rings of scalars need not be commutative (see df-cring 14409), but the existence of a unity element is always assumed (our rings are unital, see df-ring 14408). For readers knowing vector spaces but unfamiliar with modules: the elements of a module are still called "vectors" and they still form a group under addition, with a zero vector as neutral element, like in a vector space. Like in a vector space, vectors can be multiplied by scalars, with the usual rules, the only difference being that the scalars are only required to form a ring, and not necessarily a field or a division ring. Note that any vector space is a (special kind of) module, so any theorem proved below for modules applies to any vector space.
8.1  Associative algebras
8.1.1  Definition and basic properties
Syntax	casa 15104	Associative algebra.
class AssAlg
Syntax	casp 15105	Algebraic span function.
class AlgSpan
Syntax	cascl 15106	Class of algebra scalar lifting function.
class algSc
Definition	df-assa 15107*	Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)
|- AssAlg = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) }
Definition	df-asp 15108*	Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
Definition	df-ascl 15109*	Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unity element. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.)
|- algSc = ( w e. _V |-> ( x e. ( Base ` (Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) )
Theorem	isassa 15110*	The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .X. = ( .r ` W )   =>    |- ( W e. AssAlg <-> ( ( W e. LMod /\ W e. Ring ) /\ A. r e. B A. x e. V A. y e. V ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) ) )
Theorem	assalem 15111	The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .X. = ( .r ` W )   =>    |- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )
Theorem	assaass 15112	Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .X. = ( .r ` W )   =>    |- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )
Theorem	assaassr 15113	Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .X. = ( .r ` W )   =>    |- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) )
Theorem	assalmod 15114	An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. LMod )
Theorem	assaring 15115	An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. Ring )
Theorem	assasca 15116	The scalars of an associative algebra form a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by SN, 2-Mar-2025.)
|- F = (Scalar ` W )   =>    |- ( W e. AssAlg -> F e. Ring )
Theorem	assa2ass 15117	Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) (Proof shortened by Zhi Wang, 11-Sep-2025.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .* = ( .r ` F )   &    |- .x. = ( .s ` W )   &    |- .X. = ( .r ` W )   =>    |- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( C .* A ) .x. ( X .X. Y ) ) )
Theorem	assa2ass2 15118	Left- and right-associative property of an associative algebra. Notice that the scalars are not commuted! (Contributed by Zhi Wang, 11-Sep-2025.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .* = ( .r ` F )   &    |- .x. = ( .s ` W )   &    |- .X. = ( .r ` W )   =>    |- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( A .* C ) .x. ( X .X. Y ) ) )
Theorem	isassad 15119*	Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by SN, 2-Mar-2025.)
|- ( ph -> V = ( Base ` W ) )   &    |- ( ph -> F = (Scalar ` W ) )   &    |- ( ph -> B = ( Base ` F ) )   &    |- ( ph -> .x. = ( .s ` W ) )   &    |- ( ph -> .X. = ( .r ` W ) )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> W e. Ring )   &    |- ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) )   &    |- ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) )   =>    |- ( ph -> W e. AssAlg )
Theorem	issubassa3 15120	A subring that is also a subspace is a subalgebra. The key theorem is islss3 14824. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- S = ( W ↾s A )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. AssAlg /\ ( A e. (SubRing ` W ) /\ A e. L ) ) -> S e. AssAlg )
Theorem	issubassa 15121	The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015.)
|- S = ( W ↾s A )   &    |- L = ( LSubSp ` W )   &    |- V = ( Base ` W )   &    |- .1. = ( 1r ` W )   =>    |- ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) -> ( S e. AssAlg <-> ( A e. (SubRing ` W ) /\ A e. L ) ) )
Theorem	assapropd 15122*	If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-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 -> F = (Scalar ` K ) )   &    |- ( ph -> F = (Scalar ` L ) )   &    |- P = ( Base ` F )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   =>    |- ( ph -> ( K e. AssAlg <-> L e. AssAlg ) )
Theorem	aspval 15123*	Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- A = (AlgSpan ` W )   &    |- V = ( Base ` W )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( (SubRing ` W ) i^i L ) | S C_ t } )
Theorem	asplss 15124	The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- A = (AlgSpan ` W )   &    |- V = ( Base ` W )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) e. L )
Theorem	aspid 15125	The algebraic span of a subalgebra is itself. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- A = (AlgSpan ` W )   &    |- V = ( Base ` W )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. AssAlg /\ S e. (SubRing ` W ) /\ S e. L ) -> ( A ` S ) = S )
Theorem	aspsubrg 15126	The algebraic span of a set of vectors is a subring of the algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- A = (AlgSpan ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) e. (SubRing ` W ) )
Theorem	aspss 15127	Span preserves subset ordering. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- A = (AlgSpan ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. AssAlg /\ S C_ V /\ T C_ S ) -> ( A ` T ) C_ ( A ` S ) )
Theorem	aspssid 15128	A set of vectors is a subset of its span. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- A = (AlgSpan ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. AssAlg /\ S C_ V ) -> S C_ ( A ` S ) )
Theorem	asclfval 15129*	Function value of the algebra scalar lifting function. (Contributed by Mario Carneiro, 8-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .1. = ( 1r ` W )   =>    |- A = ( x e. K |-> ( x .x. .1. ) )
Theorem	asclvald 15130	Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- .1. = ( 1r ` W )   &    |- ( ph -> X e. K )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> W e. Ring )   =>    |- ( ph -> ( A ` X ) = ( X .x. .1. ) )
Theorem	asclfnd 15131	Functionality of the algebra scalar lifting function. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> W e. Ring )   =>    |- ( ph -> A Fn K )
Theorem	asclf 15132	The algebra scalar lifting function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. Ring )   &    |- ( ph -> W e. LMod )   &    |- K = ( Base ` F )   &    |- B = ( Base ` W )   =>    |- ( ph -> A : K --> B )
Theorem	asclghm 15133	The algebra scalar lifting function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. Ring )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> A e. ( F GrpHom W ) )
Theorem	asclelbas 15134	Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, 22-Sep-2025.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- ( ph -> W e. AssAlg )   &    |- ( ph -> C e. B )   =>    |- ( ph -> ( A ` C ) e. ( Base ` W ) )
Theorem	ascl0 15135	The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> W e. Ring )   =>    |- ( ph -> ( A ` ( 0g ` F ) ) = ( 0g ` W ) )
Theorem	ascl1 15136	The scalar 1 embedded into a left module corresponds to the 1 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> W e. Ring )   =>    |- ( ph -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )
Theorem	asclmul1 15137	Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .X. = ( .r ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. AssAlg /\ R e. K /\ X e. V ) -> ( ( A ` R ) .X. X ) = ( R .x. X ) )
Theorem	asclmul2 15138	Right multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .X. = ( .r ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. AssAlg /\ R e. K /\ X e. V ) -> ( X .X. ( A ` R ) ) = ( R .x. X ) )
Theorem	ascldimul 15139	The algebra scalar lifting function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015.) (Proof shortened by SN, 5-Nov-2023.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .X. = ( .r ` W )   &    |- .x. = ( .r ` F )   =>    |- ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( A ` R ) .X. ( A ` S ) ) )
Theorem	asclinvg 15140	The group inverse (negation) of a lifted scalar is the lifted negation of the scalar. (Contributed by AV, 2-Sep-2019.)
|- A = (algSc ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- I = ( invg ` R )   &    |- J = ( invg ` W )   =>    |- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> ( J ` ( A ` C ) ) = ( A ` ( I ` C ) ) )
Theorem	asclrhm 15141	The algebra scalar lifting function is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   =>    |- ( W e. AssAlg -> A e. ( F RingHom W ) )
Theorem	rnascl 15142	The set of lifted scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- .1. = ( 1r ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. AssAlg -> ran A = ( N ` { .1. } ) )
Theorem	issubassa2 15143	A subring of a unital algebra is a subspace and thus a subalgebra iff it contains all scalar multiples of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. AssAlg /\ S e. (SubRing ` W ) ) -> ( S e. L <-> ran A C_ S ) )
Theorem	rnasclsubrg 15144	The scalar multiples of the unit vector form a subring of the vectors. (Contributed by SN, 5-Nov-2023.)
|- C = (algSc ` W )   &    |- ( ph -> W e. AssAlg )   =>    |- ( ph -> ran C e. (SubRing ` W ) )
Theorem	rnasclmulcl 15145	(Vector) multiplication is closed for scalar multiples of the unit vector. (Contributed by SN, 5-Nov-2023.)
|- C = (algSc ` W )   &    |- .X. = ( .r ` W )   &    |- ( ph -> W e. AssAlg )   =>    |- ( ( ph /\ ( X e. ran C /\ Y e. ran C ) ) -> ( X .X. Y ) e. ran C )
Theorem	rnasclassa 15146	The scalar multiples of the unit vector form a subalgebra of the vectors. (Contributed by SN, 16-Nov-2023.)
|- A = (algSc ` W )   &    |- U = ( W ↾s ran A )   &    |- ( ph -> W e. AssAlg )   =>    |- ( ph -> U e. AssAlg )
Theorem	ressascl 15147	The lifting of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- X = ( W ↾s S )   =>    |- ( S e. (SubRing ` W ) -> A = (algSc ` X ) )
Theorem	asclpropd 15148*	If two structures have the same components (properties), one is an associative algebra iff the other one is. The last hypotheses on 1r can be discharged either by letting W = _V (if strong equality is known on .s) or assuming K is a ring. (Contributed by Mario Carneiro, 5-Jul-2015.)
|- F = (Scalar ` K )   &    |- G = (Scalar ` L )   &    |- ( ph -> P = ( Base ` F ) )   &    |- ( ph -> P = ( Base ` G ) )   &    |- ( ( ph /\ ( x e. P /\ y e. W ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   &    |- ( ph -> ( 1r ` K ) = ( 1r ` L ) )   &    |- ( ph -> ( 1r ` K ) e. W )   =>    |- ( ph -> (algSc ` K ) = (algSc ` L ) )
Theorem	assamulgscmlem1 15149	Lemma 1 for assamulgscm 15151 (induction base). (Contributed by AV, 26-Aug-2019.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- G = (mulGrp ` F )   &    |- .^ = (.g ` G )   &    |- H = (mulGrp ` W )   &    |- E = (.g ` H )   =>    |- ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E ( A .x. X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) )
Theorem	assamulgscmlem2 15150	Lemma for assamulgscm 15151 (induction step). (Contributed by AV, 26-Aug-2019.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- G = (mulGrp ` F )   &    |- .^ = (.g ` G )   &    |- H = (mulGrp ` W )   &    |- E = (.g ` H )   =>    |- ( y e. NN0 -> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) ) ) )
Theorem	assamulgscm 15151	Exponentiation of a scalar multiplication in an associative algebra: ( a .x. X ) ^ N = ( a ^ N ) .X. ( X ^ N ). (Contributed by AV, 26-Aug-2019.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- G = (mulGrp ` F )   &    |- .^ = (.g ` G )   &    |- H = (mulGrp ` W )   &    |- E = (.g ` H )   =>    |- ( ( W e. AssAlg /\ ( N e. NN0 /\ A e. B /\ X e. V ) ) -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) )
Theorem	asclmulg 15152	Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .^ = (.g ` W )   &    |- .* = (.g ` F )   =>    |- ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( A ` ( N .* X ) ) = ( N .^ ( A ` X ) ) )
8.2  Abstract multivariate polynomials
8.2.1  Definition and basic properties
Syntax	cmps 15153	Multivariate power series.
class mPwSer
Syntax	cmvr 15154	Multivariate power series variables.
class mVar
Syntax	cmpl 15155	Multivariate polynomials.
class mPoly
Definition	df-psr 15156*	Define the algebra of power series over the index set i and with coefficients from the ring r. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
Definition	df-mvr 15157*	Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- mVar = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) )
Definition	df-mpl 15158*	Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). The index set (which has an element for each variable) is i, the coefficients are in ring r, and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for r). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.)
|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) )
Theorem	reldmpsr 15159	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPwSer
Theorem	psrval 15160*	Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- O = ( TopOpen ` R )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   &    |- ( ph -> B = ( K ^m D ) )   &    |- .+b = ( oF .+ |` ( B X. B ) )   &    |- .X. = ( f e. B , g e. B |-> ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )   &    |- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )   &    |- ( ph -> J = ( Xt_ ` ( D X. { O } ) ) )   &    |- ( ph -> I e. W )   &    |- ( ph -> R e. X )   =>    |- ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
Theorem	fnpsr 15161	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
|- mPwSer Fn ( _V X. _V )
Theorem	psrvalstrd 15162	The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( ph -> B e. X )   &    |- ( ph -> .+ e. Y )   &    |- ( ph -> .X. e. Z )   &    |- ( ph -> R e. W )   &    |- ( ph -> .x. e. P )   &    |- ( ph -> J e. Q )   =>    |- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .x. >. , <. (TopSet ` ndx ) , J >. } ) Struct <. 1 , 9 >. )
Theorem	psrbag 15163*	Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
Theorem	psrbagf 15164*	A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( F e. D -> F : I --> NN0 )
Theorem	psrbagfsuppfi 15165*	Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by Jim Kingdon, 22-Oct-2026.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ I e. Fin ) -> F finSupp 0 )
Theorem	psrbagfi 15166*	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. Fin -> D = ( NN0 ^m I ) )
Theorem	psrbagdceq 15167*	Finite bags have decidable equality. (Contributed by Jim Kingdon, 11-Oct-2026.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. Fin /\ A e. D /\ B e. D ) -> DECID A = B )
Theorem	snifpsrbagfi 15168*	A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 8-Jul-2019.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. Fin /\ N e. NN0 /\ X e. I ) -> ( y e. I |-> if ( y = X , N , 0 ) ) e. D )
Theorem	fczpsrbag 15169*	The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. V -> ( x e. I |-> 0 ) e. D )
Theorem	psrbaglesuppg 15170*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' G " NN ) C_ ( `' F " NN ) )
Theorem	psrbaglesupp 15171*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' G " NN ) C_ ( `' F " NN ) )
Theorem	psrbaglecl 15172*	The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G e. D )
Theorem	psrbagaddclfi 15173*	The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) Shorten proof and remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G e. D /\ I e. Fin ) -> ( F oF + G ) e. D )
Theorem	psrbagcon 15174*	The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )
Theorem	psrbaglefifi 15175*	There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) (Revised by Jim Kingdon, 28-Jul-2026.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ I e. Fin ) -> { y e. D | y oR <_ F } e. Fin )
Theorem	psrbagconcl 15176*	The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   =>    |- ( ( F e. D /\ X e. S ) -> ( F oF - X ) e. S )
Theorem	psrbagconf1o 15177*	Bag complementation is a bijection on the set of bags dominated by a given bag F. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   =>    |- ( F e. D -> ( x e. S |-> ( F oF - x ) ) : S -1-1-onto-> S )
Theorem	psrbagmaxlem1 15178*	Lemma for psrbagmax 15183. Existence of a bag which is greater than any element of a finite set of bags. (Contributed by Jim Kingdon, 27-Oct-2026.)
|- ( ph -> X C_ ( NN0 ^m I ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I e. Fin )   =>    |- ( ph -> E. p ( p : I --> NN0 /\ A. j e. I A. x e. X ( x ` j ) <_ ( p ` j ) ) )
Theorem	psrbagmaxlem1a 15179*	Lemma for psrbagmax 15183. A new bag which is the pointwise maximum of two bags. (Contributed by Jim Kingdon, 27-Oct-2026.)
|- ( ph -> X C_ ( NN0 ^m I ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> P : I --> NN0 )   &    |- ( ph -> R : I --> NN0 )   &    |- S = ( i e. I |-> sup ( { ( P ` i ) , ( R ` i ) } , RR , < ) )   =>    |- ( ph -> S : I --> NN0 )
Theorem	psrbagmaxlemfi 15180*	Lemma for psrbagmax 15183. Applying psrbaglefifi 15175 to the sets in this theorem. (Contributed by Jim Kingdon, 27-Oct-2026.)
|- ( ph -> X C_ ( NN0 ^m I ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> P : I --> NN0 )   &    |- ( ph -> R : I --> NN0 )   &    |- S = ( i e. I |-> sup ( { ( P ` i ) , ( R ` i ) } , RR , < ) )   &    |- Z = { q e. ( NN0 ^m I ) | q oR <_ S }   =>    |- ( ph -> Z e. Fin )
Theorem	psrbagmaxlem1x 15181*	Lemma for psrbagmax 15183. All the bags in X are (pointwise) less than S, and thus elements of Z. (Contributed by Jim Kingdon, 27-Oct-2026.)
|- ( ph -> X C_ ( NN0 ^m I ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> P : I --> NN0 )   &    |- ( ph -> R : I --> NN0 )   &    |- S = ( i e. I |-> sup ( { ( P ` i ) , ( R ` i ) } , RR , < ) )   &    |- Z = { q e. ( NN0 ^m I ) | q oR <_ S }   &    |- ( ph -> A. j e. I A. x e. X ( x ` j ) <_ ( P ` j ) )   &    |- ( ph -> A. j e. I A. y e. Y ( y ` j ) <_ ( R ` j ) )   &    |- ( ph -> Y C_ ( NN0 ^m I ) )   &    |- ( ph -> Y e. Fin )   =>    |- ( ph -> X C_ Z )
Theorem	psrbagmaxlem1y 15182*	Lemma for psrbagmax 15183. All the bags in Y are (pointwise) less than S, and thus elements of Z. (Contributed by Jim Kingdon, 27-Oct-2026.)
|- ( ph -> X C_ ( NN0 ^m I ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> P : I --> NN0 )   &    |- ( ph -> R : I --> NN0 )   &    |- S = ( i e. I |-> sup ( { ( P ` i ) , ( R ` i ) } , RR , < ) )   &    |- Z = { q e. ( NN0 ^m I ) | q oR <_ S }   &    |- ( ph -> A. j e. I A. x e. X ( x ` j ) <_ ( P ` j ) )   &    |- ( ph -> A. j e. I A. y e. Y ( y ` j ) <_ ( R ` j ) )   &    |- ( ph -> Y C_ ( NN0 ^m I ) )   &    |- ( ph -> Y e. Fin )   =>    |- ( ph -> Y C_ Z )
Theorem	psrbagmax 15183*	Given two finite sets of bags, provide a finite set which contains all of their elements. The proof constructs the result ( Z in the lemmas), proves its properties (via psrbagmaxlemfi 15180, psrbagmaxlem1x 15181, and psrbagmaxlem1y 15182), and then this proof combines those lemmas and assigns the result to the variable z. (Contributed by Jim Kingdon, 24-Oct-2026.)
|- ( ph -> X C_ ( NN0 ^m I ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ ( NN0 ^m I ) )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> I e. Fin )   =>    |- ( ph -> E. z ( ( z C_ ( NN0 ^m I ) /\ z e. Fin ) /\ ( X C_ z /\ Y C_ z ) ) )
Theorem	gsumbagdiaglem 15184*	Lemma for gsumbagdiagfi 15185. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   &    |- ( ph -> F e. D )   =>    |- ( ( ph /\ ( X e. S /\ Y e. { x e. D | x oR <_ ( F oF - X ) } ) ) -> ( Y e. S /\ X e. { x e. D | x oR <_ ( F oF - Y ) } ) )
Theorem	gsumbagdiagfi 15185*	Two-dimensional commutation of a group sum over a "triangular" region. fisum0diag 12232 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   &    |- ( ph -> F e. D )   &    |- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> I e. Fin )   &    |- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )   =>    |- ( ph -> ( G gsumg ( j e. S , k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) = ( G gsumg ( k e. S , j e. { x e. D | x oR <_ ( F oF - k ) } |-> X ) ) )
Theorem	psrass1filem 15186*	A group sum commutation used by psrass1fi 15210. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   &    |- ( ph -> F e. D )   &    |- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> I e. Fin )   &    |- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )   &    |- ( k = ( n oF - j ) -> X = Y )   =>    |- ( ph -> ( G gsumg ( n e. S |-> ( G gsumg ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) = ( G gsumg ( j e. S |-> ( G gsumg ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) ) ) )
Theorem	psrbasg 15187*	The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 8-Jul-2019.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- B = ( Base ` S )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> B = ( K ^m D ) )
Theorem	psrelbas 15188*	An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : D --> K )
Theorem	psrelbasfi 15189	Simpler form of psrelbas 15188 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- ( ph -> I e. Fin )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : ( NN0 ^m I ) --> K )
Theorem	psrelbasfun 15190	An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   =>    |- ( X e. B -> Fun X )
Theorem	psrplusgg 15191	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   =>    |- ( ( I e. V /\ R e. W ) -> .+b = ( oF .+ |` ( B X. B ) ) )
Theorem	psradd 15192	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	psraddcl 15193	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- ( ph -> R e. Mgm )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+ Y ) e. B )
Theorem	rhmpsrfilem2 15194*	Lemma for rhmpsr et al. (Contributed by SN, 8-Feb-2025.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> X : D --> ( Base ` R ) )   &    |- ( ph -> Y : D --> ( Base ` R ) )   =>    |- ( ( ph /\ k e. D ) -> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. ( Base ` R ) )
Theorem	psrmulrg 15195*	The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` S )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   =>    |- ( ( I e. V /\ R e. W ) -> .xb = ( f e. B , g e. B |-> ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) )
Theorem	psrmulfval 15196*	The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` S )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .xb G ) = ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( F ` x ) .x. ( G ` ( k oF - x ) ) ) ) ) ) )
Theorem	psrmulvalfi 15197*	The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` S )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- ( ph -> X e. D )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> ( ( F .xb G ) ` X ) = ( R gsumg ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )
Theorem	psrmulclfilem 15198*	Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ph -> ( X .x. Y ) e. B )
Theorem	psrmulclfi 15199	Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .x. Y ) e. B )
Theorem	psr0cl 15200*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- B = ( Base ` S )   =>    |- ( ph -> ( D X. { .0. } ) e. B )