Theorem atdmd2

Description: Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	atdmd2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to A{𝑀}_{\mathscr{H}}^{*}B$$

Proof

Step	Hyp	Ref	Expression
1		atdmd	$$⊢\left(B\in \mathrm{HAtoms}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to B{𝑀}_{\mathscr{H}}^{*}A$$
2	1	ancoms	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to B{𝑀}_{\mathscr{H}}^{*}A$$
3		atelch	$$⊢B\in \mathrm{HAtoms}\to B\in {\mathbf{C}}_{\mathscr{H}}$$
4		dmdsym	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow B{𝑀}_{\mathscr{H}}^{*}A\right)$$
5	3 4	sylan2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow B{𝑀}_{\mathscr{H}}^{*}A\right)$$
6	2 5	mpbird	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to A{𝑀}_{\mathscr{H}}^{*}B$$