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

Metamath Proof Explorer

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 )