avewright/proofwiki-math huggingface dataset:
Theorem: Vector Space with Standard Affine Structure is Affine Space

Let $E$ be a vector space.
Let $\struct {\EE, E, +, -}$ be the standard affine structure on $E$.
Then with this structure, $\EE$ is an affine space.

Proof:
We are required to show that:
{{begin-axiom}}
{{axiom|n = 1
       |q = \forall p, q \in \EE
       |m = p + \paren {q - p} = q
}}
{{axiom|n = 2
       |q = \forall p \in \EE: \forall u, v \in E
       |m = \paren {p + u} + v = p + \paren {u + v}
}}
{{axiom|n = 3
       |q = \forall p, q \in \EE: \forall u \in E
       |m = \paren {p - q} + u = \paren {p + u} - q
}}
{{end-axiom}}
By definition of the standard affine structure, the addition and subtraction operations are simply those in the vector space $E$.
That is, we want to show that:
{{begin-axiom}}
{{axiom|n = 1
       |q = \forall u, v \in E
       |m = u + \paren {v - u} = v
}}
{{axiom|n = 2
       |q = \forall u, v, w \in E
       |m = \paren {u + v} + w = u + \paren {v + w}
}}
{{axiom|n = 3
       |q = \forall u, v, w \in E
       |m = \paren {v - u} + w = \paren {v + w} - u
}}
{{end-axiom}}
By definition the addition operation on a vector space is commutative and associative.
But all three axioms are immediate consequences of commutativity and associativity.
This concludes the proof.
{{Qed}}
{{MissingLinks|particularly to addition, subtraction etc.}}
Category:Affine Geometry
heb42zjfnflyazpdjp0z0kxrx8rky2p
Theorem: Reflexive Reduction of Ordering is Strict Ordering

Let $\RR$ be an ordering on a set $S$.
Let $\RR^\ne$ be the reflexive reduction of $\RR$.
Then $\RR^\ne$ is a strict ordering on $S$.

Proof:
=== Antireflexivity ===
Follows from Reflexive Reduction is Antireflexive.
{{qed|lemma}}
=== Transitivity ===
Suppose $\tuple {x, y}, \tuple {y, z} \in \RR^\ne$.
By antireflexivity $x \ne y$ and $y \ne z$.
We consider the two remaining cases.
==== Case 1: $x = z$ ====
If $x = z$ then:
:$\tuple {x, y}, \tuple {y, x} \in \RR^\ne$
and so:
:$\tuple {x, y}, \tuple {y, x} \in \RR$
Then by the antisymmetry of $\RR$:
:$x = y$
and:
:$\tuple {x, x} \in \RR^\ne$
which contradicts that $\RR^\ne$ is antireflexive.
==== Case 2: $x \ne z$ ====
By the transitivity of $\RR$:
:$\tuple {x, z} \in \RR$
and by $x$ and $z$ being distinct:
:$\tuple {x, z} \notin \Delta_S$
It follows by the definition of reflexive reduction:
:$\tuple {x, z} \in \RR^\ne$
Hence $\RR^\ne$ is transitive.
{{qed}}
Theorem: Reflexive Reduction of Ordering is Strict Ordering

Let $\RR$ be an ordering on a set $S$.
Let $\RR^\ne$ be the reflexive reduction of $\RR$.
Then $\RR^\ne$ is a strict ordering on $S$.

Proof:
By definition, an ordering is both antisymmetric and transitive.
The result then follows from Reflexive Reduction of Transitive Antisymmetric Relation is Strict Ordering.
{{qed}}
Theorem: Vectorialization of Affine Space is Vector Space

Let $\EE$ be an affine space over a field $K$ with difference space $E$.
Let $\RR = \tuple {p_0, e_1, \ldots, e_n}$ be an affine frame in $\EE$.
Let $\struct {\EE, +, \cdot}$ be the vectorialization of $\EE$.
Then $\struct {\EE, +, \cdot}$ is a vector space.

