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 AHAtomsBCA𝑀B

Proof

Step Hyp Ref Expression
1 atdmd AHAtomsxCA𝑀*x
2 1 ralrimiva AHAtomsxCA𝑀*x
3 atelch AHAtomsAC
4 mddmd2 ACxCA𝑀xxCA𝑀*x
5 3 4 syl AHAtomsxCA𝑀xxCA𝑀*x
6 2 5 mpbird AHAtomsxCA𝑀x
7 breq2 x=BA𝑀xA𝑀B
8 7 rspcv BCxCA𝑀xA𝑀B
9 6 8 mpan9 AHAtomsBCA𝑀B