P. 194 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19301-19400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opprdomn 19301	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	abvn0b 19302	Another characterization of domains, hinted at in abvtriv 18841: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.)
|- A = (AbsVal ` R )   =>    |- ( R e. Domn <-> ( R e. NzRing /\ A =/= (/) ) )
Theorem	drngdomn 19303	A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.)
|- ( R e. DivRing -> R e. Domn )
Theorem	isidom 19304	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
Theorem	fldidom 19305	A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.)
|- ( R e. Field -> R e. IDomn )
Theorem	fidomndrnglem 19306*	Lemma for fidomndrng 19307. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Domn )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> A e. ( B \ { .0. } ) )   &    |- F = ( x e. B |-> ( x .x. A ) )   =>    |- ( ph -> A .|| .1. )
Theorem	fidomndrng 19307	A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- B = ( Base ` R )   =>    |- ( B e. Fin -> ( R e. Domn <-> R e. DivRing ) )
Theorem	fiidomfld 19308	A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- B = ( Base ` R )   =>    |- ( B e. Fin -> ( R e. IDomn <-> R e. Field ) )
10.9  Associative algebras
10.9.1  Definition and basic properties
Syntax	casa 19309	Associative algebra.
class AssAlg
Syntax	casp 19310	Algebraic span function.
class AlgSpan
Syntax	cascl 19311	Class of algebra scalar injection function.
class algSc
Definition	df-assa 19312*	Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) 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.)
|- AssAlg = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. ( f e. CRing /\ 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 19313*	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 19314*	Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unit. 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 19315*	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 <-> ( ( W e. LMod /\ W e. Ring /\ F e. CRing ) /\ 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 19316	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 19317	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 19318	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 19319	An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. LMod )
Theorem	assaring 19320	An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. Ring )
Theorem	assasca 19321	An associative algebra's scalar field is a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. AssAlg -> F e. CRing )
Theorem	assa2ass 19322	Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.)
|- 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	isassad 19323*	Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( 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 -> F e. CRing )   &    |- ( ( 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	issubassa 19324	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	sraassa 19325	The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- A = ( (subringAlg ` W ) ` S )   =>    |- ( ( W e. CRing /\ S e. (SubRing ` W ) ) -> A e. AssAlg )
Theorem	rlmassa 19326	The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. CRing -> (ringLMod ` R ) e. AssAlg )
Theorem	assapropd 19327*	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 19328*	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 19329	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 19330	The algebraic span of a subalgebra is itself. (spanid 28206 analog.) (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 19331	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 19332	Span preserves subset ordering. (spanss 28207 analog.) (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 19333	A set of vectors is a subset of its span. (spanss2 28204 analog.) (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 19334*	Function value of the algebraic scalars 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	asclval 19335	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 )   =>    |- ( X e. K -> ( A ` X ) = ( X .x. .1. ) )
Theorem	asclfn 19336	Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- A = (algSc ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- A Fn K
Theorem	asclf 19337	The algebra scalars 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 19338	The algebra scalars 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	asclmul1 19339	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 19340	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	asclinvg 19341	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 19342	The scalar injection 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 19343	The set of injected 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	ressascl 19344	The injection 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	issubassa2 19345	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	asclpropd 19346*	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	aspval2 19347	The algebraic closure is the ring closure when the generating set is expanded to include all scalars. EDITORIAL : In light of this, is AlgSpan independently needed? (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- A = (AlgSpan ` W )   &    |- C = (algSc ` W )   &    |- R = (mrCls ` (SubRing ` W ) )   &    |- V = ( Base ` W )   =>    |- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = ( R ` ( ran C u. S ) ) )
Theorem	assamulgscmlem1 19348	Lemma 1 for assamulgscm 19350 (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 19349	Lemma for assamulgscm 19350 (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 19350	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 ) ) )
10.10  Abstract multivariate polynomials
10.10.1  Definition and basic properties
Syntax	cmps 19351	Multivariate power series.
class mPwSer
Syntax	cmvr 19352	Multivariate power series variables.
class mVar
Syntax	cmpl 19353	Multivariate polynomials.
class mPoly
Syntax	cltb 19354	Ordering on terms of a multivariate polynomial.
class <bag
Syntax	copws 19355	Ordered set of power series.
class ordPwSer
Definition	df-psr 19356*	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 19357*	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 19358*	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). (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 ) } ) )
Definition	df-ltbag 19359*	Define a well-order on the set of all finite bags from the index set i given a wellordering r of i. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- <bag = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } /\ E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) ) ) } )
Definition	df-opsr 19360*	Define a total order on the set of all power series in s from the index set i given a wellordering r of i and a totally ordered base ring s. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ordPwSer = ( i e. _V , s e. _V |-> ( r e. ~P ( i X. i ) |-> [_ ( i mPwSer s ) / p ]_ ( p sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` p ) /\ ( [. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]. E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r <bag i ) z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
Theorem	reldmpsr 19361	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPwSer
Theorem	psrval 19362*	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	psrvalstr 19363	The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .x. >. , <. (TopSet ` ndx ) , J >. } ) Struct <. 1 , 9 >.
Theorem	psrbag 19364*	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 19365*	A finite bag is a function. (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 )
Theorem	snifpsrbag 19366*	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. V /\ N e. NN0 ) -> ( y e. I |-> if ( y = X , N , 0 ) ) e. D )
Theorem	fczpsrbag 19367*	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	psrbaglesupp 19368*	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	psrbaglecl 19369*	The set of finite bags is downward-closed. (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 e. D )
Theorem	psrbagaddcl 19370*	The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. V /\ F e. D /\ G e. D ) -> ( F oF + G ) e. D )
Theorem	psrbagcon 19371*	The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for 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 /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )
Theorem	psrbaglefi 19372*	There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. V /\ F e. D ) -> { y e. D | y oR <_ F } e. Fin )
Theorem	psrbagconcl 19373*	The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   =>    |- ( ( I e. V /\ F e. D /\ X e. S ) -> ( F oF - X ) e. S )
Theorem	psrbagconf1o 19374*	Bag complementation is a bijection on the set of bags dominated by a given bag F. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   =>    |- ( ( I e. V /\ F e. D ) -> ( x e. S |-> ( F oF - x ) ) : S -1-1-onto-> S )
Theorem	gsumbagdiaglem 19375*	Lemma for gsumbagdiag 19376. (Contributed by Mario Carneiro, 5-Jan-2015.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   &    |- ( ph -> I e. V )   &    |- ( 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	gsumbagdiag 19376*	Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 14509 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   &    |- ( ph -> I e. V )   &    |- ( ph -> F e. D )   &    |- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ( 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	psrass1lem 19377*	A group sum commutation used by psrass1 19405. (Contributed by Mario Carneiro, 5-Jan-2015.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   &    |- ( ph -> I e. V )   &    |- ( ph -> F e. D )   &    |- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ( 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	psrbas 19378*	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 -> B = ( K ^m D ) )
Theorem	psrelbas 19379*	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	psrelbasfun 19380	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	psrplusg 19381	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 )   =>    |- .+b = ( oF .+ |` ( B X. B ) )
Theorem	psradd 19382	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 19383	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+ Y ) e. B )
Theorem	psrmulr 19384*	The multiplication 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 )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` S )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   =>    |- .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 19385*	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	psrmulval 19386*	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 -> ( ( F .xb G ) ` X ) = ( R gsumg ( k e. { y e. D | y oR <_ X } |-> ( ( F ` k ) .x. ( G ` ( X oF - k ) ) ) ) ) )
Theorem	psrmulcllem 19387*	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 -> X e. B )   &    |- ( ph -> Y e. B )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ph -> ( X .x. Y ) e. B )
Theorem	psrmulcl 19388	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 -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .x. Y ) e. B )
Theorem	psrsca 19389	The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> R = (Scalar ` S ) )
Theorem	psrvscafval 19390*	The scalar multiplication 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 )   &    |- .xb = ( .s ` S )   &    |- K = ( Base ` R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` R )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   =>    |- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
Theorem	psrvsca 19391*	The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- .xb = ( .s ` S )   &    |- K = ( Base ` R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` R )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   &    |- ( ph -> X e. K )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )
Theorem	psrvscaval 19392*	The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- .xb = ( .s ` S )   &    |- K = ( Base ` R )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` R )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   &    |- ( ph -> X e. K )   &    |- ( ph -> F e. B )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )
Theorem	psrvscacl 19393	Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- .x. = ( .s ` S )   &    |- K = ( Base ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. K )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( X .x. F ) e. B )
Theorem	psr0cl 19394*	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 )
Theorem	psr0lid 19395*	The zero element of the ring of power series is a left identity. (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 )   &    |- .+ = ( +g ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( D X. { .0. } ) .+ X ) = X )
Theorem	psrnegcl 19396*	The negative function in 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 }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N o. X ) e. B )
Theorem	psrlinv 19397*	The negative function in 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 }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( ( N o. X ) .+ X ) = ( D X. { .0. } ) )
Theorem	psrgrp 19398	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> S e. Grp )
Theorem	psr0 19399*	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 }   &    |- O = ( 0g ` R )   &    |- .0. = ( 0g ` S )   =>    |- ( ph -> .0. = ( D X. { O } ) )
Theorem	psrneg 19400*	The negative function 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 }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- M = ( invg ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( M ` X ) = ( N o. X ) )