Simple Order Product of Pair of Ordered Semigroups is Ordered Semigroup

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S_1, \circ_1, \preccurlyeq_1}$ and $\struct {S_2, \circ_2, \preccurlyeq_2}$ be ordered semigroups.


Let $\struct {S_1 \times S_2, \odot} := \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}$ denote the external direct product of $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$.

Let $\struct {S_1 \times S_2, \preccurlyeq_s} := \struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$ denote the simple (order) product of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$.


Then $\struct {S_1 \times S_2, \odot, \preccurlyeq_s}$ is also an ordered semigroup.


Proof

From Simple Order Product of Pair of Ordered Sets is Ordered Set, $\struct {S_1 \times S_2, \otimes^s}$ is an ordered set.

From External Direct Product of Semigroups, $\struct {S_1 \times S_2, \odot}$ is a semigroup.


It remains to be shown that $\preccurlyeq_s$ is compatible with $\odot$.


Let $\tuple {x_1, x_2}, \tuple {y_1, y_2} \in S_1 \times S_2$ be arbitrary such that $\tuple {x_1, x_2} \preccurlyeq_s \tuple {y_1, y_2}$.

\(\ds \tuple {x_1, x_2}\) \(\preccurlyeq_s\) \(\ds \tuple {y_1, y_2}\)
\(\ds \leadsto \ \ \) \(\ds x_1\) \(\preccurlyeq_1\) \(\ds y_1\) Definition of Simple Order Product
\(\, \ds \land \, \) \(\ds x_2\) \(\preccurlyeq_2\) \(\ds y_2\)
\(\ds \leadsto \ \ \) \(\ds \forall \tuple {z_1, z_2} \in S_1 \times S_2: \, \) \(\ds x_1 \circ_1 z_1\) \(\preccurlyeq_1\) \(\ds y_1 \circ_1 z_1\) Definition of Relation Compatible with Operation
\(\, \ds \land \, \) \(\ds x_2 \circ_2 z_2\) \(\preccurlyeq_2\) \(\ds y_2 \circ_2 z_2\)
\(\, \ds \land \, \) \(\ds z_1 \circ_1 x_1\) \(\preccurlyeq_1\) \(\ds z_1 \circ_1 y_1\)
\(\, \ds \land \, \) \(\ds z_2 \circ_2 x_2\) \(\preccurlyeq_2\) \(\ds z_2 \circ_2 y_2\)
\(\ds \leadsto \ \ \) \(\ds \tuple {x_1 \circ_1 z_1, x_2 \circ_2 z_2}\) \(\preccurlyeq_s\) \(\ds \tuple {y_1 \circ_1 z_1, y_2 \circ_2 z_2}\) Definition of Simple Order Product
\(\, \ds \land \, \) \(\ds \tuple {z_1 \circ_1 x_1, z_2 \circ_2 x_2}\) \(\preccurlyeq_s\) \(\ds \tuple {z_1 \circ_1 y_1, z_2 \circ_2 y_2}\)
\(\ds \leadsto \ \ \) \(\ds \tuple {x_1, x_2} \odot \tuple {z_1, z_2}\) \(\preccurlyeq_s\) \(\ds \tuple {y_1, y_2} \odot \tuple {z_1, z_2}\) Definition of External Direct Product
\(\, \ds \land \, \) \(\ds \tuple {z_1, z_2} \odot \tuple {x_1, x_2}\) \(\preccurlyeq_s\) \(\ds \tuple {z_1, z_2} \odot \tuple {y_1, y_2}\)

and the proof is complete.

$\blacksquare$


Sources

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