Direct Image of Intersection with Inverse Image

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $S$ and $T$ be sets.

Let $f: S \to T$ be a mapping.

Let:

$f^\to: \powerset S \to \powerset T$ denote the direct image mapping of $f$
$f^\gets: \powerset T \to \powerset S$ denote the inverse image mapping of $f$

where $\powerset S$ denotes the power set of $S$.


Then:

$\forall A \in \powerset S, B \in \powerset T: \map {f^\to} {A \cap \map {f^\gets} B} = \map {f^\to} A \cap B$


Proof

Let $A \in \powerset S, B \in \powerset T$ be arbitrary.

Then:

\(\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}\) \(\subseteq\) \(\displaystyle \map {f^\to} A \cap \map {f^\to} {\map {f^\gets} B}\) Image of Intersection under Mapping
\(\displaystyle \) \(\subseteq\) \(\displaystyle \map {f^\to} A \cap B\) Subset of Codomain is Superset of Image of Preimage


Let $x \in \map {f^\to} A \cap B$.

\(\displaystyle x\) \(\in\) \(\displaystyle \map {f^\to} A\) Definition of Set Intersection
\((1):\quad\) \(\displaystyle \leadsto \ \ \) \(\displaystyle x\) \(=\) \(\displaystyle \map f a\) for some $a \in A$
and:
\(\displaystyle x\) \(\in\) \(\displaystyle B\) Definition of Set Intersection
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f a\) \(\in\) \(\displaystyle B\) from $(1)$ above
\(\displaystyle \leadsto \ \ \) \(\displaystyle a\) \(\in\) \(\displaystyle \map {f^\gets} B\) Definition of Inverse Image Mapping
\(\displaystyle \leadsto \ \ \) \(\displaystyle a\) \(\in\) \(\displaystyle A \cap \map {f^\gets} B\) Definition of Set Intersection
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map f a\) \(\in\) \(\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}\) Definition of Direct Image Mapping
\(\displaystyle \leadsto \ \ \) \(\displaystyle x\) \(\in\) \(\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}\) as $x = \map f a$
\(\displaystyle \leadsto \ \ \) \(\displaystyle \map {f^\to} A \cap B\) \(\subseteq\) \(\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}\) Definition of Subset


Thus we have:

$\map {f^\to} {A \cap \map {f^\gets} B} \subseteq \map {f^\to} A \cap B$

and:

$\map {f^\to} A \cap B \subseteq \map {f^\to} {A \cap \map {f^\gets} B}$

and so:

$\forall A \in \powerset S, B \in \powerset T: \map {f^\to} {A \cap \map {f^\gets} B} = \map {f^\to} A \cap B$

by definition of set equality.

$\blacksquare$


Sources