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

Metamath Proof Explorer

Theorem mdsl3

Description: Sublattice mapping for a modular pair. Part of Theorem 1.3 of MaedaMaeda p. 2. (Contributed by NM, 26-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	mdsl3	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land A \cap B \subseteq C \land C \subseteq B)) \to (C \lor_{ℋ} A) \cap B = C$

Proof

Step	Hyp	Ref	Expression
1		mdi	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land C \subseteq B)) \to (C \lor_{ℋ} A) \cap B = C \lor_{ℋ} (A \cap B)$
2	1	3adantr2	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land A \cap B \subseteq C \land C \subseteq B)) \to (C \lor_{ℋ} A) \cap B = C \lor_{ℋ} (A \cap B)$
3		chincl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \cap B \in C_{ℋ}$
4		chlejb2	$⊢ (A \cap B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \cap B \subseteq C \leftrightarrow C \lor_{ℋ} (A \cap B) = C)$
5	3 4	stoic3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \cap B \subseteq C \leftrightarrow C \lor_{ℋ} (A \cap B) = C)$
6	5	biimpa	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land A \cap B \subseteq C) \to C \lor_{ℋ} (A \cap B) = C$
7	6	3ad2antr2	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land A \cap B \subseteq C \land C \subseteq B)) \to C \lor_{ℋ} (A \cap B) = C$
8	2 7	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land A \cap B \subseteq C \land C \subseteq B)) \to (C \lor_{ℋ} A) \cap B = C$