avewright/proofwiki-math huggingface dataset:
Theorem: Mapping Composed with Bijection forming Bijection is Bijection

Let $A$, $B$ and $C$ be sets.
Let $f: A \to B$ and $g: B \to C$ be mappings.
Let the composite mapping $g \circ f$ be a bijection.
Let either $f$ or $g$ be a bijection.
Then both $f$ and $g$ are bijections.

Proof:
We note that $g \circ f$ is both an injection and a surjection by definition of bijection.
We are given that:
:$g \circ f$ is a bijection.
From Injection if Composite is Injection it follows that $f$ is an injection.
From Surjection if Composite is Surjection it follows that $g$ is a surjection.
{{qed|lemma}}
First suppose that $g$ is a bijection.
We already have that $f$ is an injection.
{{AimForCont}} $f$ is not a surjection.
Then:
:$\exists y \in B: \neg \exists x \in A: \map f x = y$
But then $g$ is a surjection and so:
:$\forall z \in C: \exists y \in B: z = \map g y$
and so:
:$\exists z \in C: \neg \exists x \in A: \map g {\map f x} = z$
and so $g \circ f$ is not a surjection.
This contradicts our assertion that $g \circ f$ is a bijection and so a surjection.
Hence by Proof by Contradiction $f$ must be a surjection
So $f$ is both an injection and a surjection, and so a bijection.
{{qed|lemma}}
Now suppose that $f$ is a bijection.
{{AimForCont}} $g$ is not an injection.
Then:
:$\exists y_1, y_2 \in B: \map g {y_1} = \map g {y_2}$
But then $f$ is a bijection and so:
:$\exists x_1, x_2 \in A: y_1 = \map f {x_1} \ne \map f {x_2} = y_2$
and so:
:$\exists x_1, x_2 \in A: \map g {\map f {x_1} } = \map g {\map f {x_2} }$
and so $g \circ f$ is not an injection.
This contradicts our assertion that $g \circ f$ is a bijection and so an injection.
Hence by Proof by Contradiction $g$ must be an injection.
So $g$ is both an injection and a surjection, and so a bijection.
{{qed|lemma}}
Hence the result.
{{qed}}
Category:Bijections
Category:Composite Mappings
r59vy38dyxt59ge73vn9psa1a8qfaos
Theorem: Composite of Three Mappings in Cycle forming Injections and Surjection

Let $A$, $B$ and $C$ be non-empty sets.
Let $f: A \to B$, $g: B \to C$ and $h: C \to A$ be mappings.
Let the following hold:
:$h \circ g \circ f$ is an injection
:$f \circ h \circ g$ is an injection
:$g \circ f \circ h$ is a surjection.
where:
:$g \circ f$ (and so on) denote composition of mappings.
Then each of $f$, $g$ and $h$ are bijections.

Proof:
First note that from Composition of Mappings is Associative:
:$\paren {h \circ g} \circ f = h \circ \paren {g \circ f}$
and so on.
However, while there is no need to use parenthesis to establish the order of composition of mappings, in the following the technique will be used in order to clarify what is being done.
We have that $\paren {h \circ g} \circ f$ and $\paren {f \circ h} \circ g$ are injections.
From Injection if Composite is Injection it follows that:
:$f$ is an injection
:$g$ is an injection.
Similarly, because $h \circ \paren {g \circ f}$ and $f \circ \paren {h \circ g}$ are injections:
:$g \circ f$ is an injection
:$h \circ g$ is an injection.
We have that $g \circ \paren {f \circ h}$ is a surjection.
From Surjection if Composite is Surjection it follows that $g$ is a surjection.
Similarly, because $\paren {g \circ f} \circ h$ is a surjection:
:$g \circ f$ is a surjection.
Thus we have deduced that:
:$g$ is a bijection
and:
:$g \circ f$ is a bijection.
From Mapping Composed with Bijection forming Bijection is Bijection it follows that:
:$f$ is a bijection.
Thus from Inverse of Bijection is Bijection we have that $f^{-1}: B \to A$ and $g^{-1}: C \to B$ are both bijections.
Similarly, $\paren {g \circ f}^{-1}: C \to A$ is a bijection, which from Inverse of Composite Bijection is the same as $f^{-1} \circ g^{-1}$.
{{finish|Can we now prove that $\paren {g \circ f}^{-1} {{=}} h?$}}
Theorem: Component Mappings of Set Coproduct are Injective