Proof:
By the definition of the vectorialization of an affine space, the mapping $\Theta_\RR : K^n \to \EE$ defined by:
:$\ds \map {\Theta_\RR} {\lambda_1, \ldots, \lambda_n} = p_0 + \sum_{i \mathop = 1}^n \lambda_i e_i$
is a bijection from $K^n$ to $\EE$.
Therefore, by Homomorphic Image of Vector Space, it suffices to prove that $\Theta_\RR$ is a linear transformation.
By General Linear Group is Group:
:$\Theta_\RR$ is a linear transformation {{iff}} its inverse ${\Theta_\RR}^{-1}$ is a linear transformation.
Therefore, it suffices to show that:
:$\forall p, q \in \EE, \mu \in K: \map { {\Theta_\RR}^{-1} } {\mu \cdot p + q} = \mu \cdot \map { {\Theta_\RR}^{-1} } p + \map { {\Theta_\RR}^{-1} } g$
Thus:
{{begin-eqn}}
{{eqn | l = \map { {\Theta_\RR}^{-1} } {\mu \cdot p + q}
      | r = \map { {\Theta_\RR}^{-1} } {\map {\Theta_\RR} {\mu \cdot \map { {\Theta_\RR}^{-1} } p} + q}
      | c = Definition of $\mu \cdot p$
}}
{{eqn | r = {\Theta_\RR}^{-1} \map {\Theta_\RR} {\mu \cdot \map { {\Theta_\RR}^{-1} } p + \map { {\Theta_\RR}^{-1} } q}
      | c = Definition of $+$ in $\EE$
}}
{{eqn | r = \mu \cdot \map { {\Theta_\RR}^{-1} } p + \map { {\Theta_\RR}^{-1} } q
      | c = because $\map { {\Theta_\RR}^{-1} } {\Theta_\RR}$ is the identity mapping
}}
{{end-eqn}}
This is the required identity.
{{Qed}}
Category:Affine Geometry
d8bitbdj0bh7199vx50ird9c44wfbgm
Theorem: Reflexive Reduction is Antireflexive

Let $\RR$ be a relation on a set $S$.
Let $\RR^\ne$ denote the reflexive reduction of $\RR$.
Then $\RR^\ne$ is antireflexive.

Proof:
By the definition of reflexive reduction:
:$\RR^\ne = \RR \setminus \Delta_S$
where $\Delta_S$ denotes the diagonal relation on $S$.
By Set Difference Intersection with Second Set is Empty Set:
:$\paren {\RR \setminus \Delta_S} \cap \Delta_S = \O$
Hence by Relation is Antireflexive iff Disjoint from Diagonal Relation, $\RR^\ne$ is antireflexive.
{{qed}}
Theorem: Equivalence of Definitions of Strict Ordering

Let $S$ be a set.
Let $\RR$ be a relation on $S$.
{{TFAE|def = Strict Ordering}}

Proof:
Let $\RR$ be transitive.
Then by Transitive Relation is Antireflexive iff Asymmetric it follows directly that:
:$(1): \quad$ If $\RR$ is antireflexive then it is asymmetric
:$(2): \quad$ If $\RR$ is asymmetric then it is antireflexive.
{{qed}}
Category:Strict Orderings
5qtldkiz3xr0f1zgffx5gc1m0m0a7fr
Theorem: Subband iff Idempotent under Induced Operation

Let $\struct {S, \circ}$ be a band.
Let $\struct {\powerset S, \circ_\PP}$ be the algebraic structure consisting of the power set of $S$ and the operation induced on $\powerset S$ by $\circ$.
Let $X \in \powerset S$.
Then $X$ is idempotent {{iff}} $\struct {X, \circ}$ is a subband of $\struct {S, \circ}$.

Proof:
=== Subbandhood implies Idempotency ===
Theorem: Restriction of Idempotent Operation is Idempotent

Let $\struct {S, \circ}$ be an algebraic structure.
Let $T \subseteq S$.
Let the operation $\circ$ be idempotent.
Then $\circ$ is also idempotent upon restriction  to $\struct {T, \circ \restriction_T}$.

Proof:
{{begin-eqn}}
{{eqn | l = T
      | o = \subseteq
      | r = S
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | q = \forall a \in T
      | l = a
      | o = \in
      | r = S
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = a \mathop {\circ \restriction_T} a
      | r = a \circ a
      | c = {{Defof|Restriction of Operation}}
}}
{{eqn | r = a
      | c = {{Defof|Idempotence}}
}}
{{end-eqn}}
{{qed}}
Category:Abstract Algebra
Category:Idempotence
jd9u548z4lp5yvasiqmuzc1z43hm98a
Theorem: Subband of Induced Operation is Set of Subbands

