Theorem atmd2

Description: Two Hilbert lattice elements have the dual modular pair property if the second is an atom. Part of Exercise 6 of Kalmbach p. 103. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cvp	|- ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A
2		atelch	|- ( B e. HAtoms -> B e. CH )
3		cvexch	|- ( ( A e. CH /\ B e. CH ) -> ( ( A i^i B ) A
4		cvmd	|- ( ( A e. CH /\ B e. CH /\ ( A i^i B ) A MH B )
5	4	3expia	|- ( ( A e. CH /\ B e. CH ) -> ( ( A i^i B ) A MH B ) )
6	3 5	sylbird	|- ( ( A e. CH /\ B e. CH ) -> ( A A MH B ) )
7	2 6	sylan2	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A A MH B ) )
8	1 7	sylbid	|- ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H -> A MH B ) )
9		atnssm0	|- ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> ( A i^i B ) = 0H ) )
10	9	con1bid	|- ( ( A e. CH /\ B e. HAtoms ) -> ( -. ( A i^i B ) = 0H <-> B C_ A ) )
11		ssmd2	|- ( ( B e. CH /\ A e. CH /\ B C_ A ) -> A MH B )
12	11	3com12	|- ( ( A e. CH /\ B e. CH /\ B C_ A ) -> A MH B )
13	2 12	syl3an2	|- ( ( A e. CH /\ B e. HAtoms /\ B C_ A ) -> A MH B )
14	13	3expia	|- ( ( A e. CH /\ B e. HAtoms ) -> ( B C_ A -> A MH B ) )
15	10 14	sylbid	|- ( ( A e. CH /\ B e. HAtoms ) -> ( -. ( A i^i B ) = 0H -> A MH B ) )
16	8 15	pm2.61d	|- ( ( A e. CH /\ B e. HAtoms ) -> A MH B )