Let $S_1$ and $S_2$ be sets.
Let $\struct {C, i_1, i_2}$ be a coproduct of $S_1$ and $S_2$.
Then $i_1$ and $i_2$ are injections.

Proof:
By definition of coproduct:
:for all sets $X$ and mappings $f_1: S_1 \to X$ and $f_1: S_1 \to X$
::there exists a unique mapping $h: C \to X$ such that:
:::$h \circ i_1 = f_1$
:::$h \circ i_2 = f_2$
Let $X := S_1$ and $f_1: S_1 \to X = I_{S_1}$ where $I_{S_1}$ denotes the identity mapping.
We have:
:$h \circ i_1 = I_{S_1}$
From Identity Mapping is Injection, $I_{S_1}$ is an injection.
From Injection if Composite is Injection it follows that $i_1$ is an injection.
By setting $X := S_2$ and $f_2 := I_{S_2}$ it follows in the same way that $i_2$ is also an injection.
Hence the result.
{{qed}}
Theorem: Coproduct on Disjoint Union

Let $S_1$ and $S_2$ be sets.
Let $S_1 \sqcup S_2 := \paren {S_1 \times \set 1} \cup \paren {S_2 \times \set 2}$ be the disjoint union of $S_1$ and $S_2$.
Let $i_1: S_1 \to S_1 \sqcup S_2$ and $i_2: S_2 \to S_1 \sqcup S_2$ be the mappings defined as:
:$\forall s_1 \in S_1: \map {i_1} {s_1} = \tuple {s_1, 1}$
:$\forall s_2 \in S_2: \map {i_2} {s_2} = \tuple {s_2, 2}$
Then $\struct {S_1 \sqcup S_2, i_1, i_2}$ is a coproduct of $S_1$ and $S_2$.

Proof:
For $\struct {S_1 \sqcup S_2, i_1, i_2}$ to be a coproduct, it is necessary that:
:for all sets $X$ and all mappings $f_1: S_1 \to X$ and $f_2: S_2 \to X$
::there exists a unique mapping $h: S_1 \sqcup S_2 \to X$ such that:
:::$h \circ i_1 = f_1$
:::$h \circ i_2 = f_2$
Let $h$ be the mapping defined as:
:$\forall \tuple {s, t} \in S_1 \sqcup S_2: \map h {s, t} = \begin {cases} \map {f_1} s & : t = 1 \\ \map {f_2} s & : t = 2 \end {cases}$
Then:
{{begin-eqn}}
{{eqn | l = \map {h \circ i_1} {s_1}
      | r = \map h {s_1, 1}
      | c = 
}}
{{eqn | r = \map {f_1} {s_1}
      | c = 
}}
{{eqn-intertext|and:}}
{{eqn | l = \map {h \circ i_2} {s_2}
      | r = \map h {s_2, 2}
      | c = 
}}
{{eqn | r = \map {f_2} {s_2}
      | c = 
}}
{{end-eqn}}
The existence of $h$ is apparent.
It remains to prove that $h$ is unique.
Let $h_1: S_1 \sqcup S_2 \to X$ and $h_2: S_1 \sqcup S_2 \to X$ both be mappings with the properties of $h$.
Let $\tuple {s, t} \in S_1 \sqcup S_2$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map {h_1 \circ i_1} {s_1}
      | r = \map {f_1} {s_1}
      | c = 
}}
{{eqn | r = \map {h_2 \circ i_1} {s_1}
      | c = as $h_1$ and $h_2$ have the same properties
}}
{{eqn | ll= \leadsto
      | l = \map {h_1} {s_1, 1}
      | r = \map {h_2} {s_1, 1}
      | c = for all $s_1 \in S_1$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {h_1 \circ i_2} {s_2}
      | r = \map {f_2} {s_2}
      | c = 
}}
{{eqn | r = \map {h_2 \circ i_2} {s_2}
      | c = as $h_1$ and $h_2$ have the same properties
}}
{{eqn | ll= \leadsto
      | l = \map {h_2} {s_2, 2}
      | r = \map {h_2} {s_2, 2}
      | c = for all $s_2 \in S_2$
}}
{{end-eqn}}
Hence $h_1 = h_2$ and so $h$ is unique
Hence $\struct {S_1 \sqcup S_2, i_1, i_2}$ is a coproduct of $S_1$ and $S_2$.
{{qed}}
Theorem: Existence of Bijection between Coproducts of two Sets