Let $\struct {S, \circ}$ be a band.
Let $\struct {\powerset S, \circ_\PP}$ be the algebraic structure consisting of:
: the power set $\powerset S$ of $S$
and
: the operation $\circ_\PP$ induced on $\powerset S$ by $\circ$.
Let $T \subseteq \powerset S$.
Let $\struct {T, \circ_\PP}$ be a subband of $\struct {\powerset S, \circ_\PP}$.
Then every element of $T$ is a subband of $\struct {S, \circ}$.

Proof:
{{improve|See talk page}}
Theorem: Composition of Commuting Idempotent Mappings is Idempotent

Let $S$ be a set.
Let $f, g: S \to S$ be idempotent mappings from $S$ to $S$.
Let:
:$f \circ g = g \circ f$
where $\circ$ denotes composition.
Then $f \circ g$ is idempotent.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {f \circ g} \circ \paren {f \circ g}
      | r =  f \circ \paren {g \circ f} \circ g
      | c = Composition of Mappings is Associative
}}
{{eqn | r = f \circ \paren {f \circ g} \circ g
      | c = by hypothesis
}}
{{eqn | r = \paren {f \circ f} \circ \paren {g \circ g}
      | c = Composition of Mappings is Associative
}}
{{eqn | r = f \circ g
      | c = $f$ and $g$ are idempotent by hypothesis
}}
{{end-eqn}}
{{qed}}
Theorem: Composition of Commuting Idempotent Mappings is Idempotent

Let $S$ be a set.
Let $f, g: S \to S$ be idempotent mappings from $S$ to $S$.
Let:
:$f \circ g = g \circ f$
where $\circ$ denotes composition.
Then $f \circ g$ is idempotent.

Proof:
By Set of all Self-Maps under Composition forms Semigroup, the set of all self-maps on $S$ forms a semigroup under composition.
The result follows from Product of Commuting Idempotent Elements is Idempotent.
{{qed}}
Theorem: Compositions of Closure Operators are both Closure Operators iff Operators Commute

Let $\struct {S, \preceq}$ be an ordered set.
Let $f$ and $g$ be closure operators on $S$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$f \circ g$ and $g \circ f$ are both closure operators}}
{{item|(2):|$f$ and $g$ commute (that is, $f \circ g {{=}} g \circ f$)}}
{{item|(3):|$\Img {f \circ g} {{=}} \Img {g \circ f}$}}
{{end-itemize}}
where $\Img \cdot$ denotes the image of a mapping.

Proof:
By Composition of Inflationary Mappings is Inflationary:
:$f \circ g$ and $g \circ f$ are inflationary.
By Composite of Increasing Mappings is Increasing:
:$f \circ g$ and $g \circ f$ are increasing.
Thus each of the two composite mappings will be a closure operator {{iff}} it is idempotent.
Therefore the equivalences follow from Composition of Inflationary and Idempotent Mappings.
{{qed}}
Category:Closure Operators
2sryc9fxdu7ndyx4hddka44kt8spvyz
Theorem: Composition of Inflationary Mappings is Inflationary

Let $\struct {S, \preceq}$ be an ordered set.
Let $f, g: S \to S$ be inflationary mappings.
Then $f \circ g$, the composition of $f$ and $g$, is also inflationary.

