Image of Composite Relation

Theorem

Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be relations.

Let $\RR_2 \circ \RR_1 \subseteq S_1 \times T_2$ be the composition of $\RR_1$ and $\RR_2$.

Then the image of $\RR_2 \circ \RR_1$ is given by:

$\Img {\RR_2 \circ \RR_1} = \Img {\Img {\RR_1} \cap \Preimg {\RR_2} }$

Proof

We have by definition of composition of $\RR_1$ and $\RR_2$:

$\RR_2 \circ \RR_1 := \set {\tuple {x, z} \in S_1 \times T_2: \exists y \in S_2 \cap T_1: \tuple {x, y} \in \RR_1 \land \tuple {y, z} \in \RR_2}$

Let $\left({x, z}\right) \in \RR_2 \circ \RR_1$.

By definition of image:

$z \in \Img {\RR_2 \circ \RR_1}$

By definition of composition of $\RR_1$ and $\RR_2$:

$z \in \Img {\RR_2}$

But also:

$z \in \Img {\Img {\RR_1} }$

We also have that $\Img {\RR_2} = \Img {\Preimg {\RR_2} }$

That is: $z \in \Img {\Img {\RR_1} } \cap \Img {\Preimg {\RR_2} }$

This needs considerable tedious hard slog to complete it. In particular: Not convinced this is going to work. 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 {{Finish}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.