Way Below Relation is Multiplicative implies Pseudoprime Element is Prime

Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice such that

$\ll$ is multiplicative relation

where $\ll$ denotes the way below relation of $L$.

Let $p \in S$.

Then $p$ is a pseudoprime element is a prime element.

Proof

Let $p$ be a pseudoprime element.

Aiming for a contradiction, suppose:

$p$ is not a prime element.

By definition of prime element:

$\exists x, y \in S: x \wedge y \preceq p$ and $x \npreceq p$ and $y \npreceq p$

By definition of continuous:

$\forall z \in S: z^\ll$ is directed.

and

$L$ satisfies the axiom of approximation.

By Axiom of Approximation in Up-Complete Semilattice:

$\exists u \in S: u \ll x \land u \npreceq p$

and

$\exists v \in S: v \ll y \land v \npreceq p$

By Way Below Relation is Auxiliary Relation:

$\ll$ is auxiliary relation.

By Multiplicative Auxiliary Relation iff Congruent:

$u \wedge v \ll x \wedge y$

By definition of transitivity:

$u \wedge v \ll p$

By Characterization of Pseudoprime Element when Way Below Relation is Multiplicative:

$u \preceq p$ or $v \preceq p$

This contradicts $u \npreceq p$ and $v \npreceq p$

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL_7:45