comodular

Description: A strong modular law for the composition of relations. The modular law is an axiom defining allegories. (Contributed by BJ, 7-Nov-2026)

		Ref	Expression
	Assertion	comodular	$⊢ (A \circ B) \cap C \subseteq (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))$

Proof

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel (A \circ B)$
2		relin1	$⊢ Rel (A \circ B) \to Rel ((A \circ B) \cap C)$
3	1 2	ax-mp	$⊢ Rel ((A \circ B) \cap C)$
4		brin	$⊢ x ((A \circ B) \cap C) y \leftrightarrow (x (A \circ B) y \land x C y)$
5		vex	$⊢ x \in V$
6		vex	$⊢ y \in V$
7	5 6	brco	$⊢ x (A \circ B) y \leftrightarrow \exists z (x B z \land z A y)$
8		simprl	$⊢ (x C y \land (x B z \land z A y)) \to x B z$
9		simpl	$⊢ (x C y \land (x B z \land z A y)) \to x C y$
10		simprr	$⊢ (x C y \land (x B z \land z A y)) \to z A y$
11		vex	$⊢ z \in V$
12	6 11	brcnv	$⊢ y A^{-1} z \leftrightarrow z A y$
13	10 12	sylibr	$⊢ (x C y \land (x B z \land z A y)) \to y A^{-1} z$
14	5 6 11	brcoi	$⊢ (x C y \land y A^{-1} z) \to x (A^{-1} \circ C) z$
15	9 13 14	syl2anc	$⊢ (x C y \land (x B z \land z A y)) \to x (A^{-1} \circ C) z$
16		brin	$⊢ x (B \cap (A^{-1} \circ C)) z \leftrightarrow (x B z \land x (A^{-1} \circ C) z)$
17	8 15 16	sylanbrc	$⊢ (x C y \land (x B z \land z A y)) \to x (B \cap (A^{-1} \circ C)) z$
18	11 5	brcnv	$⊢ z B^{-1} x \leftrightarrow x B z$
19	8 18	sylibr	$⊢ (x C y \land (x B z \land z A y)) \to z B^{-1} x$
20	11 5 6	brcoi	$⊢ (z B^{-1} x \land x C y) \to z (C \circ B^{-1}) y$
21	19 9 20	syl2anc	$⊢ (x C y \land (x B z \land z A y)) \to z (C \circ B^{-1}) y$
22		brin	$⊢ z (A \cap (C \circ B^{-1})) y \leftrightarrow (z A y \land z (C \circ B^{-1}) y)$
23	10 21 22	sylanbrc	$⊢ (x C y \land (x B z \land z A y)) \to z (A \cap (C \circ B^{-1})) y$
24	5 11 6	brcoi	$⊢ (x (B \cap (A^{-1} \circ C)) z \land z (A \cap (C \circ B^{-1})) y) \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y$
25	17 23 24	syl2anc	$⊢ (x C y \land (x B z \land z A y)) \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y$
26	25	ex	$⊢ x C y \to ((x B z \land z A y) \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y)$
27	26	exlimdv	$⊢ x C y \to (\exists z (x B z \land z A y) \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y)$
28	7 27	biimtrid	$⊢ x C y \to (x (A \circ B) y \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y)$
29	28	impcom	$⊢ (x (A \circ B) y \land x C y) \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y$
30	4 29	sylbi	$⊢ x ((A \circ B) \cap C) y \to x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y$
31		df-br	$⊢ x ((A \circ B) \cap C) y \leftrightarrow ⟨x, y⟩ \in ((A \circ B) \cap C)$
32		df-br	$⊢ x ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))) y \leftrightarrow ⟨x, y⟩ \in ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)))$
33	30 31 32	3imtr3i	$⊢ ⟨x, y⟩ \in ((A \circ B) \cap C) \to ⟨x, y⟩ \in ((A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)))$
34	3 33	relssi	$⊢ (A \circ B) \cap C \subseteq (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))$

Metamath Proof Explorer

Theorem comodular

Proof