$\;$Dear SE$.$Mathematics community,
I am trying to prove some properties on a Lattice with a proof assistant and extend these properties by interaction with addition $+$ and multiplication $·$ e.g. on a lattice that is also a ring⁽¹⁾.
In particular I am wondering whether it is possible to proof
$$∀\,x\,y\,∀\,z≥0\,.\,\min(x · z, y · z)=\min(x,y) · z$$
or equivalently
$$∀\,x\,y\,∀\,z≥0\,∀\,w\,.\,w ≤ \min(x · z, y · z)⇒w≤\min(x,y) · z$$
without assuming the existence of multiplicative inverses. This would make the proof hold on a lattice-ring and not only on a lattice-field.
E.g. with the assumption of multiplicative inverses, a proof goes like this:
$\begin{align} &w ≤ \min(x · z, y · z)\\ &\quad ⇒\text{by is-min}\\ &w ≤ x · z \quad\text{ and }\quad w ≤ y · z\\ &\quad ⇒\text{by · preserving ≤ for 0 < z}\\ &w · z⁻¹ ≤ x · z · z⁻¹ \quad\text{ and }\quad w · z⁻¹ ≤ y · z · z⁻¹\\ &\quad ⇒\text{by inverse of ·}\\ &w · z⁻¹ ≤ x \quad\text{ and }\quad w · z⁻¹ ≤ y\\ &\quad ⇒\text{by is-min}\\ &w · z⁻¹ ≤ \min(x,y)\\ &\quad ⇒\text{by · preserving ≤ for 0 < z}\\ &w · z⁻¹ · z ≤ \min(x,y) · z\\ &\quad ⇒\text{by inverse of ·}\\ &w ≤ \min(x,y) · z \end{align}$
but I could not come up with a proof without $z⁻¹$. Is that property even derivable then?
regards, Christian
Context
The lattice definition that I am using is:
Let $(A, ≤)$ be a partial order (reflexive, transitive, antisymmetric), and let $\min, \max : A → A → A$ be binary operators on $A$. Then $(A, ≤, \min, \max)$ is a lattice if $\min$ and $\max$ compute bounds in the sense that for every $x, y, w : A$, we have
is-min: $\quad w ≤ \min(x, y)\quad$ iff $\quad w ≤ x$ and $w ≤ y$,
is-max: $\quad \max(x, y) ≤ w\quad$ iff $\quad x ≤ w$ and $y ≤ w$.
and I was able to obtain the "usual" lattice-properties from this definition:
min-≤ : $∀\,x\,y \,.\, \min(x,y) ≤ x$ and $\min(x,y) ≤ y$
min-identity : $∀\,x \,.\, \min(x,x) = x$
min-comm : $∀\,x\,y \,.\, \min(x,y) = \min(y,x)$
min-assoc : $∀\,x\,y\,z \,.\, \min(\min(x,y),z) = \min(x,\min(y,z))$
... similar properties for max
min-max-absorptive : $∀\,x\,y \,.\, \min(x,\max(x,y)) = x$
max-min-absorptive : $∀\,x\,y \,.\, \max(x,\min(x,y)) = x$
From antisymmetry and reflexivity of ≤ we get that "≤ reflects equality" in the following sense: for all $x, y : A$
$\quad ∀ z\,.\,z ≤ x ⇔ z ≤ y\quad$ iff $\quad x = y$,
$\quad ∀ z\,.\,x ≤ z ⇔ y ≤ z\quad$ iff $\quad x = y$
and I used this reflection property in the above proofs.
Footnotes
(1) a ring (or semiring) with a tight apartness relation and
$\quad$ addition + is <-extensional : $∀\,x\,y\,z\,w\,.\,x + y < z + w ⇒ (x < z\text{ or } y < w)$
$\quad$ multiplication · preserves < : $∀\,x\,y.\,x < y ⇒ ∀\,z>0\,.\,x · z < y · z$