dmdmd

Description: The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of MaedaMaeda p. 130. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	dmdmd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow ⊥ (A) 𝑀_{ℋ} ⊥ (B))$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$⊢ y = ⊥ (x) \to (y \subseteq ⊥ (B) \leftrightarrow ⊥ (x) \subseteq ⊥ (B))$
2		oveq1	$⊢ y = ⊥ (x) \to y \lor_{ℋ} ⊥ (A) = ⊥ (x) \lor_{ℋ} ⊥ (A)$
3	2	ineq1d	$⊢ y = ⊥ (x) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)$
4		oveq1	$⊢ y = ⊥ (x) \to y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))$
5	3 4	eqeq12d	$⊢ y = ⊥ (x) \to ((y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)) \leftrightarrow (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))$
6	1 5	imbi12d	$⊢ y = ⊥ (x) \to ((y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \leftrightarrow (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
7	6	rspccv	$⊢ \forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \to (⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
8		choccl	$⊢ x \in C_{ℋ} \to ⊥ (x) \in C_{ℋ}$
9	8	imim1i	$⊢ (⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))) \to (x \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
10	9	com12	$⊢ x \in C_{ℋ} \to ((⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))) \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
11	10	adantl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))) \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
12		chsscon3	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to (B \subseteq x \leftrightarrow ⊥ (x) \subseteq ⊥ (B))$
13	12	biimpd	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to (B \subseteq x \to ⊥ (x) \subseteq ⊥ (B))$
14	13	adantll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (B \subseteq x \to ⊥ (x) \subseteq ⊥ (B))$
15		fveq2	$⊢ (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)) \to ⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = ⊥ (⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))$
16		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
17		chjcl	$⊢ (⊥ (x) \in C_{ℋ} \land ⊥ (A) \in C_{ℋ}) \to ⊥ (x) \lor_{ℋ} ⊥ (A) \in C_{ℋ}$
18	8 16 17	syl2an	$⊢ (x \in C_{ℋ} \land A \in C_{ℋ}) \to ⊥ (x) \lor_{ℋ} ⊥ (A) \in C_{ℋ}$
19		chdmm3	$⊢ (⊥ (x) \lor_{ℋ} ⊥ (A) \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = ⊥ (⊥ (x) \lor_{ℋ} ⊥ (A)) \lor_{ℋ} B$
20	18 19	sylan	$⊢ ((x \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = ⊥ (⊥ (x) \lor_{ℋ} ⊥ (A)) \lor_{ℋ} B$
21		chdmj4	$⊢ (x \in C_{ℋ} \land A \in C_{ℋ}) \to ⊥ (⊥ (x) \lor_{ℋ} ⊥ (A)) = x \cap A$
22	21	adantr	$⊢ ((x \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ (⊥ (x) \lor_{ℋ} ⊥ (A)) = x \cap A$
23	22	oveq1d	$⊢ ((x \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ (⊥ (x) \lor_{ℋ} ⊥ (A)) \lor_{ℋ} B = (x \cap A) \lor_{ℋ} B$
24	20 23	eqtrd	$⊢ ((x \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = (x \cap A) \lor_{ℋ} B$
25	24	anasss	$⊢ (x \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = (x \cap A) \lor_{ℋ} B$
26		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
27		chincl	$⊢ (⊥ (A) \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to ⊥ (A) \cap ⊥ (B) \in C_{ℋ}$
28	16 26 27	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A) \cap ⊥ (B) \in C_{ℋ}$
29		chdmj2	$⊢ (x \in C_{ℋ} \land ⊥ (A) \cap ⊥ (B) \in C_{ℋ}) \to ⊥ (⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) = x \cap ⊥ (⊥ (A) \cap ⊥ (B))$
30	28 29	sylan2	$⊢ (x \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ (⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) = x \cap ⊥ (⊥ (A) \cap ⊥ (B))$
31		chdmm4	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (A) \cap ⊥ (B)) = A \lor_{ℋ} B$
32	31	adantl	$⊢ (x \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ (⊥ (A) \cap ⊥ (B)) = A \lor_{ℋ} B$
33	32	ineq2d	$⊢ (x \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to x \cap ⊥ (⊥ (A) \cap ⊥ (B)) = x \cap (A \lor_{ℋ} B)$
34	30 33	eqtrd	$⊢ (x \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ (⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) = x \cap (A \lor_{ℋ} B)$
35	25 34	eqeq12d	$⊢ (x \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to (⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = ⊥ (⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \leftrightarrow (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B))$
36	35	ancoms	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (⊥ ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)) = ⊥ (⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \leftrightarrow (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B))$
37	15 36	imbitrid	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)) \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B))$
38	14 37	imim12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)))$
39	11 38	syld	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))) \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)))$
40	39	ex	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (x \in C_{ℋ} \to ((⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))) \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B))))$
41	40	com23	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((⊥ (x) \in C_{ℋ} \to (⊥ (x) \subseteq ⊥ (B) \to (⊥ (x) \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = ⊥ (x) \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))) \to (x \in C_{ℋ} \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B))))$
42	7 41	syl5	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \to (x \in C_{ℋ} \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B))))$
43	42	ralrimdv	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \to \forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)))$
44		sseq2	$⊢ x = ⊥ (y) \to (B \subseteq x \leftrightarrow B \subseteq ⊥ (y))$
45		ineq1	$⊢ x = ⊥ (y) \to x \cap A = ⊥ (y) \cap A$
46	45	oveq1d	$⊢ x = ⊥ (y) \to (x \cap A) \lor_{ℋ} B = (⊥ (y) \cap A) \lor_{ℋ} B$
47		ineq1	$⊢ x = ⊥ (y) \to x \cap (A \lor_{ℋ} B) = ⊥ (y) \cap (A \lor_{ℋ} B)$
48	46 47	eqeq12d	$⊢ x = ⊥ (y) \to ((x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B) \leftrightarrow (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))$
49	44 48	imbi12d	$⊢ x = ⊥ (y) \to ((B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)) \leftrightarrow (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B)))$
50	49	rspccv	$⊢ \forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)) \to (⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B)))$
51		choccl	$⊢ y \in C_{ℋ} \to ⊥ (y) \in C_{ℋ}$
52	51	imim1i	$⊢ (⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))) \to (y \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B)))$
53	52	com12	$⊢ y \in C_{ℋ} \to ((⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))) \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B)))$
54	53	adantl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))) \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B)))$
55		chsscon2	$⊢ (B \in C_{ℋ} \land y \in C_{ℋ}) \to (B \subseteq ⊥ (y) \leftrightarrow y \subseteq ⊥ (B))$
56	55	biimprd	$⊢ (B \in C_{ℋ} \land y \in C_{ℋ}) \to (y \subseteq ⊥ (B) \to B \subseteq ⊥ (y))$
57	56	adantll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (y \subseteq ⊥ (B) \to B \subseteq ⊥ (y))$
58		fveq2	$⊢ (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B) \to ⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = ⊥ (⊥ (y) \cap (A \lor_{ℋ} B))$
59		chincl	$⊢ (⊥ (y) \in C_{ℋ} \land A \in C_{ℋ}) \to ⊥ (y) \cap A \in C_{ℋ}$
60	51 59	sylan	$⊢ (y \in C_{ℋ} \land A \in C_{ℋ}) \to ⊥ (y) \cap A \in C_{ℋ}$
61		chdmj1	$⊢ (⊥ (y) \cap A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = ⊥ (⊥ (y) \cap A) \cap ⊥ (B)$
62	60 61	sylan	$⊢ ((y \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = ⊥ (⊥ (y) \cap A) \cap ⊥ (B)$
63		chdmm2	$⊢ (y \in C_{ℋ} \land A \in C_{ℋ}) \to ⊥ (⊥ (y) \cap A) = y \lor_{ℋ} ⊥ (A)$
64	63	adantr	$⊢ ((y \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ (⊥ (y) \cap A) = y \lor_{ℋ} ⊥ (A)$
65	64	ineq1d	$⊢ ((y \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ (⊥ (y) \cap A) \cap ⊥ (B) = (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)$
66	62 65	eqtrd	$⊢ ((y \in C_{ℋ} \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)$
67	66	anasss	$⊢ (y \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B)$
68		chjcl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} B \in C_{ℋ}$
69		chdmm2	$⊢ (y \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ}) \to ⊥ (⊥ (y) \cap (A \lor_{ℋ} B)) = y \lor_{ℋ} ⊥ (A \lor_{ℋ} B)$
70	68 69	sylan2	$⊢ (y \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ (⊥ (y) \cap (A \lor_{ℋ} B)) = y \lor_{ℋ} ⊥ (A \lor_{ℋ} B)$
71		chdmj1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} B) = ⊥ (A) \cap ⊥ (B)$
72	71	adantl	$⊢ (y \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ (A \lor_{ℋ} B) = ⊥ (A) \cap ⊥ (B)$
73	72	oveq2d	$⊢ (y \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to y \lor_{ℋ} ⊥ (A \lor_{ℋ} B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))$
74	70 73	eqtrd	$⊢ (y \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to ⊥ (⊥ (y) \cap (A \lor_{ℋ} B)) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))$
75	67 74	eqeq12d	$⊢ (y \in C_{ℋ} \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to (⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = ⊥ (⊥ (y) \cap (A \lor_{ℋ} B)) \leftrightarrow (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))$
76	75	ancoms	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (⊥ ((⊥ (y) \cap A) \lor_{ℋ} B) = ⊥ (⊥ (y) \cap (A \lor_{ℋ} B)) \leftrightarrow (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))$
77	58 76	imbitrid	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))$
78	57 77	imim12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B)) \to (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
79	54 78	syld	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))) \to (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
80	79	ex	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (y \in C_{ℋ} \to ((⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))) \to (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))))$
81	80	com23	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((⊥ (y) \in C_{ℋ} \to (B \subseteq ⊥ (y) \to (⊥ (y) \cap A) \lor_{ℋ} B = ⊥ (y) \cap (A \lor_{ℋ} B))) \to (y \in C_{ℋ} \to (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))))$
82	50 81	syl5	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)) \to (y \in C_{ℋ} \to (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B)))))$
83	82	ralrimdv	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)) \to \forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
84	43 83	impbid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))) \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)))$
85		mdbr	$⊢ (⊥ (A) \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to (⊥ (A) 𝑀_{ℋ} ⊥ (B) \leftrightarrow \forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
86	16 26 85	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (A) 𝑀_{ℋ} ⊥ (B) \leftrightarrow \forall y \in C_{ℋ} (y \subseteq ⊥ (B) \to (y \lor_{ℋ} ⊥ (A)) \cap ⊥ (B) = y \lor_{ℋ} (⊥ (A) \cap ⊥ (B))))$
87		dmdbr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)))$
88	84 86 87	3bitr4rd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow ⊥ (A) 𝑀_{ℋ} ⊥ (B))$

Metamath Proof Explorer

Theorem dmdmd

Proof