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

Metamath Proof Explorer

Theorem shmodi

Description: The modular law is implied by the closure of subspace sum. Part of proof of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 23-Nov-2004) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	shmod.1	$⊢ A \in S_{ℋ}$
		shmod.2	$⊢ B \in S_{ℋ}$
		shmod.3	$⊢ C \in S_{ℋ}$
	Assertion	shmodi	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land A \subseteq C) \to (A \lor_{ℋ} B) \cap C \subseteq A \lor_{ℋ} (B \cap C)$

Proof

Step	Hyp	Ref	Expression
1		shmod.1	$⊢ A \in S_{ℋ}$
2		shmod.2	$⊢ B \in S_{ℋ}$
3		shmod.3	$⊢ C \in S_{ℋ}$
4	1 2 3	shmodsi	$⊢ A \subseteq C \to (A +_{ℋ} B) \cap C \subseteq A +_{ℋ} (B \cap C)$
5		ineq1	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to (A +_{ℋ} B) \cap C = (A \lor_{ℋ} B) \cap C$
6	5	sseq1d	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to ((A +_{ℋ} B) \cap C \subseteq A +_{ℋ} (B \cap C) \leftrightarrow (A \lor_{ℋ} B) \cap C \subseteq A +_{ℋ} (B \cap C))$
7	4 6	imbitrid	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to (A \subseteq C \to (A \lor_{ℋ} B) \cap C \subseteq A +_{ℋ} (B \cap C))$
8	7	imp	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land A \subseteq C) \to (A \lor_{ℋ} B) \cap C \subseteq A +_{ℋ} (B \cap C)$
9	2 3	shincli	$⊢ B \cap C \in S_{ℋ}$
10	1 9	shsleji	$⊢ A +_{ℋ} (B \cap C) \subseteq A \lor_{ℋ} (B \cap C)$
11	8 10	sstrdi	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land A \subseteq C) \to (A \lor_{ℋ} B) \cap C \subseteq A \lor_{ℋ} (B \cap C)$