Let $S_1$ and $S_2$ be sets.
Let $\struct {C, i_1, i_2}$ and $\struct {D, j_1, j_2}$ be two coproducts on $S_1$ and $S_2$.
Then there exists a unique bijection $\theta: D \to C$ such that:
:$\theta \circ j_i = i_1$
:$\theta \circ j_2 = i_2$

Proof:
Let $X$ be an arbitrary set.
Let $f_1: S_1 \to X$ and $f_2: S_2 \to X$ be arbitrary mappings.
Let $h_C: C \to X$ be the unique mapping such that:
:$h_C \circ i_1 = f_1$
:$h_C \circ i_2 = f_2$
Let $h_D: D \to X$ be the unique mapping such that:
:$h_D \circ j_1 = f_1$
:$h_D \circ j_2 = f_2$
The existence and uniqueness of $h_C$ and $h_D$ follow from the fact of $\struct {C, i_1, i_2}$ and $\struct {D, j_1, j_2}$ both being coproducts of $S_1$ and $S_2$.
We have that:
:$h_C \circ i_1 = f_1 = h_D \circ j_1$
:$h_C \circ i_2 = f_2 = h_D \circ j_2$
{{ProofWanted}}
Theorem: Number of Friday 13ths in a Year

In any given year, there are between $1$ and $3$ (inclusive) months in which the $13$th falls on a Friday.

Proof:
The day of the week on which the $13$th falls is directly dependent upon the day of the week that the $1$st of the month falls.
From Months that Start on the Same Day of the Week, the months can be grouped into equivalence classes according to which day of the week the month starts:
For a non-leap year, the set of equivalence classes is:
:$\set {\set {\text {January}, \text {October} }, \set {\text {February}, \text {March}, \text {November} }, \set {\text {April}, \text {July} }, \set {\text {May} }, \set {\text {June} }, \set {\text {August} }, \set {\text {September}, \text {December} } }$
For a leap year, the set of equivalence classes is:
:$\set {\set {\text {January}, \text {April}, \text {July} }, \set {\text {February}, \text {August} }, \set {\text {March}, \text {November} }, \set {\text {May} }, \set {\text {June} }, \set {\text {September}, \text {December} }, \set {\text {October} } }$
It can be seen that none of these equivalence classes has fewer than $1$ day, and none has more than $3$.
Hence the result.
{{qed}}
Theorem: Equivalence Relation on Natural Numbers such that Quotient is Power of Two/Equivalence Class Contains 1 Odd Number

Let $\eqclass n \alpha$ be the $\alpha$-equivalence class of a natural number $n$.
Then $\eqclass n \alpha$ contains exactly $1$ odd number.

Proof:
That $\alpha$ is an equivalence relation is proved in Equivalence Relation on Natural Numbers such that Quotient is Power of Two.
Let $x$ be a natural number whose $\alpha$-equivalence class is $\eqclass x \alpha$.
If $x$ is odd, then $\eqclass x \alpha$ contains that odd number $x$
We have that $x$ is of the form $x = 2^r y$ for some $r \in \Z$ where $y$ is an odd number.
Thus by definition $y \in \eqclass x \alpha$ is an odd number which is contained in $\eqclass x \alpha$.
Thus it has been shown that an arbitrary $\eqclass x \alpha$ contains at least one odd number.
It remains to be demonstrated that $\eqclass x \alpha$ contains no more than $1$ odd number.
{{AimForCont}} $\eqclass n \alpha$ contains the odd numbers $p$ and $q$ such that $p \ne q$.
Then:
:$p = 2^n q$
for some $n \in \Z$
If $n = 0$ then $p = q$ which contradicts $q \ne p$.
Thus $n \ne 0$.
Let $n > 0$.
Then:
:$p = r q$
for $r \in \Z$ such that $r = 2^n$.
Thus $p$ is has $2$ as a divisor.
This contradicts the supposition that $p$ is odd.
Let $n < 0$.
Then:
:$p = \dfrac q {2^m}$
where $m = -n$ and so $m > 0$.
Thus:
:$q = r p$
for $r \in \Z$ such that $r = 2^m$.
Thus $q$ has $2$ as a divisor.
This contradicts the supposition that $q$ is odd.
Thus all cases of $n$ lead to a contradiction.
It follows that no $\alpha$-equivalence class can contain more than one odd number.
{{qed}}
Theorem: Equivalence Relation on Natural Numbers such that Quotient is Power of Two/One of Pair of Equivalent Elements is Divisor of the Other

