Structure Induced by Left Distributive Operation is Left Distributive

This article needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code. 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 {{Proofread}} from the code.

Theorem

Let $\struct {T, +, \times}$ be an algebraic structure, and let $S$ be a set.

Let $\struct {T^S, \oplus, \otimes}$ be the structure on $T^S$ induced by $+$ and $\times$.

Let $\times$ be left distributive over $+$:

$\forall a, b, c \in S: a \times \paren {b + c} = \paren{a \times b} + \paren{a \times c}$

Then the pointwise operation $\otimes$ is left distributive over the pointwise operation $\oplus$ on $T^S$:

$\forall f, g, h \in T^S: f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$

Proof

Let $f, g, h \in T^S$.

Then:

\(\ds \forall x \in S: \, \)

\(\ds \map {\paren{f \otimes \paren {g \oplus h} } } x\)

\(=\)

\(\ds \map f x \times \map {\paren{g \otimes h} } x\)

Definition of Pointwise Operation

\(\ds \)

\(=\)

\(\ds \map f x \times \paren{ \map g x + \map h x}\)

Definition of Pointwise Operation

\(\ds \)

\(=\)

\(\ds \paren{\map f x \times \map g x} + \paren{\map f x \times \map h x}\)

Definition of Left Distributive Operation

\(\ds \)

\(=\)

\(\ds \map {\paren{f \otimes g} } x + \map {\paren{f \otimes h} } x\)

Definition of Pointwise Operation

\(\ds \)

\(=\)

\(\ds \map {\paren{\paren{f \otimes g} \oplus \paren{f \otimes h} } } x\)

Definition of Pointwise Operation

From Equality of Mappings:

$f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$

Since $f, g, h$ were arbitrary:

$\forall f, g, h \in T^S: f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$

Hence $\otimes$ is left distributive over $\oplus$ by definition.

$\blacksquare$