Proof:
Let $x \in S$.
{{begin-eqn}}
{{eqn | n = 1
      | l = x
      | o = \preceq
      | r = \map g x
      | c = $g$ is inflationary
}}
{{eqn | n = 2
      | l = \map g x
      | o = \preceq
      | r = \map f {\map g x}
      | c = $f$ is inflationary
}}
{{eqn | l = x
      | o = \preceq
      | r = \map f {\map g x}
      | c = $(1)$ and $(2)$ and $\preceq$ is an ordering and hence transitive
}}
{{eqn | ll= \leadsto 
      | l = x
      | o = \preceq
      | r = \map {\paren {f \circ g} } x
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
Since this holds for all $x \in S$, $f \circ g$ is inflationary.
{{qed}}
Category:Order Theory
5xqbvy0hqqelai66n80k2wya61dpqp4
Theorem: Fixed Point of Idempotent Mapping

Let $S$ be a set.
Let $f: S \to S$ be an idempotent mapping.
Let $\Img f$ be the image of $f$.
Let $x \in S$.
Then $x$ is a fixed point of $f$ {{iff}} $x \in \Img f$.

Proof:
=== Necessary Condition ===
Let $x$ be a fixed point of $f$.
Then:
:$\map f x = x$
and so by definition of image of mapping:
:$x \in \Img f$
{{qed|lemma}}
Theorem: Symmetric Closure of Ordering may not be Transitive

Let $\struct {S, \preceq}$ be an ordered set.
Let $\preceq^\leftrightarrow$ be the symmetric closure of $\preceq$.
Then it is not necessarily the case that $\preceq^\leftrightarrow$ is transitive.

Proof:
Proof by Counterexample:
Let $S = \set {a, b, c}$ where $a$, $b$, and $c$ are distinct.
Let:
:${\preceq} = \set {\tuple {a, a}, \tuple {b, b}, \tuple {c, c}, \tuple {a, c}, \tuple {b, c} }$:
Then $\preceq$ is an ordering, but $\preceq^\leftrightarrow$ is not transitive, as follows:
$\preceq$ is reflexive because it contains the diagonal relation on $S$.
That $\preceq$ is transitive and antisymmetric can be verified by inspecting all ordered pairs of its elements.
Thus $\preceq$ is an ordering.
Now consider $\preceq^\leftrightarrow$, the symmetric closure of $\preceq$:
:${\preceq^\leftrightarrow} = {\preceq} \cup {\preceq}^{-1} = \set{\tuple {a, a}, \tuple {b, b}, \tuple {c, c}, \tuple {a, c}, \tuple {c, a}, \tuple {b, c}, \tuple {c, b} }$
by inspection.
Now $\tuple {a, c} \in {\preceq^\leftrightarrow}$ and $\tuple {c, b} \in {\preceq^\leftrightarrow}$, but $\tuple {a, b} \notin {\preceq^\leftrightarrow}$.
Thus $\preceq^\leftrightarrow$ is not transitive.
{{qed}}
Category:Orderings
Category:Symmetric Closures
Category:Transitive Relations
s4b1pktjn6a6gcgmgytevjgvgi6wa6q
Theorem: Composition of Idempotent Mappings

Let $S$ be a set.
Let $f, g: S \to S$ be idempotent mappings.
Suppose that $f \circ g$ and $g \circ f$ have the same images.
That is, suppose that $f \sqbrk {g \sqbrk S} = g \sqbrk {f \sqbrk S}$.
Then $f \circ g$ and $g \circ f$ are idempotent.

Proof:
Let $x \in S$.
By the premise:
:$\map f {\map g x} \in g \sqbrk {f \sqbrk S}$
Since $f \sqbrk S \subseteq S$:
:$\map f {\map g x} \in g \sqbrk S$
Thus for some $y \in S$:
:$\map f {\map g x} = \map g y$
Since $g$ is idempotent:
:$\map g {\map g y} = \map g y$
By the choice of $y$:
:$\map g {\map f {\map g x} } = \map g {\map g y} = \map g y = \map f {\map g x}$
Thus:
:$\map f {\map g {\map f {\map g x} } } = \map f {\map f {\map g x} } = \map f {\map g x}$
That is, $f \circ g$ is idempotent.
{{qed}}
Category:Idempotent Mappings
Category:Composite Mappings
188o1vw8v5s7jzlw3xg1s414okta2j3
Theorem: Composition of Inflationary and Idempotent Mappings

Let $\struct {S, \preceq}$ be an ordered set.
Let $f$ and $g$ be inflationary and idempotent mappings on $S$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$f \circ g$ and $g \circ f$ are both idempotent}}
{{item|(2):|$f$ and $g$ commute (that is, $f \circ g {{=}} g \circ f$)}}
{{item|(3):|$\Img {f \circ g} {{=}} \Img {g \circ f}$}}
{{end-itemize}}
where:
:$\circ$ represents composition
:$\Img f$ represents the image of a mapping $f$.

Proof:
=== $(2)$ implies $(1)$ ===
Follows from Composition of Commuting Idempotent Mappings is Idempotent.
{{qed|lemma}}
Theorem: Closure is Smallest Closed Successor