Let $c, d \in \N$ such that $c \mathrel \alpha d$.
Then either:
:$c \divides d$
or:
:$d \divides c$
where $\divides$ denotes divisibility.

Proof:
That $\alpha$ is an equivalence relation is proved in Equivalence Relation on Natural Numbers such that Quotient is Power of Two.
We are given that $c \mathrel \alpha d$.
{{WLOG}}, suppose $c < d$.
If $d < c$ then the same argument holds, {{mutatis}}.
By definition of $\alpha$, we have that:
:$c = 2^n d$
for some $n \in \Z$.
As $c < d$ it follows that $2^n > 1$.
That is, $n > 0$ and so $2^n \in \Z$.
So by definition $c$ is a divisor of $d$.
The result follows.
{{qed}}
Theorem: Exists Divisor in Set of n+1 Natural Numbers no greater than 2n

Let $S$ be a set of $n + 1$ non-non-zero natural numbers all less than or equal to $2 n$.
Then there exists $a, b \in S$ such that
:$a \divides b$
where $\divides$ denotes divisibility.

Proof:
Let $\alpha$ denote the relation defined on the natural numbers $\N$ by:
:$\forall x, y \in \N: x \mathrel \alpha y \iff \exists n \in \Z: x = 2^n y$
From Equivalence Relation on Natural Numbers such that Quotient is Power of Two, $\alpha$ is an equivalence relation.
From Equivalence Class under $\alpha$ Contains $1$ Odd Number, each odd integer between $1$ and $2 n$ is in its own equivalence class.
Each even integer $m$ between $1$ and $2 n$ is equal to an odd integer $p$ strictly less than $m$ multiplied by a power of $2$.
Hence each such $m$ is an element of one of the equivalence classes of one of the $n$ odd integers between $1$ and $2 n$.
Thus each element of $S$ is an element of one of exactly $n$ equivalence classes of $\alpha$.
But there are $n + 1$ elements of $S$.
So by the Pigeonhole Principle, at least $2$ elements of $S$ are in the same equivalence class.
Thus let $a, b \in S: a \mathrel \alpha b$.
From One of Pair of Equivalent Elements is Divisor of the Other, either $a \divides b$ or $b \divides a$.
Hence the result.
{{qed}}
Theorem: Equality of Squares Modulo Integer is Equivalence Relation

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $\RR_n$ be the relation on the set of integers $\Z$ defined as:
:$\forall x, y \in \Z: x \mathrel {\RR_n} y \iff x^2 \equiv y^2 \pmod n$
Then $\RR_n$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Left Ideal is Left Module over Ring

Let $\struct {R, +, \times}$ be a ring.
Let $J \subseteq R$ be a left ideal of $R$.
Let $\circ : R \times J \to J$ be the restriction of $\times$ to $R \times J$.
Then $\struct {J, +, \circ}$ is a left module over $\struct {R, +, \times}$.

Proof:
By definition of a left ideal then $\circ$ is well-defined.
Theorem: Right Ideal is Right Module over Ring

Let $\struct {R, +, \times}$ be a ring.
Let $J \subseteq R$ be a right ideal of $R$.
Let $\circ : J \times R \to J$ be the restriction of $\times$ to $J \times R$.
Then $\struct {J, +, \circ}$ is a right module over $\struct {R, +, \times}$.

Proof:
By definition of a right ideal then $\circ$ is well-defined.
Theorem: Opposite Ring is Ring

Let $\struct {R, +, \times}$ be a ring.
Let $\struct {R, +, *}$ be the opposite ring of $\struct {R, +, \times}$.
Then $\struct {R, +, *}$ is a ring.

