This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )