This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atmd

Description: Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of MaedaMaeda p. 31. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atmd ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → A 𝑀 ℋ B

Proof

Step Hyp Ref Expression
1 atdmd ⊢ A ∈ HAtoms ∧ x ∈ C ℋ → A 𝑀 ℋ * x
2 1 ralrimiva ⊢ A ∈ HAtoms → ∀ x ∈ C ℋ A 𝑀 ℋ * x
3 atelch ⊢ A ∈ HAtoms → A ∈ C ℋ
4 mddmd2 ⊢ A ∈ C ℋ → ∀ x ∈ C ℋ A 𝑀 ℋ x ↔ ∀ x ∈ C ℋ A 𝑀 ℋ * x
5 3 4 syl ⊢ A ∈ HAtoms → ∀ x ∈ C ℋ A 𝑀 ℋ x ↔ ∀ x ∈ C ℋ A 𝑀 ℋ * x
6 2 5 mpbird ⊢ A ∈ HAtoms → ∀ x ∈ C ℋ A 𝑀 ℋ x
7 breq2 ⊢ x = B → A 𝑀 ℋ x ↔ A 𝑀 ℋ B
8 7 rspcv ⊢ B ∈ C ℋ → ∀ x ∈ C ℋ A 𝑀 ℋ x → A 𝑀 ℋ B
9 6 8 mpan9 ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → A 𝑀 ℋ B