Proof:
By definition of the opposite ring:
:$\forall x, y \in R: x * y = y \times x$.
By definition of the ring $R$, $\struct {R, +}$ is an abelian group.
To complete the proof, it remains to be shown that $\struct {R, *}$ is a semigroup.
That is, it remains to show that $\struct{R, *}$ is associative.
Let $a, b, c \in R$.
{{begin-eqn}}
{{eqn | l = a * \paren {b * c}
      | r = \paren{b * c} \times a
      | c = Definition of $*$
}}
{{eqn | r = \paren {c \times b} \times a
      | c = Definition of $*$
}}
{{eqn | r = c \times \paren {b \times a}
      | c = {{Ring-axiom|M1}}
}}
{{eqn | r = c \times \paren {a * b}
      | c = Definition of $*$
}}
{{eqn | r = \paren {a * b} * c
      | c = Definition of $*$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Opposite Ring of Opposite Ring

Let $\struct {R, +, \times}$ be a ring.
Let $\struct {R, +, *}$ be the opposite ring of $\struct {R, +, \times}$.
Let $\struct {R, +, \circ}$ be the opposite ring of $\struct {R, +, *}$.
Then $\struct {R, +, \circ} = \struct {R, +, \times}$.

Proof:
By definition of the opposite ring:
:$\forall x, y \in S: x * y = y \times x$
:$\forall x, y \in S: x \circ y = y * x$
Hence for all $x,y \in S$:
:$x \circ y = y * x = x \times y$
The result follows.
{{qed}}
Category:Ring Theory
k14myncy6bkp8xbic8ndvx15pkuigex
Theorem: Left Module over Ring Induces Right Module over Opposite Ring

Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {R, +_R, *_R}$ be the opposite ring of $\struct {R, +_R, \times_R}$.
Let $\struct{G, +_G, \circ}$ be a left module over $\struct {R, +_R, \times_R}$.
Let $\circ' : G \times R \to G$ be the binary operation defined by:
:$\forall \lambda \in R: \forall x \in G: x \circ’ \lambda = \lambda \circ x$
Then $\struct{G, +_G, \circ'}$ is a right module over $\struct {R, +_R, *_R}$.

Proof:
It is shown that $\struct{G, +_G, \circ'}$ satisfies the right module axioms.
By definition of the opposite ring:
:$\forall x, y \in R: x *_R y = y \times_R x$
Theorem: Right Module over Ring Induces Left Module over Opposite Ring

Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {R, +_R, *_R}$ be the opposite ring of $\struct {R, +_R, \times_R}$.
Let $\struct{G, +_G, \circ}$ be a right module over $\struct {R, +_R, \times_R}$.
Let $\circ' : R \times G \to G$ be the binary operation defined by:
:$\forall \lambda \in R: \forall x \in G: \lambda \circ' x = x \circ \lambda$
Then $\struct {G, +_G, \circ'}$ is a left module over $\struct {R, +_R, *_R}$.

Proof:
It is shown that $\struct {G, +_G, \circ'}$ satisfies the left module axioms.
By definition of the opposite ring:
:$\forall x, y \in S: x *_R y = y \times_R x$.
Theorem: Ring is Commutative iff Opposite Ring is Itself

Let $\struct {R, +, \times}$ be a ring.
Let $\struct {R, +, *}$ be the opposite ring of $\struct {R, +, \times}$.
Then $\struct {R, +, \times}$ is a commutative ring {{iff}}:
:$\struct {R, +, \times} = \struct {R, +, *}$

Proof:
By definition of the opposite ring:
:$\forall x, y \in R: x * y = y \times x$
Theorem: Ceva's Theorem

Let $\triangle ABC$ be a triangle.
Let $L$, $M$ and $N$ be points on the sides $BC$, $AC$ and $AB$ respectively.
Then the lines $AL$, $BM$ and $CN$ are concurrent {{iff}}:
:$\dfrac {BL} {LC} \times \dfrac {CM} {MA} \times \dfrac {AN} {NB} = 1$

Proof:
:400px
=== Necessary Condition ===
Let $AL$, $BM$ and $CN$ be concurrent.
Let the point of concurrency be $P$.
Consider the triangles $\triangle ALB$ and $\triangle ALC$.
They have the same altitude from the common base $BC$.
Hence:
:$\dfrac {\map \Area {ALB} } {\map \Area {ALC} } = \dfrac {BL} {LC}$
Similarly, consider the triangles $\triangle PLB$ and $\triangle PLC$.
They also have the same altitude from the common base $BC$.
Hence:
:$\dfrac {\map \Area {PLB} } {\map \Area {PLC} } = \dfrac {BL} {LC}$
Next we consider the triangles $\triangle APB$ and $\triangle APC$.
We have:
:$\map \Area {APB} = \map \Area {ALB} - \map \Area {PLB}$
and:
:$\map \Area {APC} = \map \Area {ALC} - \map \Area {PLC}$
and so:
:$\dfrac {\map \Area {APB} } {\map \Area {APC} } = \dfrac {BL} {LC}$
In the same way, we derive:
:$\dfrac {\map \Area {BPC} } {\map \Area {APB} } = \dfrac {CM} {MA}$
and:
:$\dfrac {\map \Area {APC} } {\map \Area {BPC} } = \dfrac {AN} {NB}$
Thus we have:
:$\dfrac {\map \Area {APB} } {\map \Area {APC} } \times \dfrac {\map \Area {BPC} } {\map \Area {APB} } \times \dfrac {\map \Area {APC} } {\map \Area {BPC} } = \dfrac {BL} {LC} \times \dfrac {CM} {MA} \times \dfrac {AN} {NB}$
The areas on the {{LHS}} cancel out, leaving us with:
:$\dfrac {BL} {LC} \times \dfrac {CM} {MA} \times \dfrac {AN} {NB} = 1$
{{qed|lemma}}
=== Sufficient Condition ===
Let:
:$\dfrac {BL} {LC} \times \dfrac {CM} {MA} \times \dfrac {AN} {NB} = 1$
Let $P$ be the intersection of $AM$ and $CN$ as in the diagram above.
We need to show that $A$, $P$ and $L$ are collinear.
From the first part, we have that:
:$\dfrac {\map \Area {BPC} } {\map \Area {APB} } = \dfrac {CM} {MA}$
and:
:$\dfrac {\map \Area {APC} } {\map \Area {BPC} } = \dfrac {AN} {NB}$
Multiplying them:
:$\dfrac {\map \Area {BPC} } {\map \Area {APB} } \times \dfrac {\map \Area {APC} } {\map \Area {BPC} } = \dfrac {CM} {MA} \times \dfrac {AN} {NB}$
Simplifying:
:$\dfrac {\map \Area {APC} } {\map \Area {APB} } = \dfrac {CM} {MA} \times \dfrac {AN} {NB}$
It is given that:
:$\dfrac {BL} {LC} \times \dfrac {CM} {MA} \times \dfrac {AN} {NB} = 1$
and so:
:$\dfrac {CM} {MA} \times \dfrac {AN} {NB} = \dfrac {LC} {BL} = \dfrac {\map \Area {APC} } {\map \Area {APB} }$
Extend $BP$ to meet $AC$ at point $Z$, say.
By the same construction that we have used throughout, we have:
:$\dfrac {\map \Area {APC} } {\map \Area {APB} } = \dfrac {ZC} {BZ}$
But then we have just shown that:
:$\dfrac {LC} {BL} = \dfrac {\map \Area {APC} } {\map \Area {APB} }$
So $Z$ coincides with $L$ and the result follows.
{{qed}}
Theorem: Ceva's Theorem

Let $\triangle ABC$ be a triangle.
Let $L$, $M$ and $N$ be points on the sides $BC$, $AC$ and $AB$ respectively.
Then the lines $AL$, $BM$ and $CN$ are concurrent {{iff}}:
:$\dfrac {BL} {LC} \times \dfrac {CM} {MA} \times \dfrac {AN} {NB} = 1$

Proof:
=== Necessary Condition ===
We have {{hypothesis}}:
:$AL$, $BM$ and $CN$ are concurrent in $\triangle ABC$ at point $P$.
:400px
Following the sides anticlockwise in $\triangle LAB$:
{{begin-eqn}}
{{eqn | n = 1
      | l = \dfrac {LP} {PA} \cdot \dfrac {AN} {NB} \cdot \dfrac {BC} {CL}
      | r = -1
      | c = Menelaus's Theorem
}}
{{end-eqn}}
Following the sides clockwise in $\triangle LAC$:
{{begin-eqn}}
{{eqn | n = 2
      | l = \dfrac {LP} {PA} \cdot \dfrac {AM} {MC} \cdot \dfrac {CB} {BL}
      | r = -1
      | c = Menelaus's Theorem
}}
{{end-eqn}}
Equate $(1)$ and $(2)$ and cancel $\dfrac {LP} {PA}$.
{{begin-eqn}}
{{eqn | l = \dfrac {AN} {NB} \cdot \dfrac {BC} {CL} 
      | r = \dfrac {AM} {MC} \cdot \dfrac {CB} {BL}
      | c = 
}}
{{end-eqn}}
By definition of directed line segments:
* $AM = -MA$
* $MC = -CM$
* $CL = -LC$
* $CB = -BC$
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {AN} {NB} \cdot \dfrac {BC} {-LC} 
      | r = \dfrac {-MA} {-CM} \cdot \dfrac {-BC} {BL}
      | c = substituting
}}
{{eqn | l = \dfrac {AN} {NB} \cdot \dfrac {BC} {LC} 
      | r = \dfrac {MA} {CM} \cdot \dfrac {BC} {BL}
      | c = cancel $-1$ twice
}}
{{eqn | l = \dfrac {CM} {MA} \cdot \dfrac {AN} {NB} \cdot \dfrac {BL} {LC}
      | r = 1
      | c = cancel $BC$ and rearrange
}}
{{end-eqn}}
The result follows.
{{qed|lemma}}
=== Sufficient Condition ===
Given:
{{begin-eqn}}
{{eqn | l = \dfrac {CM} {MA} \cdot \dfrac {AN} {NB} \cdot \dfrac {BL} {LC}
      | r = 1
      | c = {{hypothesis}}
}}
{{end-eqn}}
{{WLOG}}, let $BM$ and $CN$ be concurrent at $P$.
Suppose $AL$ does not go through point $P$.
Then let $AP$ produced to $BC$ to give $AL'$, where $L'$ is not the same point as $L$.
By the '''Necessary Condition''':
{{begin-eqn}}
{{eqn | l = \dfrac {CM} {MA} \cdot \dfrac {AN} {NB} \cdot \dfrac {BL'} {L'C}
      | r = 1
      | c = 
}}
{{end-eqn}}
Equating the two results:
{{begin-eqn}}
{{eqn | l = \dfrac {CM} {MA} \cdot \dfrac {AN} {NB} \cdot \dfrac {BL'} {L'C}
      | r = \dfrac {CM} {MA} \cdot \dfrac {AN} {NB} \cdot \dfrac {BL} {LC}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \dfrac {BL'} {L'C}
      | r = \dfrac {BL} {LC}
      | c = cancelling
}}
{{eqn | l = \dfrac {BL'} {L'C} + \dfrac {L'C} {L'C}
      | r = \dfrac {BL} {LC} + \dfrac {LC} {LC}
      | c = add $1$ to both sides
}}
{{eqn | l = \dfrac {BC} {L'C}
      | r = \dfrac {BC} {LC}
      | c = addition
}}
{{eqn | l = LC
      | r = L'C
      | c = cancel $BC$ and rearrange
}}
{{end-eqn}}
Hence $L'$ is the same point as $L$.
This is a contradiction.
$AL$, $BM$ and $CN$ are concurrent at $P$.
The result follows.
{{qed}}
Theorem: Left Module induces Right Module over same Ring iff Actions are Commutative

Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {G, +_G, \circ}$ be a left module over $\struct {R, +_R, \times_R}$.
Let $\circ': G \times R \to G$ be the binary operation defined by:
:$\forall \lambda \in R: \forall x \in G: x \circ' \lambda = \lambda \circ x$
Then $\struct {G, +_G, \circ'}$ is a right module over $\struct {R, +_R, \times_R}$ {{iff}}:
:$\forall \lambda, \mu \in R: \forall x \in G: \paren {\lambda \times_R \mu} \circ x = \paren {\mu \times_R \lambda} \circ x$

Proof:
=== Necessary Condition ===
Let $\struct {G, +_G, \circ'}$ be a right module over $\struct {R, +_R, \times_R}$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {\lambda \times_R \mu} \circ x
      | r = x \circ' \paren {\lambda \times_R \mu}
      | c = Definition of $\circ'$
}}
{{eqn | r = \paren {x \circ' \lambda} \circ' \mu
      | c = {{Right-module-axiom|3}}
}}
{{eqn | r = \mu \circ \paren {\lambda \circ x} 
      | c = Definition of $\circ'$
}}
{{eqn | r = \paren {\mu \times_R \lambda} \circ x
      | c = {{Left-module-axiom|3}}
}}
{{end-eqn}}
{{qed|lemma}}