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	znidom 15101	The ℤ/nℤ structure is an integral domain when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. Prime -> Y e. IDomn )
Theorem	znidomb 15102	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 15103	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 15104	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 14410), but the existence of a unity element is always assumed (our rings are unital, see df-ring 14409). 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 15105	Associative algebra.
class AssAlg
Syntax	casp 15106	Algebraic span function.
class AlgSpan
Syntax	cascl 15107	Class of algebra scalar lifting function.
class algSc
Definition	df-assa 15108*	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 15109*	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 15110*	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 15111*	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 15112	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 15113	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 15114	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 15115	An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. LMod )
Theorem	assaring 15116	An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. Ring )
Theorem	assasca 15117	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 15118	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 15119	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 15120*	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 15121	A subring that is also a subspace is a subalgebra. The key theorem is islss3 14825. (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 15122	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 15123*	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 15124*	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 15125	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 15126	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 15127	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 15128	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 15129	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 15130*	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 15131	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 15132	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 15133	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 15134	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 15135	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 15136	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 15137	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 15138	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 15139	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 15140	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 15141	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 15142	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 15143	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 15144	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 15145	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 15146	(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 15147	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 15148	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 15149*	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 15150	Lemma 1 for assamulgscm 15152 (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 15151	Lemma for assamulgscm 15152 (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 15152	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 15153	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 15154	Multivariate power series.
class mPwSer
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-mplcoe 15157*	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.) (Revised by Jim Kingdon, 7-Oct-2025.)
|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
Theorem	reldmpsr 15158	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPwSer
Theorem	psrval 15159*	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 15160	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
|- mPwSer Fn ( _V X. _V )
Theorem	psrvalstrd 15161	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 15162*	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 15163*	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	psrbagfsupp 15164*	Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( F e. D -> F finSupp 0 )
Theorem	fczpsrbag 15165*	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 15166*	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 15167*	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	psrbagfi 15168*	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	psrbaglecl 15169*	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 15170*	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 15171*	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 15172*	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 15173*	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 15174*	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	gsumbagdiaglem 15175*	Lemma for gsumbagdiagfi 15176. (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 15176*	Two-dimensional commutation of a group sum over a "triangular" region. fisum0diag 12233 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 15177*	A group sum commutation used by psrass1fi 15201. (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 15178*	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 15179*	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 15180	Simpler form of psrelbas 15179 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 15181	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 15182	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 15183	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 15184	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 15185*	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 15186*	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 15187*	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 15188*	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 15189*	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 15190	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 15191*	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 15192*	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 15193*	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 15194*	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 15195	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> S e. Grp )
Theorem	psr0 15196*	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 15197*	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 ) )
Theorem	psr1clfi 15198*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Ring )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )   &    |- B = ( Base ` S )   =>    |- ( ph -> U e. B )
Theorem	psrlidmfi 15199*	The identity element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Ring )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( U .x. X ) = X )
Theorem	psrridmfi 15200*	The identity element of the ring of power series is a right identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Ring )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )   &    |- B = ( Base ` S )   &    |- .x. = ( .r ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .x. U ) = X )