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 \in C_{ℋ} \land B \in HAtoms) \to A 𝑀_{ℋ} B$

Proof

Step	Hyp	Ref	Expression
1		cvp	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A \cap B = 0_{ℋ} \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$
2		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
3		cvexch	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \cap B) ⋖_{ℋ} B \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$
4		cvmd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land (A \cap B) ⋖_{ℋ} B) \to A 𝑀_{ℋ} B$
5	4	3expia	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \cap B) ⋖_{ℋ} B \to A 𝑀_{ℋ} B)$
6	3 5	sylbird	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} (A \lor_{ℋ} B) \to A 𝑀_{ℋ} B)$
7	2 6	sylan2	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A ⋖_{ℋ} (A \lor_{ℋ} B) \to A 𝑀_{ℋ} B)$
8	1 7	sylbid	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A \cap B = 0_{ℋ} \to A 𝑀_{ℋ} B)$
9		atnssm0	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \cap B = 0_{ℋ})$
10	9	con1bid	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg A \cap B = 0_{ℋ} \leftrightarrow B \subseteq A)$
11		ssmd2	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ} \land B \subseteq A) \to A 𝑀_{ℋ} B$
12	11	3com12	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land B \subseteq A) \to A 𝑀_{ℋ} B$
13	2 12	syl3an2	$⊢ (A \in C_{ℋ} \land B \in HAtoms \land B \subseteq A) \to A 𝑀_{ℋ} B$
14	13	3expia	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (B \subseteq A \to A 𝑀_{ℋ} B)$
15	10 14	sylbid	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg A \cap B = 0_{ℋ} \to A 𝑀_{ℋ} B)$
16	8 15	pm2.61d	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to A 𝑀_{ℋ} B$