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

Proof

Step	Hyp	Ref	Expression
1		cvp	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ HAtoms ) → ( ( 𝐵 ∩ 𝐴 ) = 0ℋ ↔ 𝐵 ⋖ℋ ( 𝐵 ∨ℋ 𝐴 ) ) )
2		atelch	⊢ ( 𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )
3		chjcom	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 ) )
4	2 3	sylan2	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ HAtoms ) → ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 ) )
5	4	breq2d	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ HAtoms ) → ( 𝐵 ⋖ℋ ( 𝐵 ∨ℋ 𝐴 ) ↔ 𝐵 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
6	1 5	bitrd	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ HAtoms ) → ( ( 𝐵 ∩ 𝐴 ) = 0ℋ ↔ 𝐵 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐵 ∩ 𝐴 ) = 0ℋ ↔ 𝐵 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
8		cvdmd	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐵 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐴 𝑀ℋ* 𝐵 )
9	8	3expia	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐵 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ* 𝐵 ) )
10	2 9	sylan	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( 𝐵 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ* 𝐵 ) )
11	7 10	sylbid	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐵 ∩ 𝐴 ) = 0ℋ → 𝐴 𝑀ℋ* 𝐵 ) )
12		atnssm0	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ HAtoms ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐴 ) = 0ℋ ) )
13	12	ancoms	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐴 ) = 0ℋ ) )
14	13	con1bid	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( ¬ ( 𝐵 ∩ 𝐴 ) = 0ℋ ↔ 𝐴 ⊆ 𝐵 ) )
15		ssdmd1	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 𝑀ℋ* 𝐵 )
16	15	3expia	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 → 𝐴 𝑀ℋ* 𝐵 ) )
17	2 16	sylan	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 → 𝐴 𝑀ℋ* 𝐵 ) )
18	14 17	sylbid	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → ( ¬ ( 𝐵 ∩ 𝐴 ) = 0ℋ → 𝐴 𝑀ℋ* 𝐵 ) )
19	11 18	pm2.61d	⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ* 𝐵 )