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
Theorem	zrhval 15001	Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- L = U. (ℤring RingHom R )
Theorem	zrhvalg 15002	Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. V -> L = U. (ℤring RingHom R ) )
Theorem	zrhval2 15003*	Alternate value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- L = ( ZRHom ` R )   &    |- .x. = (.g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> L = ( n e. ZZ |-> ( n .x. .1. ) ) )
Theorem	zrhmulg 15004	Value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- L = ( ZRHom ` R )   &    |- .x. = (.g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ N e. ZZ ) -> ( L ` N ) = ( N .x. .1. ) )
Theorem	zrhex 15005	Set existence for ZRHom. (Contributed by Jim Kingdon, 19-May-2025.)
|- L = ( ZRHom ` R )   =>    |- ( R e. V -> L e. _V )
Theorem	zrhrhmb 15006	The ZRHom homomorphism is the unique ring homomorphism from ZZ. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. Ring -> ( F e. (ℤring RingHom R ) <-> F = L ) )
Theorem	zrhrhm 15007	The ZRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. Ring -> L e. (ℤring RingHom R ) )
Theorem	zrh1 15008	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- L = ( ZRHom ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( L ` 1 ) = .1. )
Theorem	zrh0 15009	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( L ` 0 ) = .0. )
Theorem	zrhpropd 15010*	The ZZ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-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 -> ( ZRHom ` K ) = ( ZRHom ` L ) )
Theorem	zlmval 15011	Augment an abelian group with vector space operations to turn it into a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> W = ( ( G sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )
Theorem	zlmlemg 15012	Lemma for zlmbasg 15013 and zlmplusgg 15014. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( E ` ndx ) =/= (Scalar ` ndx )   &    |- ( E ` ndx ) =/= ( .s ` ndx )   =>    |- ( G e. V -> ( E ` G ) = ( E ` W ) )
Theorem	zlmbasg 15013	Base set of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- B = ( Base ` G )   =>    |- ( G e. V -> B = ( Base ` W ) )
Theorem	zlmplusgg 15014	Group operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. V -> .+ = ( +g ` W ) )
Theorem	zlmmulrg 15015	Ring operation of a ZZ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- .x. = ( .r ` G )   =>    |- ( G e. V -> .x. = ( .r ` W ) )
Theorem	zlmsca 15016	Scalar ring of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
|- W = ( ZMod ` G )   =>    |- ( G e. V -> ℤring = (Scalar ` W ) )
Theorem	zlmvscag 15017	Scalar multiplication operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> .x. = ( .s ` W ) )
Theorem	znlidl 15018	The set n ZZ is an ideal in ZZ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   =>    |- ( N e. ZZ -> ( S ` { N } ) e. (LIdeal ` ℤring ) )
Theorem	zncrng2 15019	Making a commutative ring as a quotient of ZZ and n ZZ. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   =>    |- ( N e. ZZ -> U e. CRing )
Theorem	znval 15020	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, with an "artificial" ordering added. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` U ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( ( F o. <_ ) o. `' F )   =>    |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
Theorem	znle 15021	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, with an "artificial" ordering added. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` U ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
Theorem	znval2 15022	Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
Theorem	znbaslemnn 15023	Lemma for znbas 15028. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( E ` ndx ) =/= ( le ` ndx )   =>    |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )
Theorem	znbas2 15024	The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) )
Theorem	znadd 15025	The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) )
Theorem	znmul 15026	The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) )
Theorem	znzrh 15027	The ZZ ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( ZRHom ` U ) = ( ZRHom ` Y ) )
Theorem	znbas 15028	The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- Y = (ℤ/nℤ ` N )   &    |- R = (ℤring ~QG ( S ` { N } ) )   =>    |- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )
Theorem	zncrng 15029	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> Y e. CRing )
Theorem	znzrh2 15030*	The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- .~ = (ℤring ~QG ( S ` { N } ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) )
Theorem	znzrhval 15031	The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- .~ = (ℤring ~QG ( S ` { N } ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ )
Theorem	znzrhfo 15032	The ZZ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L : ZZ -onto-> B )
Theorem	zndvds 15033	Express equality of equivalence classes in ZZ / n ZZ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` A ) = ( L ` B ) <-> N || ( A - B ) ) )
Theorem	zndvds0 15034	Special case of zndvds 15033 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   &    |- .0. = ( 0g ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) = .0. <-> N || A ) )
Theorem	znf1o 15035	The function F enumerates all equivalence classes in ℤ/nℤ for each n. When n = 0, ZZ / 0 ZZ = ZZ / { 0 } ~~ ZZ so we let W = ZZ; otherwise W = { 0 , ... , n - 1 } enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   =>    |- ( N e. NN0 -> F : W -1-1-onto-> B )
Theorem	znle2 15036	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
Theorem	znleval 15037	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   &    |- X = ( Base ` Y )   =>    |- ( N e. NN0 -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
Theorem	znleval2 15038	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   &    |- X = ( Base ` Y )   =>    |- ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A .<_ B <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
Theorem	znfi 15039	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   =>    |- ( N e. NN -> B e. Fin )
Theorem	znhash 15040	The ℤ/nℤ structure has n elements. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   =>    |- ( N e. NN -> (♯ ` B ) = N )
Theorem	znidom 15041	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 15042	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 15043	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 15044	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 14352), but the existence of a unity element is always assumed (our rings are unital, see df-ring 14351). 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 15045	Associative algebra.
class AssAlg
Syntax	casp 15046	Algebraic span function.
class AlgSpan
Syntax	cascl 15047	Class of algebra scalar lifting function.
class algSc
Definition	df-assa 15048*	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 15049*	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 15050*	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 15051*	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 15052	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 15053	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 15054	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 15055	An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. LMod )
Theorem	assaring 15056	An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( W e. AssAlg -> W e. Ring )
Theorem	assasca 15057	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 15058	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 15059	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 15060*	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 15061	A subring that is also a subspace is a subalgebra. The key theorem is islss3 14765. (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 15062	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 15063*	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 15064*	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 15065	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 15066	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 15067	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 15068	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 15069	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 15070*	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 15071	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 15072	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 15073	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 15074	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 15075	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 15076	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 15077	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 15078	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 15079	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 15080	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 15081	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 15082	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 15083	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 15084	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 15085	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 15086	(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 15087	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 15088	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 15089*	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 15090	Lemma 1 for assamulgscm 15092 (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 15091	Lemma for assamulgscm 15092 (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 15092	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 15093	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 15094	Multivariate power series.
class mPwSer
Syntax	cmpl 15095	Multivariate polynomials.
class mPoly
Definition	df-psr 15096*	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 15097*	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 15098	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPwSer
Theorem	psrval 15099*	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 15100	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
|- mPwSer Fn ( _V X. _V )