mddmdin0i

Description: If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of Holland p. 1524 to hold. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mddmdin0.1	$⊢ A \in C_{ℋ}$
	mddmdin0.2	$⊢ B \in C_{ℋ}$
	mddmdin0.3	$⊢ \forall x \in C_{ℋ} \forall y \in C_{ℋ} ((x 𝑀_{ℋ}^{*} y \land x \cap y = 0_{ℋ}) \to x 𝑀_{ℋ} y)$
Assertion	mddmdin0i	$⊢ A 𝑀_{ℋ}^{*} B \to A 𝑀_{ℋ} B$

Proof

Step	Hyp	Ref	Expression
1		mddmdin0.1	$⊢ A \in C_{ℋ}$
2		mddmdin0.2	$⊢ B \in C_{ℋ}$
3		mddmdin0.3	$⊢ \forall x \in C_{ℋ} \forall y \in C_{ℋ} ((x 𝑀_{ℋ}^{*} y \land x \cap y = 0_{ℋ}) \to x 𝑀_{ℋ} y)$
4		inindir	$⊢ (A \cap B) \cap ⊥ (A \cap B) = (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B))$
5	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
6	5	chocini	$⊢ (A \cap B) \cap ⊥ (A \cap B) = 0_{ℋ}$
7	4 6	eqtr3i	$⊢ (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ}$
8	5	choccli	$⊢ ⊥ (A \cap B) \in C_{ℋ}$
9	1 8	chincli	$⊢ A \cap ⊥ (A \cap B) \in C_{ℋ}$
10	2 8	chincli	$⊢ B \cap ⊥ (A \cap B) \in C_{ℋ}$
11		breq1	$⊢ x = A \cap ⊥ (A \cap B) \to (x 𝑀_{ℋ}^{} y \leftrightarrow (A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} y)$
12		ineq1	$⊢ x = A \cap ⊥ (A \cap B) \to x \cap y = (A \cap ⊥ (A \cap B)) \cap y$
13	12	eqeq1d	$⊢ x = A \cap ⊥ (A \cap B) \to (x \cap y = 0_{ℋ} \leftrightarrow (A \cap ⊥ (A \cap B)) \cap y = 0_{ℋ})$
14	11 13	anbi12d	$⊢ x = A \cap ⊥ (A \cap B) \to ((x 𝑀_{ℋ}^{} y \land x \cap y = 0_{ℋ}) \leftrightarrow ((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} y \land (A \cap ⊥ (A \cap B)) \cap y = 0_{ℋ}))$
15		breq1	$⊢ x = A \cap ⊥ (A \cap B) \to (x 𝑀_{ℋ} y \leftrightarrow (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} y)$
16	14 15	imbi12d	$⊢ x = A \cap ⊥ (A \cap B) \to (((x 𝑀_{ℋ}^{} y \land x \cap y = 0_{ℋ}) \to x 𝑀_{ℋ} y) \leftrightarrow (((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} y \land (A \cap ⊥ (A \cap B)) \cap y = 0_{ℋ}) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} y))$
17		breq2	$⊢ y = B \cap ⊥ (A \cap B) \to ((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} y \leftrightarrow (A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} (B \cap ⊥ (A \cap B)))$
18		ineq2	$⊢ y = B \cap ⊥ (A \cap B) \to (A \cap ⊥ (A \cap B)) \cap y = (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B))$
19	18	eqeq1d	$⊢ y = B \cap ⊥ (A \cap B) \to ((A \cap ⊥ (A \cap B)) \cap y = 0_{ℋ} \leftrightarrow (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ})$
20	17 19	anbi12d	$⊢ y = B \cap ⊥ (A \cap B) \to (((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} y \land (A \cap ⊥ (A \cap B)) \cap y = 0_{ℋ}) \leftrightarrow ((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} (B \cap ⊥ (A \cap B)) \land (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ}))$
21		breq2	$⊢ y = B \cap ⊥ (A \cap B) \to ((A \cap ⊥ (A \cap B)) 𝑀_{ℋ} y \leftrightarrow (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B)))$
22	20 21	imbi12d	$⊢ y = B \cap ⊥ (A \cap B) \to ((((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} y \land (A \cap ⊥ (A \cap B)) \cap y = 0_{ℋ}) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} y) \leftrightarrow (((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} (B \cap ⊥ (A \cap B)) \land (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ}) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B))))$
23	16 22	rspc2v	$⊢ (A \cap ⊥ (A \cap B) \in C_{ℋ} \land B \cap ⊥ (A \cap B) \in C_{ℋ}) \to (\forall x \in C_{ℋ} \forall y \in C_{ℋ} ((x 𝑀_{ℋ}^{} y \land x \cap y = 0_{ℋ}) \to x 𝑀_{ℋ} y) \to (((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} (B \cap ⊥ (A \cap B)) \land (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ}) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B))))$
24	9 10 23	mp2an	$⊢ \forall x \in C_{ℋ} \forall y \in C_{ℋ} ((x 𝑀_{ℋ}^{} y \land x \cap y = 0_{ℋ}) \to x 𝑀_{ℋ} y) \to (((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} (B \cap ⊥ (A \cap B)) \land (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ}) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B)))$
25	3 24	ax-mp	$⊢ ((A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{*} (B \cap ⊥ (A \cap B)) \land (A \cap ⊥ (A \cap B)) \cap (B \cap ⊥ (A \cap B)) = 0_{ℋ}) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B))$
26	7 25	mpan2	$⊢ (A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{*} (B \cap ⊥ (A \cap B)) \to (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B))$
27	1 2	dmdcompli	$⊢ A 𝑀_{ℋ}^{} B \leftrightarrow (A \cap ⊥ (A \cap B)) 𝑀_{ℋ}^{} (B \cap ⊥ (A \cap B))$
28	1 2	mdcompli	$⊢ A 𝑀_{ℋ} B \leftrightarrow (A \cap ⊥ (A \cap B)) 𝑀_{ℋ} (B \cap ⊥ (A \cap B))$
29	26 27 28	3imtr4i	$⊢ A 𝑀_{ℋ}^{*} B \to A 𝑀_{ℋ} B$

Metamath Proof Explorer

Theorem mddmdin0i

Proof