![]() |
Metamath
Proof Explorer Theorem List (p. 150 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | repsw2 14901 | The "repeated symbol word" of length two. (Contributed by AV, 6-Nov-2018.) |
β’ (π β π β (π repeatS 2) = β¨βππββ©) | ||
Theorem | repsw3 14902 | The "repeated symbol word" of length three. (Contributed by AV, 6-Nov-2018.) |
β’ (π β π β (π repeatS 3) = β¨βπππββ©) | ||
Theorem | swrd2lsw 14903 | Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
β’ ((π β Word π β§ 1 < (β―βπ)) β (π substr β¨((β―βπ) β 2), (β―βπ)β©) = β¨β(πβ((β―βπ) β 2))(lastSβπ)ββ©) | ||
Theorem | 2swrd2eqwrdeq 14904 | Two words of length at least two are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018.) (Revised by AV, 12-Oct-2022.) |
β’ ((π β Word π β§ π β Word π β§ 1 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 2)) = (π prefix ((β―βπ) β 2)) β§ (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 2)) β§ (lastSβπ) = (lastSβπ))))) | ||
Theorem | ccatw2s1ccatws2 14905 | The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018.) (Revised by AV, 29-Jan-2024.) |
β’ (π β Word π β ((π ++ β¨βπββ©) ++ β¨βπββ©) = (π ++ β¨βππββ©)) | ||
Theorem | ccat2s1fvwALT 14906 | Alternate proof of ccat2s1fvw 14588 using words of length 2, see df-s2 14799. A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018.) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018.) (Revised by AV, 28-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ ((π β Word π β§ πΌ β β0 β§ πΌ < (β―βπ)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)βπΌ) = (πβπΌ)) | ||
Theorem | wwlktovf 14907* | Lemma 1 for wrd2f1tovbij 14911. (Contributed by Alexander van der Vekens, 27-Jul-2018.) |
β’ π· = {π€ β Word π β£ ((β―βπ€) = 2 β§ (π€β0) = π β§ {(π€β0), (π€β1)} β π)} & β’ π = {π β π β£ {π, π} β π} & β’ πΉ = (π‘ β π· β¦ (π‘β1)) β β’ πΉ:π·βΆπ | ||
Theorem | wwlktovf1 14908* | Lemma 2 for wrd2f1tovbij 14911. (Contributed by Alexander van der Vekens, 27-Jul-2018.) |
β’ π· = {π€ β Word π β£ ((β―βπ€) = 2 β§ (π€β0) = π β§ {(π€β0), (π€β1)} β π)} & β’ π = {π β π β£ {π, π} β π} & β’ πΉ = (π‘ β π· β¦ (π‘β1)) β β’ πΉ:π·β1-1βπ | ||
Theorem | wwlktovfo 14909* | Lemma 3 for wrd2f1tovbij 14911. (Contributed by Alexander van der Vekens, 27-Jul-2018.) |
β’ π· = {π€ β Word π β£ ((β―βπ€) = 2 β§ (π€β0) = π β§ {(π€β0), (π€β1)} β π)} & β’ π = {π β π β£ {π, π} β π} & β’ πΉ = (π‘ β π· β¦ (π‘β1)) β β’ (π β π β πΉ:π·βontoβπ ) | ||
Theorem | wwlktovf1o 14910* | Lemma 4 for wrd2f1tovbij 14911. (Contributed by Alexander van der Vekens, 28-Jul-2018.) |
β’ π· = {π€ β Word π β£ ((β―βπ€) = 2 β§ (π€β0) = π β§ {(π€β0), (π€β1)} β π)} & β’ π = {π β π β£ {π, π} β π} & β’ πΉ = (π‘ β π· β¦ (π‘β1)) β β’ (π β π β πΉ:π·β1-1-ontoβπ ) | ||
Theorem | wrd2f1tovbij 14911* | There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018.) |
β’ ((π β π β§ π β π) β βπ π:{π€ β Word π β£ ((β―βπ€) = 2 β§ (π€β0) = π β§ {(π€β0), (π€β1)} β π)}β1-1-ontoβ{π β π β£ {π, π} β π}) | ||
Theorem | eqwrds3 14912 | A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021.) |
β’ ((π β Word π β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π = β¨βπ΄π΅πΆββ© β ((β―βπ) = 3 β§ ((πβ0) = π΄ β§ (πβ1) = π΅ β§ (πβ2) = πΆ)))) | ||
Theorem | wrdl3s3 14913* | A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.) |
β’ ((π β Word π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π π = β¨βπππββ©) | ||
Theorem | s3sndisj 14914* | The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.) |
β’ ((π΄ β π β§ π΅ β π) β Disj π β π {β¨βπ΄π΅πββ©}) | ||
Theorem | s3iunsndisj 14915* | The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021.) |
β’ (π΅ β π β Disj π β π βͺ π β (π β {π}){β¨βππ΅πββ©}) | ||
Theorem | ofccat 14916 | Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
β’ (π β πΈ β Word π) & β’ (π β πΉ β Word π) & β’ (π β πΊ β Word π) & β’ (π β π» β Word π) & β’ (π β (β―βπΈ) = (β―βπΊ)) & β’ (π β (β―βπΉ) = (β―βπ»)) β β’ (π β ((πΈ ++ πΉ) βf π (πΊ ++ π»)) = ((πΈ βf π πΊ) ++ (πΉ βf π π»))) | ||
Theorem | ofs1 14917 | Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
β’ ((π΄ β π β§ π΅ β π) β (β¨βπ΄ββ© βf π β¨βπ΅ββ©) = β¨β(π΄π π΅)ββ©) | ||
Theorem | ofs2 14918 | Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
β’ (((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (β¨βπ΄π΅ββ© βf π β¨βπΆπ·ββ©) = β¨β(π΄π πΆ)(π΅π π·)ββ©) | ||
A relation, π , has the reflexive property if π΄π π΄ holds whenever π΄ is an element which could be related by the relation, namely, an element of its domain or range. Eliminating dummy variables, we see that a segment of the identity relation must be a subset of the relation, or ( I βΎ (ran π βͺ dom π )) β π . See idref 7144. A relation, π , has the transitive property if π΄π πΆ holds whenever there exists an intermediate value π΅ such that both π΄π π΅ and π΅π πΆ hold. This can be expressed without dummy variables as (π β π ) β π . See cotr 6112. The transitive closure of a relation, (t+βπ ), is the smallest superset of the relation which has the transitive property. Likewise, the reflexive-transitive closure, (t*βπ ), is the smallest superset which has both the reflexive and transitive properties. Not to be confused with the transitive closure of a set, trcl 9723, which is a closure relative to a different transitive property, df-tr 5267. | ||
Theorem | coss12d 14919 | Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.) |
β’ (π β π΄ β π΅) & β’ (π β πΆ β π·) β β’ (π β (π΄ β πΆ) β (π΅ β π·)) | ||
Theorem | trrelssd 14920 | The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.) |
β’ (π β (π β π ) β π ) & β’ (π β π β π ) & β’ (π β π β π ) β β’ (π β (π β π) β π ) | ||
Theorem | xpcogend 14921 | The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019.) |
β’ (π β (π΅ β© πΆ) β β ) β β’ (π β ((πΆ Γ π·) β (π΄ Γ π΅)) = (π΄ Γ π·)) | ||
Theorem | xpcoidgend 14922 | If two classes are not disjoint, then the composition of their Cartesian product with itself is idempotent. (Contributed by RP, 24-Dec-2019.) |
β’ (π β (π΄ β© π΅) β β ) β β’ (π β ((π΄ Γ π΅) β (π΄ Γ π΅)) = (π΄ Γ π΅)) | ||
Theorem | cotr2g 14923* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14924 for the main application. (Contributed by RP, 22-Mar-2020.) |
β’ dom π΅ β π· & β’ (ran π΅ β© dom π΄) β πΈ & β’ ran π΄ β πΉ β β’ ((π΄ β π΅) β πΆ β βπ₯ β π· βπ¦ β πΈ βπ§ β πΉ ((π₯π΅π¦ β§ π¦π΄π§) β π₯πΆπ§)) | ||
Theorem | cotr2 14924* | Two ways of saying a relation is transitive. Special instance of cotr2g 14923. (Contributed by RP, 22-Mar-2020.) |
β’ dom π β π΄ & β’ (dom π β© ran π ) β π΅ & β’ ran π β πΆ β β’ ((π β π ) β π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ ((π₯π π¦ β§ π¦π π§) β π₯π π§)) | ||
Theorem | cotr3 14925* | Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.) |
β’ π΄ = dom π & β’ π΅ = (π΄ β© πΆ) & β’ πΆ = ran π β β’ ((π β π ) β π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ ((π₯π π¦ β§ π¦π π§) β π₯π π§)) | ||
Theorem | coemptyd 14926 | Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.) |
β’ (π β (dom π΄ β© ran π΅) = β ) β β’ (π β (π΄ β π΅) = β ) | ||
Theorem | xptrrel 14927 | The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.) |
β’ ((π΄ Γ π΅) β (π΄ Γ π΅)) β (π΄ Γ π΅) | ||
Theorem | 0trrel 14928 | The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
β’ (β β β ) β β | ||
Theorem | cleq1lem 14929 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
β’ (π΄ = π΅ β ((π΄ β πΆ β§ π) β (π΅ β πΆ β§ π))) | ||
Theorem | cleq1 14930* | Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.) |
β’ (π = π β β© {π β£ (π β π β§ π)} = β© {π β£ (π β π β§ π)}) | ||
Theorem | clsslem 14931* | The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.) |
β’ (π β π β β© {π β£ (π β π β§ π)} β β© {π β£ (π β π β§ π)}) | ||
Syntax | ctcl 14932 | Extend class notation to include the transitive closure symbol. |
class t+ | ||
Syntax | crtcl 14933 | Extend class notation with reflexive-transitive closure. |
class t* | ||
Definition | df-trcl 14934* | Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011.) |
β’ t+ = (π₯ β V β¦ β© {π§ β£ (π₯ β π§ β§ (π§ β π§) β π§)}) | ||
Definition | df-rtrcl 14935* | Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011.) |
β’ t* = (π₯ β V β¦ β© {π§ β£ (( I βΎ (dom π₯ βͺ ran π₯)) β π§ β§ π₯ β π§ β§ (π§ β π§) β π§)}) | ||
Theorem | trcleq1 14936* | Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.) |
β’ (π = π β β© {π β£ (π β π β§ (π β π) β π)} = β© {π β£ (π β π β§ (π β π) β π)}) | ||
Theorem | trclsslem 14937* | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
β’ (π β π β β© {π β£ (π β π β§ (π β π) β π)} β β© {π β£ (π β π β§ (π β π) β π)}) | ||
Theorem | trcleq2lem 14938 | Equality implies bijection. (Contributed by RP, 5-May-2020.) |
β’ (π΄ = π΅ β ((π β π΄ β§ (π΄ β π΄) β π΄) β (π β π΅ β§ (π΅ β π΅) β π΅))) | ||
Theorem | cvbtrcl 14939* | Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.) |
β’ {π₯ β£ (π β π₯ β§ (π₯ β π₯) β π₯)} = {π¦ β£ (π β π¦ β§ (π¦ β π¦) β π¦)} | ||
Theorem | trcleq12lem 14940 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
β’ ((π = π β§ π΄ = π΅) β ((π β π΄ β§ (π΄ β π΄) β π΄) β (π β π΅ β§ (π΅ β π΅) β π΅))) | ||
Theorem | trclexlem 14941 | Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 5-May-2020.) |
β’ (π β π β (π βͺ (dom π Γ ran π )) β V) | ||
Theorem | trclublem 14942* | If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020.) |
β’ (π β π β (π βͺ (dom π Γ ran π )) β {π₯ β£ (π β π₯ β§ (π₯ β π₯) β π₯)}) | ||
Theorem | trclubi 14943* | The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020.) (Revised by RP, 28-Apr-2020.) (Revised by AV, 26-Mar-2021.) |
β’ Rel π & β’ π β V β β’ β© {π β£ (π β π β§ (π β π ) β π )} β (dom π Γ ran π ) | ||
Theorem | trclubgi 14944* | The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure. (Contributed by RP, 3-Jan-2020.) (Revised by RP, 28-Apr-2020.) (Revised by AV, 26-Mar-2021.) |
β’ π β V β β’ β© {π β£ (π β π β§ (π β π ) β π )} β (π βͺ (dom π Γ ran π )) | ||
Theorem | trclub 14945* | The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 17-May-2020.) |
β’ ((π β π β§ Rel π ) β β© {π β£ (π β π β§ (π β π) β π)} β (dom π Γ ran π )) | ||
Theorem | trclubg 14946* | The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure (as a relation). (Contributed by RP, 17-May-2020.) |
β’ (π β π β β© {π β£ (π β π β§ (π β π) β π)} β (π βͺ (dom π Γ ran π ))) | ||
Theorem | trclfv 14947* | The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.) |
β’ (π β π β (t+βπ ) = β© {π₯ β£ (π β π₯ β§ (π₯ β π₯) β π₯)}) | ||
Theorem | brintclab 14948* | Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.) |
β’ (π΄β© {π₯ β£ π}π΅ β βπ₯(π β β¨π΄, π΅β© β π₯)) | ||
Theorem | brtrclfv 14949* | Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.) |
β’ (π β π β (π΄(t+βπ )π΅ β βπ((π β π β§ (π β π) β π) β π΄ππ΅))) | ||
Theorem | brcnvtrclfv 14950* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.) |
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄β‘(t+βπ )π΅ β βπ((π β π β§ (π β π) β π) β π΅ππ΄))) | ||
Theorem | brtrclfvcnv 14951* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
β’ (π β π β (π΄(t+ββ‘π )π΅ β βπ((β‘π β π β§ (π β π) β π) β π΄ππ΅))) | ||
Theorem | brcnvtrclfvcnv 14952* | Two ways of expressing the transitive closure of the converse of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄β‘(t+ββ‘π )π΅ β βπ((β‘π β π β§ (π β π) β π) β π΅ππ΄))) | ||
Theorem | trclfvss 14953 | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
β’ ((π β π β§ π β π β§ π β π) β (t+βπ ) β (t+βπ)) | ||
Theorem | trclfvub 14954 | The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.) |
β’ (π β π β (t+βπ ) β (π βͺ (dom π Γ ran π ))) | ||
Theorem | trclfvlb 14955 | The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.) |
β’ (π β π β π β (t+βπ )) | ||
Theorem | trclfvcotr 14956 | The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.) |
β’ (π β π β ((t+βπ ) β (t+βπ )) β (t+βπ )) | ||
Theorem | trclfvlb2 14957 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
β’ (π β π β (π β π ) β (t+βπ )) | ||
Theorem | trclfvlb3 14958 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
β’ (π β π β (π βͺ (π β π )) β (t+βπ )) | ||
Theorem | cotrtrclfv 14959 | The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.) |
β’ ((π β π β§ (π β π ) β π ) β (t+βπ ) = π ) | ||
Theorem | trclidm 14960 | The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.) |
β’ (π β π β (t+β(t+βπ )) = (t+βπ )) | ||
Theorem | trclun 14961 | Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.) |
β’ ((π β π β§ π β π) β (t+β(π βͺ π)) = (t+β((t+βπ ) βͺ (t+βπ)))) | ||
Theorem | trclfvg 14962 | The value of the transitive closure of a relation is a superset or (for proper classes) the empty set. (Contributed by RP, 8-May-2020.) |
β’ (π β (t+βπ ) β¨ (t+βπ ) = β ) | ||
Theorem | trclfvcotrg 14963 | The value of the transitive closure of a relation is always a transitive relation. (Contributed by RP, 8-May-2020.) |
β’ ((t+βπ ) β (t+βπ )) β (t+βπ ) | ||
Theorem | reltrclfv 14964 | The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.) |
β’ ((π β π β§ Rel π ) β Rel (t+βπ )) | ||
Theorem | dmtrclfv 14965 | The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020.) |
β’ (π β π β dom (t+βπ ) = dom π ) | ||
Syntax | crelexp 14966 | Extend class notation to include relation exponentiation. |
class βπ | ||
Definition | df-relexp 14967* | Definition of repeated composition of a relation with itself, aka relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 22-May-2020.) |
β’ βπ = (π β V, π β β0 β¦ if(π = 0, ( I βΎ (dom π βͺ ran π)), (seq1((π₯ β V, π¦ β V β¦ (π₯ β π)), (π§ β V β¦ π))βπ))) | ||
Theorem | reldmrelexp 14968 | The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.) |
β’ Rel dom βπ | ||
Theorem | relexp0g 14969 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
β’ (π β π β (π βπ0) = ( I βΎ (dom π βͺ ran π ))) | ||
Theorem | relexp0 14970 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
β’ ((π β π β§ Rel π ) β (π βπ0) = ( I βΎ βͺ βͺ π )) | ||
Theorem | relexp0d 14971 | A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β π) β β’ (π β (π βπ0) = ( I βΎ βͺ βͺ π )) | ||
Theorem | relexpsucnnr 14972 | A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.) |
β’ ((π β π β§ π β β) β (π βπ(π + 1)) = ((π βππ) β π )) | ||
Theorem | relexp1g 14973 | A relation composed once is itself. (Contributed by RP, 22-May-2020.) |
β’ (π β π β (π βπ1) = π ) | ||
Theorem | dfid5 14974 | Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.) |
β’ I = (π₯ β V β¦ (π₯βπ1)) | ||
Theorem | dfid6 14975* | Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.) |
β’ I = (π₯ β V β¦ βͺ π β {1} (π₯βππ)) | ||
Theorem | relexp1d 14976 | A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β π) β β’ (π β (π βπ1) = π ) | ||
Theorem | relexpsucnnl 14977 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
β’ ((π β π β§ π β β) β (π βπ(π + 1)) = (π β (π βππ))) | ||
Theorem | relexpsucl 14978 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
β’ ((π β π β§ Rel π β§ π β β0) β (π βπ(π + 1)) = (π β (π βππ))) | ||
Theorem | relexpsucr 14979 | A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.) |
β’ ((π β π β§ Rel π β§ π β β0) β (π βπ(π + 1)) = ((π βππ) β π )) | ||
Theorem | relexpsucrd 14980 | A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) β β’ (π β (π βπ(π + 1)) = ((π βππ) β π )) | ||
Theorem | relexpsucld 14981 | A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) β β’ (π β (π βπ(π + 1)) = (π β (π βππ))) | ||
Theorem | relexpcnv 14982 | Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β β‘(π βππ) = (β‘π βππ)) | ||
Theorem | relexpcnvd 14983 | Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β π) & β’ (π β π β β0) β β’ (π β β‘(π βππ) = (β‘π βππ)) | ||
Theorem | relexp0rel 14984 | The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.) |
β’ (π β π β Rel (π βπ0)) | ||
Theorem | relexprelg 14985 | The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π β§ (π = 1 β Rel π )) β Rel (π βππ)) | ||
Theorem | relexprel 14986 | The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π β§ Rel π ) β Rel (π βππ)) | ||
Theorem | relexpreld 14987 | The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) β β’ (π β Rel (π βππ)) | ||
Theorem | relexpnndm 14988 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β β§ π β π) β dom (π βππ) β dom π ) | ||
Theorem | relexpdmg 14989 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β dom (π βππ) β (dom π βͺ ran π )) | ||
Theorem | relexpdm 14990 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β dom (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpdmd 14991 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β β0) β β’ (π β dom (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpnnrn 14992 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β β§ π β π) β ran (π βππ) β ran π ) | ||
Theorem | relexprng 14993 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β ran (π βππ) β (dom π βͺ ran π )) | ||
Theorem | relexprn 14994 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β ran (π βππ) β βͺ βͺ π ) | ||
Theorem | relexprnd 14995 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β β0) β β’ (π β ran (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpfld 14996 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β βͺ βͺ (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpfldd 14997 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β β0) β β’ (π β βͺ βͺ (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpaddnn 14998 | Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β β§ π β β β§ π β π) β ((π βππ) β (π βππ)) = (π βπ(π + π))) | ||
Theorem | relexpuzrel 14999 | The exponentiation of a class to an integer not smaller than 2 is a relation. (Contributed by RP, 23-May-2020.) |
β’ ((π β (β€β₯β2) β§ π β π) β Rel (π βππ)) | ||
Theorem | relexpaddg 15000 | Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020.) |
β’ ((π β β0 β§ (π β β0 β§ π β π β§ ((π + π) = 1 β Rel π ))) β ((π βππ) β (π βππ)) = (π βπ(π + π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |