P. 151 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ascl 15001*	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 15002*	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 15003	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 15004	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 15005	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 15006	An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. LMod )
Theorem	assaring 15007	An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. Ring )
Theorem	assasca 15008	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 15009	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 15010	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 15011*	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 15012	A subring that is also a subspace is a subalgebra. The key theorem is islss3 14716. (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 15013	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 15014*	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 15015*	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 15016	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 15017	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 15018	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 15019	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 15020	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 15021*	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 15022	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 15023	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 15024	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 15025	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 15026	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 15027	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 15028	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 15029	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 15030	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 15031	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 15032	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 15033	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 15034	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 15035	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 15036	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 15037	(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 15038	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 15039	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 15040*	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 15041	Lemma 1 for assamulgscm 15043 (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 15042	Lemma for assamulgscm 15043 (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 15043	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 15044	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 15045	Multivariate power series.
class mPwSer
Syntax	cmpl 15046	Multivariate polynomials.
class mPoly
Definition	df-psr 15047*	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 15048*	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 15049	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPwSer
Theorem	psrval 15050*	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 15051	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
|- mPwSer Fn ( _V X. _V )
Theorem	psrvalstrd 15052	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 15053*	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 15054*	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 15055*	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 15056*	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 15057*	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 15058*	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 15059*	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 15060*	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 15061*	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 15062*	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	psrbagconcl 15063*	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 15064*	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	psrbasg 15065*	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 15066*	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 15067	Simpler form of psrelbas 15066 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 15068	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 15069	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 15070	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 15071	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	psr0cl 15072*	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 15073*	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 15074*	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 15075*	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 15076	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 15077*	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 15078*	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 15079*	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	reldmmpl 15080	The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPoly
Theorem	mplvalcoe 15081*	Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) }   =>    |- ( ( I e. V /\ R e. W ) -> P = ( S ↾s U ) )
Theorem	mplbascoe 15082*	Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) } )
Theorem	mplelbascoe 15083*	Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> ( X e. U <-> ( X e. B /\ E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( X ` b ) = .0. ) ) ) )
Theorem	fnmpl 15084	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
|- mPoly Fn ( _V X. _V )
Theorem	mplrcl 15085	Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- P = ( I mPoly R )   &    |- B = ( Base ` P )   =>    |- ( X e. B -> I e. _V )
Theorem	mplval2g 15086	Self-referential expression for the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> P = ( S ↾s U ) )
Theorem	mplbasss 15087	The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- U = ( Base ` P )   &    |- B = ( Base ` S )   =>    |- U C_ B
Theorem	mplelf 15088*	A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : D --> K )
Theorem	mplsubgfilemm 15089*	Lemma for mplsubgfi 15092. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> E. j j e. U )
Theorem	mplsubgfilemcl 15090	Lemma for mplsubgfi 15092. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( X .+ Y ) e. U )
Theorem	mplsubgfileminv 15091	Lemma for mplsubgfi 15092. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- N = ( invg ` S )   =>    |- ( ph -> ( N ` X ) e. U )
Theorem	mplsubgfi 15092	The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> U e. (SubGrp ` S ) )
Theorem	mpl0fi 15093*	The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.)
|- P = ( I mPoly R )   &    |- O = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> .0. = ( x e. ( NN0 ^m I ) |-> O ) )
Theorem	mplplusgg 15094	Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- Y = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- .+ = ( +g ` Y )   =>    |- ( ( I e. V /\ R e. W ) -> .+ = ( +g ` S ) )
Theorem	mpladd 15095	The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- B = ( Base ` P )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` P )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	mplnegfi 15096	The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.)
|- P = ( I mPoly R )   &    |- B = ( Base ` P )   &    |- N = ( invg ` R )   &    |- M = ( invg ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( M ` X ) = ( N o. X ) )
Theorem	mplgrpfi 15097	The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.)
|- P = ( I mPoly R )   =>    |- ( ( I e. Fin /\ R e. Grp ) -> P e. Grp )
PART 9  BASIC TOPOLOGY
9.1  Topology
9.1.1  Topological spaces A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union), and it may sometimes be more convenient to consider topologies without reference to the underlying set.
9.1.1.1  Topologies
Syntax	ctop 15098	Syntax for the class of topologies.
class Top
Definition	df-top 15099*	Define the class of topologies. It is a proper class. See istopg 15100 and istopfin 15101 for the corresponding characterizations, using respectively binary intersections like in this definition and nonempty finite intersections. The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.)
|- Top = { x | ( A. y e. ~P x U. y e. x /\ A. y e. x A. z e. x ( y i^i z ) e. x ) }
Theorem	istopg 15100*	Express the predicate " J is a topology". See istopfin 15101 for another characterization using nonempty finite intersections instead of binary intersections. Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )