P. 130 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12901-13000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	basendxnocndx 12901	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( Base ` ndx ) =/= ( oc ` ndx )
Theorem	plendxnocndx 12902	The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( le ` ndx ) =/= ( oc ` ndx )
Theorem	dsndx 12903	Index value of the df-ds 12788 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 12904	Utility theorem: index-independent form of df-ds 12788. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	dsslid 12905	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
|- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN )
Theorem	dsndxnn 12906	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( dist ` ndx ) e. NN
Theorem	basendxltdsndx 12907	The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( dist ` ndx )
Theorem	dsndxnbasendx 12908	The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.)
|- ( dist ` ndx ) =/= ( Base ` ndx )
Theorem	dsndxnplusgndx 12909	The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( dist ` ndx ) =/= ( +g ` ndx )
Theorem	dsndxnmulrndx 12910	The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- ( dist ` ndx ) =/= ( .r ` ndx )
Theorem	slotsdnscsi 12911	The slots Scalar, .s and .i are different from the slot dist. (Contributed by AV, 29-Oct-2024.)
|- ( ( dist ` ndx ) =/= (Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
Theorem	dsndxntsetndx 12912	The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( dist ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifdsndx 12913	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
|- ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )
Theorem	unifndx 12914	Index value of the df-unif 12789 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
|- ( UnifSet ` ndx ) = ; 1 3
Theorem	unifid 12915	Utility theorem: index-independent form of df-unif 12789. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	unifndxnn 12916	The index of the slot for the uniform set in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( UnifSet ` ndx ) e. NN
Theorem	basendxltunifndx 12917	The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( UnifSet ` ndx )
Theorem	unifndxnbasendx 12918	The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
|- ( UnifSet ` ndx ) =/= ( Base ` ndx )
Theorem	unifndxntsetndx 12919	The slot for the uniform set is not the slot for the topology in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( UnifSet ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifunifndx 12920	The index of the slot for the uniform set is not the index of other slots. (Contributed by AV, 10-Nov-2024.)
|- ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )
Theorem	homndx 12921	Index value of the df-hom 12790 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- ( Hom ` ndx ) = ; 1 4
Theorem	homid 12922	Utility theorem: index-independent form of df-hom 12790. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	homslid 12923	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
Theorem	ccondx 12924	Index value of the df-cco 12791 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- (comp ` ndx ) = ; 1 5
Theorem	ccoid 12925	Utility theorem: index-independent form of df-cco 12791. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	ccoslid 12926	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
6.1.3  Definition of the structure product
Syntax	crest 12927	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 12928	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 12929*	Function returning the subspace topology induced by the topology y and the set x. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
Definition	df-topn 12930	Define the topology extractor function. This differs from df-tset 12785 when a structure has been restricted using df-iress 12697; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
Theorem	restfn 12931	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 12932	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 12933*	The subspace topology induced by the topology J on the set A. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ran ( x e. J |-> ( x i^i A ) ) )
Theorem	elrest 12934*	The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. V /\ B e. W ) -> ( A e. ( J ↾t B ) <-> E. x e. J A = ( x i^i B ) ) )
Theorem	elrestr 12935	Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. V /\ S e. W /\ A e. J ) -> ( A i^i S ) e. ( J ↾t S ) )
Theorem	restid2 12936	The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( A e. V /\ J C_ ~P A ) -> ( J ↾t A ) = J )
Theorem	restsspw 12937	The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J ↾t A ) C_ ~P A
Theorem	restid 12938	The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( J e. V -> ( J ↾t X ) = J )
Theorem	topnvalg 12939	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( W e. V -> ( J ↾t B ) = ( TopOpen ` W ) )
Theorem	topnidg 12940	Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( ( W e. V /\ J C_ ~P B ) -> J = ( TopOpen ` W ) )
Theorem	topnpropgd 12941	The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> (TopSet ` K ) = (TopSet ` L ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. W )   =>    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
Syntax	ctg 12942	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 12943	Extend class notation with a function whose value is a product topology.
class Xt_
Syntax	c0g 12944	Extend class notation with group identity element.
class 0g
Syntax	cgsu 12945	Extend class notation to include finitely supported group sums.
class gsumg
Definition	df-0g 12946*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-igsum 12947. The related theorems will be provided later. (Contributed by NM, 20-Aug-2011.)
|- 0g = ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )
Definition	df-igsum 12947*	Define a finite group sum (also called "iterated sum") of a structure. 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. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set A and each demanding different properties of G. 1. If A = (/) and G has an identity element, then the sum equals this identity. 2. If A = ( M ... N ) and G is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ( ( F ` 1 ) + ( F ` 2 ) ) + ( F ` 3 ), etc. 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)
|- gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )
Definition	df-topgen 12948*	Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78. (Contributed by NM, 16-Jul-2006.)
|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
Definition	df-pt 12949*	Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- Xt_ = ( f e. _V |-> ( topGen ` { x | E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) } ) )
Theorem	tgval 12950*	The topology generated by a basis. See also tgval2 14313 and tgval3 14320. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )
Theorem	tgvalex 12951	The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
|- ( B e. V -> ( topGen ` B ) e. _V )
Theorem	ptex 12952	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
|- ( F e. V -> ( Xt_ ` F ) e. _V )
Syntax	cprds 12953	The function constructing structure products.
class X_s
Syntax	cpws 12954	The function constructing structure powers.
class ^s
Definition	df-prds 12955*	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 12956	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 12957	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	imasvalstrd 12958	An image structure value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Z )   &    |- ( ph -> ., e. P )   &    |- ( ph -> O e. Q )   &    |- ( ph -> L e. R )   &    |- ( ph -> D e. A )   =>    |- ( ph -> U Struct <. 1 , ; 1 2 >. )
Theorem	prdsvalstrd 12959	Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Z )   &    |- ( ph -> ., e. P )   &    |- ( ph -> O e. Q )   &    |- ( ph -> L e. R )   &    |- ( ph -> D e. A )   &    |- ( ph -> H e. T )   &    |- ( ph -> .xb e. U )   =>    |- ( ph -> ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) Struct <. 1 , ; 1 5 >. )
Theorem	prdsvallem 12960*	Lemma for prdsval 12961. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 12961, dependency on df-hom 12790 removed. (Revised by AV, 13-Oct-2024.)
|- ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V
Theorem	prdsval 12961*	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 12962	Lemma for prdsbas 12964 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 12963	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 12964*	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 12965*	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 12966*	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 ) ) ) ) )
Definition	df-pws 12967*	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 } ) ) )
6.1.4  Definition of the structure quotient
Syntax	cimas 12968	Image structure function.
class "s
Syntax	cqus 12969	Quotient structure function.
class /.s
Syntax	cxps 12970	Binary product structure function.
class X.s
Definition	df-iimas 12971*	Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly f must either be injective or satisfy the well-definedness condition f ( a ) = f ( c ) /\ f ( b ) = f ( d ) -> f ( a + b ) = f ( c + d ) for each relevant operation. Note that although we call this an "image" by association to df-ima 4677, in order to keep the definition simple we consider only the case when the domain of F is equal to the base set of R. Other cases can be achieved by restricting F (with df-res 4676) and/or R ( with df-iress 12697) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)
|- "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } )
Definition	df-qus 12972*	Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 12971 where the image function is x |-> [ x ] e. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
Definition	df-xps 12973*	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	imasex 12974	Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.)
|- ( ( F e. V /\ R e. W ) -> ( F "s R ) e. _V )
Theorem	imasival 12975*	Value of an image structure. The is a lemma for the theorems imasbas 12976, imasplusg 12977, and imasmulr 12978 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- .x. = ( .s ` R )   &    |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
Theorem	imasbas 12976	The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> B = ( Base ` U ) )
Theorem	imasplusg 12977*	The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` U )   =>    |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
Theorem	imasmulr 12978*	The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
Theorem	f1ocpbllem 12979	Lemma for f1ocpbl 12980. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A = C /\ B = D ) ) )
Theorem	f1ocpbl 12980	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )
Theorem	f1ovscpbl 12981	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( F ` B ) = ( F ` C ) -> ( F ` ( A .+ B ) ) = ( F ` ( A .+ C ) ) ) )
Theorem	f1olecpbl 12982	An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( A N B <-> C N D ) ) )
Theorem	imasaddfnlemg 12983*	The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> V e. W )   &    |- ( ph -> .x. e. C )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasaddvallemg 12984*	The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> V e. W )   &    |- ( ph -> .x. e. C )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasaddflemg 12985*	The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> V e. W )   &    |- ( ph -> .x. e. C )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasaddfn 12986*	The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasaddval 12987*	The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasaddf 12988*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasmulfn 12989*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasmulval 12990*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasmulf 12991*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( 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 .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	qusval 12992*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = ( F "s R ) )
Theorem	quslem 12993*	The function in qusval 12992 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> F : V -onto-> ( V /. .~ ) )
Theorem	qusex 12994	Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( ( R e. V /\ .~ e. W ) -> ( R /.s .~ ) e. _V )
Theorem	qusin 12995	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( .~ " V ) C_ V )   =>    |- ( ph -> U = ( R /.s ( .~ i^i ( V X. V ) ) ) )
Theorem	qusbas 12996	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> ( V /. .~ ) = ( Base ` U ) )
Theorem	divsfval 12997*	Value of the function in qusval 12992. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	divsfvalg 12998*	Value of the function in qusval 12992. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	ercpbllemg 12999*	Lemma for ercpbl 13000. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   =>    |- ( ph -> ( ( F ` A ) = ( F ` B ) <-> A .~ B ) )
Theorem	ercpbl 13000*	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a .+ b ) e. V )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )