English
A duplicate formulation of the product identity of modulus-divisions holds: |(a ⊔ c)/(b ⊔ c)|_m · |(a ⊓ c)/(b ⊓ c)|_m = |a/b|_m.
Русский
Дубликат идентичности произведения модулей деления: |(a ⊔ c)/(b ⊔ c)|_м · |(a ⊓ c)/(b ⊓ c)|_м = |a/b|_м.
LaTeX
$$|(a ⊔ c)/(b ⊔ c)|_m \cdot |(a ⊓ c)/(b ⊓ c)|_m = |a / b|_m$$
Lean4
@[to_additive]
theorem mabs_div_sup_mul_mabs_div_inf (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ :=
by
letI : DistribLattice α := CommGroup.toDistribLattice α
calc
|(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
rw [sup_div_inf_eq_mabs_div]
_ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
_ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem, sup_assoc, inf_assoc,
inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
_ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
_ = (b ⊔ a) * c / ((b ⊓ a) * c) := by rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
_ = (b ⊔ a) / (b ⊓ a) := by rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
_ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