Let $\struct {S, \preceq}$ be an ordered set.
Let $f: S \to S$ be a closure operator on $S$.
Let $x \in S$.
Then $\map f x$ is the smallest closed element that succeeds $x$.

Proof:
By the definition of closure operator, $f$ is inflationary.
Thus $x \preceq \map f x$.
By definition, $\map f x$ is closed.
So $\map f x$ is a closed element that succeeds $x$.
We will now show that it is the smallest such.
Let $k$ be a closed element of $S$ such that $x \preceq k$.
Since $f$ is a closure operator, it is increasing.
Therefore $\map f x \preceq \map f k$.
Since $k$ is closed, $\map f k = k$.
Thus $\map f x \preceq k$.
{{qed}}
Category:Closure Operators
1955mm4t98ditsvzrbvqb6rtpq7y9zu
Theorem: Closed Elements Uniquely Determine Closure Operator

Let $\struct {S, \preceq}$ be an ordered set.
Let $f, g: S \to S$ be closure operators on $S$.
Suppose that $f$ and $g$ have the same closed elements.
Then $f = g$.

Proof:
Let $x \in S$.
Let $C$ be the set of closed elements of $S$ ({{WRT}} either $f$ or $g$) that succeed $x$.
By Closure is Smallest Closed Successor, $\map f x$ and $\map g x$ are smallest closed successors of $x$.
That is, $\map f x$ and $\map g x$ are smallest elements of $C \cap x^\succeq$, where $x^\succeq$ denotes the upper closure of $x$.
By Smallest Element is Unique:
:$\map f x = \map g x$
As $x \in S$ is arbitrary it follows that:
:$\forall x \in S: \map f x = \map g x$
Hence by Equality of Mappings:
:$f = g$
{{qed}}
Category:Closure Operators
gzmnc6vhwhagmgsm8lu9gthmwohtnrt
Theorem: Equivalence of Definitions of Closed Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $\cl$ be a closure operator on $S$.
Let $x \in S$.
{{TFAE|def = Closed Element}}

Proof:
Let $\struct {S, \preceq}$ be an ordered set.
Let $\cl: S \to S$ be a closure operator on $S$.
Let $x \in S$.
By the definition of closure operator, $\cl$ is idempotent.
Thus by Fixed Point of Idempotent Mapping:
:An element of $S$ is a fixed point of $\cl$ {{iff}} it is in the image of $\cl$.
Thus the above definitions are equivalent.
{{qed}}
Category:Closed Elements
eqbq1t77njfpjomy2mjwmxbrb9oyen8
Theorem: Square of Number Always Exists

Let $x$ be a number.
Then its square $x^2$ is guaranteed to exist.

Proof:
Whatever flavour of number under discussion, the algebraic structure $\struct {\mathbb K, +, \times}$ in which this number sits is at least a semiring.
The binary operation that is multiplication is therefore closed on that algebraic structure.
Therefore:
: $\forall x \in \mathbb K: x \times x \in \mathbb K$
{{qed}}
Category:Numbers
h9o91tir35n4ut6k92frbx01j9dqge4
Theorem: Schröder Rule

Let $A$, $B$ and $C$ be relations on a set $S$.
{{TFAE}}
:$(1): \quad A \circ B \subseteq C$
:$(2): \quad A^{-1} \circ \overline C \subseteq \overline B$
:$(3): \quad \overline C \circ B^{-1} \subseteq \overline A$
where:
:$\circ$ denotes relation composition
:$A^{-1}$ denotes the inverse of $A$
:$\overline A$ denotes the complement of $A$.

