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	$$⊢\left(A\in \mathrm{HAtoms}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{𝑀}_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		atdmd	$$⊢\left(A\in \mathrm{HAtoms}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{𝑀}_{\mathscr{H}}^{*}x$$
2	1	ralrimiva	$$⊢A\in \mathrm{HAtoms}\to \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}^{*}x$$
3		atelch	$$⊢A\in \mathrm{HAtoms}\to A\in {\mathbf{C}}_{\mathscr{H}}$$
4		mddmd2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}^{*}x\right)$$
5	3 4	syl	$$⊢A\in \mathrm{HAtoms}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}^{*}x\right)$$
6	2 5	mpbird	$$⊢A\in \mathrm{HAtoms}\to \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x$$
7		breq2	$$⊢x=B\to \left(A{𝑀}_{\mathscr{H}}x\leftrightarrow A{𝑀}_{\mathscr{H}}B\right)$$
8	7	rspcv	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\to A{𝑀}_{\mathscr{H}}B\right)$$
9	6 8	mpan9	$$⊢\left(A\in \mathrm{HAtoms}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{𝑀}_{\mathscr{H}}B$$