Theorem atdmd

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

	Ref	Expression
Assertion	atdmd	|- ( ( A e. HAtoms /\ B e. CH ) -> A MH* B )

Proof

Step	Hyp	Ref	Expression
1		cvp	|- ( ( B e. CH /\ A e. HAtoms ) -> ( ( B i^i A ) = 0H <-> B
2		atelch	|- ( A e. HAtoms -> A e. CH )
3		chjcom	|- ( ( B e. CH /\ A e. CH ) -> ( B vH A ) = ( A vH B ) )
4	2 3	sylan2	|- ( ( B e. CH /\ A e. HAtoms ) -> ( B vH A ) = ( A vH B ) )
5	4	breq2d	|- ( ( B e. CH /\ A e. HAtoms ) -> ( B B
6	1 5	bitrd	|- ( ( B e. CH /\ A e. HAtoms ) -> ( ( B i^i A ) = 0H <-> B
7	6	ancoms	|- ( ( A e. HAtoms /\ B e. CH ) -> ( ( B i^i A ) = 0H <-> B
8		cvdmd	|- ( ( A e. CH /\ B e. CH /\ B A MH* B )
9	8	3expia	|- ( ( A e. CH /\ B e. CH ) -> ( B A MH* B ) )
10	2 9	sylan	|- ( ( A e. HAtoms /\ B e. CH ) -> ( B A MH* B ) )
11	7 10	sylbid	|- ( ( A e. HAtoms /\ B e. CH ) -> ( ( B i^i A ) = 0H -> A MH* B ) )
12		atnssm0	|- ( ( B e. CH /\ A e. HAtoms ) -> ( -. A C_ B <-> ( B i^i A ) = 0H ) )
13	12	ancoms	|- ( ( A e. HAtoms /\ B e. CH ) -> ( -. A C_ B <-> ( B i^i A ) = 0H ) )
14	13	con1bid	|- ( ( A e. HAtoms /\ B e. CH ) -> ( -. ( B i^i A ) = 0H <-> A C_ B ) )
15		ssdmd1	|- ( ( A e. CH /\ B e. CH /\ A C_ B ) -> A MH* B )
16	15	3expia	|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B -> A MH* B ) )
17	2 16	sylan	|- ( ( A e. HAtoms /\ B e. CH ) -> ( A C_ B -> A MH* B ) )
18	14 17	sylbid	|- ( ( A e. HAtoms /\ B e. CH ) -> ( -. ( B i^i A ) = 0H -> A MH* B ) )
19	11 18	pm2.61d	|- ( ( A e. HAtoms /\ B e. CH ) -> A MH* B )