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	ablpnpcan 14101	Cancellation law for mixed addition and subtraction. (pnpcan 8555 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 14102	Cancellation law for group subtraction. (nncan 8545 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 14103	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 14104	Cancellation law for group subtraction. (nnncan 8551 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 14105	Cancellation law for group subtraction. (nnncan1 8552 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 14106	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 14107*	The function fulfilling the conditions of ghmgrp 13898 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 14108*	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 14109*	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 14110	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 14111	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 14112	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 14113	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 14114	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 14115	Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( G e. Abel -> (NrmSGrp ` G ) = (SubGrp ` G ) )
Theorem	ablressid 14116	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 13402. (Contributed by Jim Kingdon, 5-May-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Abel -> ( G ↾s B ) e. Abel )
Theorem	imasabl 14117*	The image structure of an abelian group is an abelian group (imasgrp 13891 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 14118	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 14119	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 14120*	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 14121*	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 14122	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 14123*	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 14124*	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 14125	Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gzsumsplit1r 13692 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 14126*	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 14127	Extend class notation to include group sums over finite sets.
class gsumg
Definition	df-gsumfi 14128*	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 13590. (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 14129	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 14130	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 14131	An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- ( G e. CMnd -> ( G gsumg (/) ) = ( 0g ` G ) )
Theorem	gzsumgsum 14132	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 14133*	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 14134	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 14135*	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 14136	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 14137	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 14138*	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 14139*	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 14140	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 14141	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 14142*	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 14143*	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 14144*	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 14145	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 14146	The function constructing structure products.
class X_s
Definition	df-prds 14147*	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 14148	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 14149	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 14150*	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 14151	Lemma for prdsbas 14153 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 14152	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 14153*	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 14154*	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 14155*	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 14156*	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 14157*	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 14158	Points in the structure product are functions; use this with dffn5im 5742 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 14159	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 14160*	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 14161	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 14162*	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 14163	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 14164*	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 14165*	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 14166*	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 14167	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 14168	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 14169	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 14170*	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 14171	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 14172	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 14173*	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 14174	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 14175*	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 14176	Binary product structure function.
class X.s
Definition	df-xps 14177*	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 >. } ) ) )
Theorem	xpsval 14178*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )   &    |- G = (Scalar ` R )   &    |- U = ( G X_s { <. (/) , R >. , <. 1o , S >. } )   =>    |- ( ph -> T = ( `' F "s U ) )
7.2.9  Structure power
Syntax	cpws 14179	The function constructing structure powers.
class ^s
Definition	df-pws 14180*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
Theorem	pwsval 14181	Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- F = (Scalar ` R )   =>    |- ( ( R e. V /\ I e. W ) -> Y = ( F X_s ( I X. { R } ) ) )
Theorem	pwsbas 14182	Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   =>    |- ( ( R e. V /\ I e. W ) -> ( B ^m I ) = ( Base ` Y ) )
Theorem	pwselbasb 14183	Membership in the base set of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- V = ( Base ` Y )   =>    |- ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )
Theorem	pwselbas 14184	An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- V = ( Base ` Y )   &    |- ( ph -> R e. W )   &    |- ( ph -> I e. Z )   &    |- ( ph -> X e. V )   =>    |- ( ph -> X : I --> B )
Theorem	pwsplusgval 14185	Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` Y )   =>    |- ( ph -> ( F .+b G ) = ( F oF .+ G ) )
Theorem	pwsmulrval 14186	Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` Y )   =>    |- ( ph -> ( F .xb G ) = ( F oF .x. G ) )
Theorem	pwsdiagel 14187	Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- C = ( Base ` Y )   =>    |- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( I X. { A } ) e. C )
Theorem	pwssnf1o 14188*	Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s { I } )   &    |- B = ( Base ` R )   &    |- F = ( x e. B |-> ( { I } X. { x } ) )   &    |- C = ( Base ` Y )   =>    |- ( ( R e. V /\ I e. W ) -> F : B -1-1-onto-> C )
Theorem	pwsmnd 14189	The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Mnd /\ I e. V ) -> Y e. Mnd )
Theorem	pws0g 14190	The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g ` Y ) )
Theorem	pwsgrp 14191	A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Grp /\ I e. V ) -> Y e. Grp )
Theorem	pwsinvg 14192	Negation in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- M = ( invg ` R )   &    |- N = ( invg ` Y )   =>    |- ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( N ` X ) = ( M o. X ) )
Theorem	pwssub 14193	Subtraction in a structure power. (Contributed by Mario Carneiro, 12-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- M = ( -g ` R )   &    |- .- = ( -g ` Y )   =>    |- ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F oF M G ) )
7.3  Rings
7.3.1  Multiplicative Group
Syntax	cmgp 14194	Multiplicative group.
class mulGrp
Definition	df-mgp 14195	Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" or "the multiplicative identity" in terms of the identity of a monoid (df-ur 14238). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 14196	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V
Theorem	mgpvalg 14197	Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. V -> M = ( R sSet <. ( +g ` ndx ) , .x. >. ) )
Theorem	mgpplusgg 14198	Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. V -> .x. = ( +g ` M ) )
Theorem	mgpex 14199	Existence of the multiplication group. If R is known to be a semiring, see srgmgp 14246. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- M = (mulGrp ` R )   =>    |- ( R e. V -> M e. _V )
Theorem	mgpbasg 14200	Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. V -> B = ( Base ` M ) )