coineq0

Description: A composition ( A o. B ) is disjoint from a class C if and only if B is disjoint from (`' A o. C ) ` . This is a form of the Schroeder rule that does not use complements. See also coeq0 . (Contributed by BJ, 8-Nov-2026)

		Ref	Expression
	Assertion	coineq0	$⊢ (A \circ B) \cap C = \emptyset \leftrightarrow B \cap (A^{-1} \circ C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		incom	$⊢ B \cap (A^{-1} \circ C) = (A^{-1} \circ C) \cap B$
2		cocnvcnv1	$⊢ {A^{-1}}^{-1} \circ B = A \circ B$
3	2	ineq2i	$⊢ C \cap ({A^{-1}}^{-1} \circ B) = C \cap (A \circ B)$
4		incom	$⊢ C \cap (A \circ B) = (A \circ B) \cap C$
5	3 4	eqtri	$⊢ C \cap ({A^{-1}}^{-1} \circ B) = (A \circ B) \cap C$
6		id	$⊢ (A \circ B) \cap C = \emptyset \to (A \circ B) \cap C = \emptyset$
7	5 6	eqtrid	$⊢ (A \circ B) \cap C = \emptyset \to C \cap ({A^{-1}}^{-1} \circ B) = \emptyset$
8		coeq2	$⊢ C \cap ({A^{-1}}^{-1} \circ B) = \emptyset \to (A^{-1} \cap (B \circ C^{-1})) \circ (C \cap ({A^{-1}}^{-1} \circ B)) = (A^{-1} \cap (B \circ C^{-1})) \circ \emptyset$
9		co02	$⊢ (A^{-1} \cap (B \circ C^{-1})) \circ \emptyset = \emptyset$
10	8 9	eqtrdi	$⊢ C \cap ({A^{-1}}^{-1} \circ B) = \emptyset \to (A^{-1} \cap (B \circ C^{-1})) \circ (C \cap ({A^{-1}}^{-1} \circ B)) = \emptyset$
11		comodular	$⊢ (A^{-1} \circ C) \cap B \subseteq (A^{-1} \cap (B \circ C^{-1})) \circ (C \cap ({A^{-1}}^{-1} \circ B))$
12		sseq0	$⊢ ((A^{-1} \circ C) \cap B \subseteq (A^{-1} \cap (B \circ C^{-1})) \circ (C \cap ({A^{-1}}^{-1} \circ B)) \land (A^{-1} \cap (B \circ C^{-1})) \circ (C \cap ({A^{-1}}^{-1} \circ B)) = \emptyset) \to (A^{-1} \circ C) \cap B = \emptyset$
13	11 12	mpan	$⊢ (A^{-1} \cap (B \circ C^{-1})) \circ (C \cap ({A^{-1}}^{-1} \circ B)) = \emptyset \to (A^{-1} \circ C) \cap B = \emptyset$
14	10 13	syl	$⊢ C \cap ({A^{-1}}^{-1} \circ B) = \emptyset \to (A^{-1} \circ C) \cap B = \emptyset$
15	7 14	syl	$⊢ (A \circ B) \cap C = \emptyset \to (A^{-1} \circ C) \cap B = \emptyset$
16	1 15	eqtrid	$⊢ (A \circ B) \cap C = \emptyset \to B \cap (A^{-1} \circ C) = \emptyset$
17		coeq2	$⊢ B \cap (A^{-1} \circ C) = \emptyset \to (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)) = (A \cap (C \circ B^{-1})) \circ \emptyset$
18		co02	$⊢ (A \cap (C \circ B^{-1})) \circ \emptyset = \emptyset$
19	17 18	eqtrdi	$⊢ B \cap (A^{-1} \circ C) = \emptyset \to (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)) = \emptyset$
20		comodular	$⊢ (A \circ B) \cap C \subseteq (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C))$
21		sseq0	$⊢ ((A \circ B) \cap C \subseteq (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)) \land (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)) = \emptyset) \to (A \circ B) \cap C = \emptyset$
22	20 21	mpan	$⊢ (A \cap (C \circ B^{-1})) \circ (B \cap (A^{-1} \circ C)) = \emptyset \to (A \circ B) \cap C = \emptyset$
23	19 22	syl	$⊢ B \cap (A^{-1} \circ C) = \emptyset \to (A \circ B) \cap C = \emptyset$
24	16 23	impbii	$⊢ (A \circ B) \cap C = \emptyset \leftrightarrow B \cap (A^{-1} \circ C) = \emptyset$

Metamath Proof Explorer

Theorem coineq0

Proof