Proof:
=== $(1)$ iff $(2)$ ===
By the definition of relation composition and subset we have that statement $(1)$ may be written as:
:$(1'): \quad \forall x, y, z \in S: \paren {\tuple {y, z} \in A  \land \tuple {x, y} \in B \implies \tuple {x, z} \in C}$
Using a different arrangement of variable names, statement $(2)$ can be written:
:$(2'): \quad \forall x, y, z \in S: \paren {\tuple {z, y} \in A^{-1} \land \tuple {x, z} \in \overline C \implies \tuple {x, y} \in \overline B}$
By the definition of inverse relation and the complement of a relation we can rewrite this as:
:$(2''): \quad \forall x, y, z \in S: \paren {\tuple {y, z} \in A  \land \tuple {x, z} \notin C) \implies \tuple {x, y} \notin B}$
We shall use the method of truth tables.
The two statements will be equivalent {{iff}} the columns under the main connectives, which is $\implies$ in each case, are identical.
'''Statement 1:'''
$\begin{array}{ccccc}
(\tuple {y, z} \in A & \land & \tuple {x, y} \in B) & \implies & \tuple {x, z} \in C \\
\hline
\T & \T & \T & \T & \T \\
\T & \T & \T & \F & \F \\
\T & \F & \F & \T & \T \\
\T & \F & \F & \T & \F \\
\F & \F & \T & \T & \T \\
\F & \F & \T & \T & \F \\
\F & \F & \F & \T & \T \\
\F & \F & \F & \T & \F \\
\end{array}$
'''Statement 2:'''
$\begin{array}{ccccc}
(\tuple {y, z} \in A & \land & \tuple {x, z} \notin C) & \implies & \tuple {x, y} \notin B \\
\hline
\T & \F & \F & \T & \F \\
\T & \T & \T & \F & \F \\
\T & \F & \F & \T & \T \\
\T & \T & \T & \T & \T \\
\F & \F & \F & \T & \F \\
\F & \F & \T & \T & \F \\
\F & \F & \F & \T & \T \\
\F & \F & \T & \T & \T \\
\end{array}$
{{qed|lemma}}
=== $(2)$ iff $(3)$ ===
{{finish}}
Theorem: Schröder Rule

Let $A$, $B$ and $C$ be relations on a set $S$.
{{TFAE}}
:$(1): \quad A \circ B \subseteq C$
:$(2): \quad A^{-1} \circ \overline C \subseteq \overline B$
:$(3): \quad \overline C \circ B^{-1} \subseteq \overline A$
where:
:$\circ$ denotes relation composition
:$A^{-1}$ denotes the inverse of $A$
:$\overline A$ denotes the complement of $A$.

Proof:
By the definition of relation composition and subset we have that statement $(1)$ may be written as:
:$(1') \quad \forall x, y, z \in S: \paren {\tuple {y, z} \in A \land \tuple {x, y} \in B \implies \tuple {x, z} \in C}$
{{explain|Actually, that only gets us to $\forall x, z \in S: \paren {\paren {\exists y \in S: \tuple {y, z} \in A \land \tuple {x, y} \in B} \implies \tuple {x, z} \in C}$.}}
Using a different arrangement of variable names, statement $(2)$ can be written:
:$(2') \quad \forall x, y, z \in S: \paren {\tuple {z, y} \in A^{-1} \land \tuple {x, z} \in \overline C \implies \tuple {x, y} \in \overline B}$
By the definition of the inverse and the complement of a relation we can rewrite this as:
:$(2'') \quad \forall x, y, z \in S: \paren {\tuple {y, z} \in A \land \tuple {x, z} \notin C \implies \tuple {x, y} \notin B}$
Similarly, statement $(3)$ can be written:
:$(3') \quad \forall x, y, z \in S: \paren {\tuple {x, z} \in \overline C \land \tuple {y, x} \in B^{-1} \implies \tuple {y, z} \in \overline A}$
By the definition of the inverse and the complement of a relation we can rewrite this as:
:$(3'') \quad \forall x, y, z \in S: \paren {\tuple {x, z} \notin C \land \tuple {x, y} \in B \implies \tuple {y, z} \notin A}$
So in all we have:
:$(1') \quad \forall x, y, z \in S: \paren {\tuple {y, z} \in A \land \tuple {x, y} \in B  \implies \tuple {x, z} \in C}$
:$(2'') \quad \forall x, y, z \in S: \paren {\tuple {y, z} \in A \land \tuple {x, z} \notin C \implies \tuple {x, y} \notin B}$
:$(3'') \quad \forall x, y, z \in S: \paren {\tuple {x, z} \notin C \land \tuple {x, y} \in B \implies \tuple {y, z} \notin A}$
{{finish}}
Theorem: Equivalence of Definitions of Dual Relation

{{TFAE|def = Dual Relation}}
Let $\RR \subseteq S \times T$ be a relation.

Proof:
Let $\tuple {x, y} \in \paren {\overline \RR}^{-1}$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \overline \RR
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {y, x}
      | o = \in
      | r = \overline \RR
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {y, x}
      | o = \notin
      | r = \RR
      | c = {{Defof|Complement of Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \notin
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \in
      | r = \overline {\paren {\RR^{-1} } }
      | c = {{Defof|Complement of Relation}}
}}
{{end-eqn}}
{{qed}}
Category:Relation Theory
ensi99c6zqi2h5m2vwmz30jqqt18exa
Theorem: Trivial Gradation is Gradation

Let $\struct {R, +, \circ}$ be a ring.
Let $\struct {M, e, \cdot}$ be a monoid.
Let
:$\ds R = \bigoplus_{m \mathop \in M} R_m$
be the trivial $M$-gradation on $R$.
This is a gradation on $R$.

Proof:
We are required to show that:
:$\forall x \in R_m, y \in R_n: x \circ y \in R_{m \cdot n}$
First suppose that $m = n = e$ are both the identity.
In this case, $R_m = R_n = R$.
Since by definition, $R$ is closed under $\circ$, it follows that
:$\forall x \in R, y \in R: x \circ y \in R$
as required.
Now suppose that either $m \ne e$ or $n \ne e$.
After possibly exchanging $m$ and $n$, we may as well assume that $n \ne e$.
In particular, $R_n = \mathbf 0$ is the zero ring.
So if $y \in R_n$, then $y = 0$.
Therefore, for every $x \in R_m$, by Ring Product with Zero, we must have 
:$x \circ y = x \circ 0 = 0$
Since $R_{m \cdot n}$ is an abelian group it must by definition contain $0$.
Therefore $x \circ y \in R_{m \cdot n}$ as required.
{{Qed}}
Category:Ring Theory
hdzdlh3nsbmkp7x22xbyq68cmcnikyn
Theorem: Fixed Point of Mappings is Fixed Point of Composition

Let $S$ be a set.
Let $f, g: S \to S$ be mappings.
Let $x \in S$ be a fixed point of both $f$ and $g$.
Then $x$ is also a fixed point of $f \circ g$, the composition of $f$ and $g$.

Proof:
Since $x$ is a fixed point of $g$:
: $\map g x = x$
Thus:
: $\map f {\map g x} = \map f x$
Since $x$ is a fixed point of $f$:
: $\map f x = x$
It follows that:
: $\map {\paren {f \circ g} } x = \map f {\map g x} = x$
Thus $x$ is a fixed point of $f \circ g$.
{{qed}}
Category:Mapping Theory
5vr2j2gkw62xlk2jb3eooda53pg2quo
Theorem: Fixed Point of Mappings is Fixed Point of Composition/General Result

Let $S$ be a set.
Let $n \in \N$ be a strictly positive integer.
Let $\N_n$ be the initial segment of $n$ in $\N$.
That is, let $\N_n = \set {0, 1, \dots, n-1}$.
For each $i \in \N_n$, let $f_i: S \to S$ be a mapping.
Let $x \in S$ be a fixed point of $f_i$ for each $i \in \N_n$.
Let $g = f_0 \circ f_1 \circ \dots \circ f_{n-1}$ be the composition of all the $f_i$s.
Then $x$ is a fixed point of $g$.

Proof:
The proof proceeds by mathematical induction on $n$, the number of mappings.
Theorem: Polynomial has Integer Coefficients iff Content is Integer

$f$ has integer coefficients {{iff}} $\cont f$ is an integer.

Proof:
If $f \in \Z \sqbrk X$ then $\cont f \in \Z$ by definition of content.
Conversely, suppose that:
:$f = a_d X^d + \cdots + a_1 X + a_0 \notin \Z \sqbrk X$
Let $m = \min \set {n \in \N : n f \in \Z \sqbrk X}$.
Then, by definition of content:
:$\cont f = \dfrac 1 m \gcd \set {m a_d, \ldots, m a_0}$
So $\cont f \in \Z$ would mean that this GCD is a multiple of $m$.
This, however, means that for each $i$, $\dfrac {m a_i} m = a_i$ is an integer, which contradicts our assumption that $f \notin \Z \sqbrk X$.
{{Qed}}
Category:Content of Polynomial
tle7se59a7q909dvaxtit66n56tgio1