P. 142 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14101-14200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscmnd 14101*	Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. CMnd )
Theorem	isabld 14102*	Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. Abel )
Theorem	isabli 14103*	Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
|- G e. Grp   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- G e. Abel
Theorem	cmnmnd 14104	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. CMnd -> G e. Mnd )
Theorem	cmncom 14105	A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	ablcom 14106	An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	cmn32 14107	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmn4 14108	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
Theorem	cmn12 14109	Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
Theorem	abl32 14110	Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmnmndd 14111	A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. CMnd )   =>    |- ( ph -> G e. Mnd )
Theorem	cmnsubm 14112	A submonoid of a commutative monoid is commutative. (Contributed by Jim Kingdon, 7-Jul-2026.)
|- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> G e. CMnd )   &    |- H = ( G ↾s S )   =>    |- ( ph -> H e. CMnd )
Theorem	rinvmod 14113*	Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6283. (Contributed by AV, 31-Dec-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E* w e. B ( A .+ w ) = .0. )
Theorem	ablinvadd 14114	The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( N ` ( X .+ Y ) ) = ( ( N ` X ) .+ ( N ` Y ) ) )
Theorem	ablsub2inv 14115	Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( Y .- X ) )
Theorem	ablsubadd 14116	Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Y .+ Z ) = X ) )
Theorem	ablsub4 14117	Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) )
Theorem	abladdsub4 14118	Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) = ( Z .+ W ) <-> ( X .- Z ) = ( W .- Y ) ) )
Theorem	abladdsub 14119	Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( X .- Z ) .+ Y ) )
Theorem	ablpncan2 14120	Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = Y )
Theorem	ablpncan3 14121	A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = Y )
Theorem	ablsubsub 14122	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .- ( Y .- Z ) ) = ( ( X .- Y ) .+ Z ) )
Theorem	ablsubsub4 14123	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y .+ Z ) ) )
Theorem	ablpnpcan 14124	Cancellation law for mixed addition and subtraction. (pnpcan 8565 analog.) (Contributed by NM, 29-May-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( Y .- Z ) )
Theorem	ablnncan 14125	Cancellation law for group subtraction. (nncan 8555 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .- ( X .- Y ) ) = Y )
Theorem	ablsub32 14126	Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- Z ) .- Y ) )
Theorem	ablnnncan 14127	Cancellation law for group subtraction. (nnncan 8561 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- ( Y .- Z ) ) .- Z ) = ( X .- Y ) )
Theorem	ablnnncan1 14128	Cancellation law for group subtraction. (nnncan1 8562 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( Z .- Y ) )
Theorem	ablsubsub23 14129	Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( A .- C ) = B ) )
Theorem	ghmfghm 14130*	The function fulfilling the conditions of ghmgrp 13921 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> F e. ( G GrpHom H ) )
Theorem	ghmcmn 14131*	The image of a commutative monoid G under a group homomorphism F is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. CMnd )   =>    |- ( ph -> H e. CMnd )
Theorem	ghmabl 14132*	The image of an abelian group G under a group homomorphism F is an abelian group. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.)
|- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Abel )   =>    |- ( ph -> H e. Abel )
Theorem	invghm 14133	The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. Abel <-> I e. ( G GrpHom G ) )
Theorem	eqgabl 14134	Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .~ = ( G ~QG S )   =>    |- ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) )
Theorem	qusecsub 14135	Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .~ = ( G ~QG S )   =>    |- ( ( ( G e. Abel /\ S e. (SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ = [ Y ] .~ <-> ( Y .- X ) e. S ) )
Theorem	subgabl 14136	A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- H = ( G ↾s S )   =>    |- ( ( G e. Abel /\ S e. (SubGrp ` G ) ) -> H e. Abel )
Theorem	subcmnd 14137	A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- ( ph -> H = ( G ↾s S ) )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> S e. V )   =>    |- ( ph -> H e. CMnd )
Theorem	ablnsg 14138	Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( G e. Abel -> (NrmSGrp ` G ) = (SubGrp ` G ) )
Theorem	ablressid 14139	A commutative group restricted to its base set is a commutative group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 13425. (Contributed by Jim Kingdon, 5-May-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Abel -> ( G ↾s B ) e. Abel )
Theorem	imasabl 14140*	The image structure of an abelian group is an abelian group (imasgrp 13914 analog). (Contributed by AV, 22-Feb-2025.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ph -> R e. Abel )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( U e. Abel /\ ( F ` .0. ) = ( 0g ` U ) ) )
7.2.5.2  Group sum operation
Theorem	gzsumreidx 14141	Re-index a finite group sum using a bijection. Corresponds to the first equation in [Lang] p. 5 with M = 1. (Contributed by AV, 26-Dec-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   &    |- ( ph -> H : ( M ... N ) -1-1-onto-> ( M ... N ) )   =>    |- ( ph -> ( G gzsumgz F ) = ( G gzsumgz ( F o. H ) ) )
Theorem	gzsumsubmcl 14142	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.)
|- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : ( M ... N ) --> S )   =>    |- ( ph -> ( G gzsumgz F ) e. S )
Theorem	gzsumconst 14143*	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> ( G gzsumgz ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) )
Theorem	gzsumconstf 14144*	Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.)
|- F/_ k X   &    |- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> ( G gzsumgz ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) )
Theorem	gzsummhm 14145	Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( H gzsumgz ( K o. F ) ) = ( K ` ( G gzsumgz F ) ) )
Theorem	gzsummhm2 14146*	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> X e. B )   &    |- ( x = X -> C = D )   &    |- ( x = ( G gzsumgz ( k e. ( M ... N ) |-> X ) ) -> C = E )   =>    |- ( ph -> ( H gzsumgz ( k e. ( M ... N ) |-> D ) ) = E )
Theorem	gzsumsnfd 14147*	Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Revised by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ k = M ) -> A = C )   &    |- F/ k ph   &    |- F/_ k C   =>    |- ( ph -> ( G gzsumgz ( k e. { M } |-> A ) ) = C )
Theorem	gzsumsplit0 14148	Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gzsumsplit1r 13715 except that N can equal M - 1. (Contributed by Jim Kingdon, 4-Apr-2026.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M - 1 ) ) )   &    |- ( ph -> F : ( M ... ( N + 1 ) ) --> B )   =>    |- ( ph -> ( G gzsumgz F ) = ( ( G gzsumgz ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	gzsumshift 14149*	Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) --> B )   &    |- S = ( j e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( j - ( 1 - M ) ) )   =>    |- ( ph -> ( G gzsumgz F ) = ( G gzsumgz ( F o. S ) ) )
7.2.6  Finite group sum over unordered finite set
Syntax	cgsu 14150	Extend class notation to include group sums over finite sets.
class gsumg
Definition	df-gsumfi 14151*	Define the finite group sum (iterated sum) over an unordered finite set. Given G gsumg F where F : A --> ( Base ` G ), the set of indices is A and the values are given by F at each index. For this notation, A is a finite set and G is a commutative monoid, and the sum adds up these elements in some order (the sum does not depend on the order). For a sum indexed by consecutive integers (and thus defining an order for the sum), see df-gzsum 13613. (Contributed by Jim Kingdon, 23-Mar-2026.)
|- gsumg = ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) ) ) ) )
Theorem	gsumvalfi 14152	Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)
|- B = ( Base ` W )   &    |- ( ph -> W e. CMnd )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )   =>    |- ( ph -> ( W gsumg F ) = ( W gzsumgz ( F o. G ) ) )
Theorem	gzsumgsum1 14153	On an integer range starting at one, gzsumgz and gsumg agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> F : ( 1 ... N ) --> B )   =>    |- ( ph -> ( G gzsumgz F ) = ( G gsumg F ) )
Theorem	gsum0cmn 14154	An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- ( G e. CMnd -> ( G gsumg (/) ) = ( 0g ` G ) )
Theorem	gzsumgsum 14155	On an integer range, gzsumgz and gsumg agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gzsumgz F ) = ( G gsumg F ) )
Theorem	gsumsncmn 14156*	Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
|- B = ( Base ` G )   &    |- ( k = M -> A = C )   =>    |- ( ( G e. CMnd /\ M e. V /\ C e. B ) -> ( G gsumg ( k e. { M } |-> A ) ) = C )
Theorem	gsump1 14157	Splitting off one element from a finite group sum. This would typically used in a proof by induction. (Contributed by Jim Kingdon, 3-Apr-2026.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F : ( Y u. { Z } ) --> B )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. Y )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` Y ) ) .+ ( F ` Z ) ) )
Theorem	gsumzfi 14158*	Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. CMnd /\ A e. Fin ) -> ( G gsumg ( k e. A |-> .0. ) ) = .0. )
Theorem	gsumclfi 14159	Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( G gsumg F ) e. B )
Theorem	gsumf1ofi 14160	Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> H : C -1-1-onto-> A )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
Theorem	gsummptfidmadd 14161*	The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- F = ( x e. A |-> C )   &    |- H = ( x e. A |-> D )   =>    |- ( ph -> ( G gsumg ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsummptfidmadd2 14162*	The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ x e. A ) -> D e. B )   &    |- F = ( x e. A |-> C )   &    |- H = ( x e. A |-> D )   =>    |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsumsubmclfi 14163	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
|- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : A --> S )   =>    |- ( ph -> ( G gsumg F ) e. S )
Theorem	gsummhmfi 14164	Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( H gsumg ( K o. F ) ) = ( K ` ( G gsumg F ) ) )
Theorem	gsummhm2fi 14165*	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( x = X -> C = D )   &    |- ( x = ( G gsumg ( k e. A |-> X ) ) -> C = E )   =>    |- ( ph -> ( H gsumg ( k e. A |-> D ) ) = E )
Theorem	gsumconstcmn 14166*	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. CMnd /\ A e. Fin /\ X e. B ) -> ( G gsumg ( k e. A |-> X ) ) = ( (♯ ` A ) .x. X ) )
Theorem	gsumressfi 14167*	The group sum in a substructure is the same as the group sum in the original structure. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- H = ( G ↾s S )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> S C_ B )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> .0. e. S )   &    |- ( ( ph /\ x e. B ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumsubmfi 14168	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F : A --> S )   &    |- H = ( G ↾s S )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
7.2.7  Structure product
Syntax	cprds 14169	The function constructing structure products.
class X_s
Definition	df-prds 14170*	Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- X_s = ( s e. _V , r e. _V |-> [_ X_ x e. dom r ( Base ` ( r ` x ) ) / v ]_ [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. (Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. (comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( ( 2nd ` a ) h c ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
Theorem	reldmprds 14171	The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)
|- Rel dom X_s
Theorem	prdsex 14172	Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.)
|- ( ( S e. V /\ R e. W ) -> ( S X_s R ) e. _V )
Theorem	prdsval 14173*	Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- P = ( S X_s R )   &    |- K = ( Base ` S )   &    |- ( ph -> dom R = I )   &    |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )   &    |- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )   &    |- ( ph -> .X. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )   &    |- ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )   &    |- ( ph -> ., = ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )   &    |- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )   &    |- ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )   &    |- ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )   &    |- ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )   &    |- ( ph -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) H c ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )   &    |- ( ph -> S e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) )
Theorem	prdsbaslemss 14174	Lemma for prdsbas 14176 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- A = ( E ` P )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( ph -> T e. X )   &    |- ( ph -> { <. ( E ` ndx ) , T >. } C_ P )   =>    |- ( ph -> A = T )
Theorem	prdssca 14175	Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> S = (Scalar ` P ) )
Theorem	prdsbas 14176*	Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   =>    |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
Theorem	prdsplusg 14177*	Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- .+ = ( +g ` P )   =>    |- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
Theorem	prdsmulr 14178*	Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- .x. = ( .r ` P )   =>    |- ( ph -> .x. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
Theorem	prdsbas2 14179*	The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   =>    |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
Theorem	prdsbasmpt 14180*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   =>    |- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. ( Base ` ( R ` x ) ) ) )
Theorem	prdsbasfn 14181	Points in the structure product are functions; use this with dffn5im 5748 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> T e. B )   =>    |- ( ph -> T Fn I )
Theorem	prdsbasprj 14182	Each point in a structure product restricts on each coordinate to the relevant base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> T e. B )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( T ` J ) e. ( Base ` ( R ` J ) ) )
Theorem	prdsplusgval 14183*	Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` Y )   =>    |- ( ph -> ( F .+ G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )
Theorem	prdsplusgfval 14184	Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( ( F .+ G ) ` J ) = ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) )
Theorem	prdsmulrval 14185*	Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` Y )   =>    |- ( ph -> ( F .x. G ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) )
Theorem	prdsmulrfval 14186	Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( ( F .x. G ) ` J ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )
Theorem	prdsbas3 14187*	The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- K = ( Base ` R )   =>    |- ( ph -> B = X_ x e. I K )
Theorem	prdsbasmpt2 14188*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- K = ( Base ` R )   =>    |- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. K ) )
Theorem	prdsbascl 14189*	An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- K = ( Base ` R )   &    |- ( ph -> F e. B )   =>    |- ( ph -> A. x e. I ( F ` x ) e. K )
Theorem	prdsplusgsgrpcl 14190	Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I -->Smgrp )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .+ G ) e. B )
Theorem	prdssgrpd 14191	The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I -->Smgrp )   =>    |- ( ph -> Y e. Smgrp )
Theorem	prdsplusgcl 14192	Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Mnd )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .+ G ) e. B )
Theorem	prdsidlem 14193*	Characterization of identity in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Mnd )   &    |- .0. = ( 0g o. R )   =>    |- ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
Theorem	prdsmndd 14194	The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Mnd )   =>    |- ( ph -> Y e. Mnd )
Theorem	prds0g 14195	The identity in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Mnd )   =>    |- ( ph -> ( 0g o. R ) = ( 0g ` Y ) )
Theorem	prdsinvlem 14196*	Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Grp )   &    |- ( ph -> F e. B )   &    |- .0. = ( 0g o. R )   &    |- N = ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) )   =>    |- ( ph -> ( N e. B /\ ( N .+ F ) = .0. ) )
Theorem	prdsgrpd 14197	The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Grp )   =>    |- ( ph -> Y e. Grp )
Theorem	prdsinvgd 14198*	Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Grp )   &    |- B = ( Base ` Y )   &    |- N = ( invg ` Y )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) )
7.2.8  Binary product on structures
Syntax	cxps 14199	Binary product structure function.
class X.s
Definition	df-xps 14200*	Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
|- X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) ) )