Quotient Structure is Well-Defined

From ProofWiki
Jump to navigation Jump to search


Let $\struct {S, \circ}$ be an algebraic structure.

Let $\RR$ be a congruence relation on $\struct {S, \circ}$.

Let $S / \RR$ be the quotient set of $S$ by $\RR$.

Let $\circ_\RR$ be the operation induced on $S / \RR$ by $\circ$.

Then $\circ_\RR$ is a well-defined operation in the quotient structure $\struct {S / \RR, \circ_\RR}$.


\(\ds \eqclass {x_1} \RR = \eqclass {x_2} \RR\) \(\land\) \(\ds \eqclass {y_1} \RR = \eqclass {y_2} \RR\)
\(\ds \leadsto \ \ \) \(\ds x_1 \mathop \RR x_2\) \(\land\) \(\ds y_1 \mathop \RR y_2\) Definition of Equivalence Class
\(\ds \leadsto \ \ \) \(\ds \paren {x_1 \circ y_1}\) \(\RR\) \(\ds \paren {x_2 \circ y_2}\) Definition of Congruence Relation
\(\ds \leadsto \ \ \) \(\ds \eqclass {x_1 \circ y_1} \RR\) \(=\) \(\ds \eqclass {x_2 \circ y_2} \RR\) Definition of Equivalence Class