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	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → 𝐴 𝑀ℋ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cvp	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
2		atelch	⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
3		cvexch	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
4		cvmd	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 )
5	4	3expia	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵 ) )
6	3 5	sylbird	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 ) )
7	2 6	sylan2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 ) )
8	1 7	sylbid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → 𝐴 𝑀ℋ 𝐵 ) )
9		atnssm0	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
10	9	con1bid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐵 ⊆ 𝐴 ) )
11		ssmd2	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
12	11	3com12	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
13	2 12	syl3an2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
14	13	3expia	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐵 ⊆ 𝐴 → 𝐴 𝑀ℋ 𝐵 ) )
15	10 14	sylbid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ ( 𝐴 ∩ 𝐵 ) = 0ℋ → 𝐴 𝑀ℋ 𝐵 ) )
16	8 15	pm2.61d	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → 𝐴 𝑀ℋ 𝐵 )