Composition of Relations is Associative

From ProofWiki
Jump to navigation Jump to search

Theorem

The composition of relations is an associative binary operation:

$\paren {\RR_3 \circ \RR_2} \circ \RR_1 = \RR_3 \circ \paren {\RR_2 \circ \RR_1}$


Proof


This has to be rewritten.
In particular: Needs to be rewritten in light of the actual definition of the composition of relations and domain of relations. These equalities may not hold for all relations
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by doing so.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Rewrite}} from the code.


First, note that from the definition of composition of relations, the following must be the case before the above expression is even to be defined:

$\Dom {\RR_2} = \Cdm {\RR_1}$
$\Dom {\RR_3} = \Cdm {\RR_2}$


The two composite relations can be seen to have the same domain, thus:

\(\ds \Dom {\paren {\RR_3 \circ \RR_2} \circ \RR_1}\) \(=\) \(\ds \Dom {\RR_1}\) Domain of Composite Relation


\(\ds \Dom {\RR_3 \circ \paren {\RR_2 \circ \RR_1} }\) \(=\) \(\ds \Dom {\RR_2 \circ \RR_1}\) Domain of Composite Relation
\(\ds \) \(=\) \(\ds \Dom {\RR_1}\) Domain of Composite Relation


and also the same codomain, thus:

\(\ds \Cdm {\paren {\RR_3 \circ \RR_2} \circ \RR_1}\) \(=\) \(\ds \Cdm {\RR_3 \circ \RR_2}\) Codomain of Composite Relation
\(\ds \) \(=\) \(\ds \Cdm {\RR_3}\) Codomain of Composite Relation


\(\ds \Cdm {\RR_3 \circ \paren {\RR_2 \circ \RR_1} }\) \(=\) \(\ds \Cdm {\RR_3}\) Codomain of Composite Relation


This page has been identified as a candidate for refactoring.
In particular: Put this statement into a theorem page
Until this has been finished, please leave {{Refactor}} in the code.

New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.

Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Refactor}} from the code.


So they are equal if and only if they have the same value at each point in their common domain, which this shows:


This has to be rewritten.
In particular: These terms may not be defined for all relations. So a different approach is required
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by doing so.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Rewrite}} from the code.


\(\ds \forall x \in \Dom {\RR_1}: \, \) \(\ds \map {\paren {\paren {\RR_3 \circ \RR_2} \circ \RR_1} } x\) \(=\) \(\ds \map {\paren {\RR_3 \circ \RR_2} } {\map {\RR_1} x}\) Definition of Composition of Relations
\(\ds \) \(=\) \(\ds \map {\RR_3} {\map {\RR_2} {\map {\RR_1} x} }\) Definition of Composition of Relations
\(\ds \) \(=\) \(\ds \map {\RR_3} {\map {\paren {\RR_2 \circ \RR_1} } x}\) Definition of Composition of Relations
\(\ds \) \(=\) \(\ds \map {\paren {\RR_3 \circ \paren {\RR_2 \circ \RR_1} } } x\) Definition of Composition of Relations

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Composition_of_Relations_is_Associative&oldid=742979"