English
If H1 and H2 are normal subgroups of G and their intersection is trivial (Disjoint), then every element of H1 commutes with every element of H2.
Русский
Если H1 и H2 нормальны в G и их пересечение тривиально, то любые элементы из H1 и H2 commute.
LaTeX
$$Disjoint(H1,H2) ∧ H1 ⫽ G ∧ H2 ⫽ G ⇒ ∀ x ∈ H1, ∀ y ∈ H2, xy = yx$$
Lean4
/-- Elements of disjoint, normal subgroups commute. -/
@[to_additive /-- Elements of disjoint, normal subgroups commute. -/
]
theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂)
(x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y :=
by
suffices x * y * x⁻¹ * y⁻¹ = 1 by
change x * y = y * x
· rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
simpa
apply hdis.le_bot
constructor
· suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)
· change x * y * x⁻¹ * y⁻¹ ∈ H₂
apply H₂.mul_mem _ (H₂.inv_mem hy)
apply hH₂.conj_mem _ hy
