Metamath Proof Explorer

Theorem coidmid

Description: A composition that includes the identity relation on the relevant class can be inserted in the middle of a composition. (Contributed by BJ, 8-Nov-2026)

		Ref	Expression
	Assertion	coidmid	$⊢ {I ↾}_{(dom A \cap ran D)} \subseteq B \circ C \to A \circ D \subseteq (A \circ B) \circ (C \circ D)$

Proof

Step	Hyp	Ref	Expression
1		coss2	$⊢ {I ↾}_{(dom A \cap ran D)} \subseteq B \circ C \to A \circ ({I ↾}_{(dom A \cap ran D)}) \subseteq A \circ (B \circ C)$
2		coss1	$⊢ A \circ ({I ↾}_{(dom A \cap ran D)}) \subseteq A \circ (B \circ C) \to (A \circ ({I ↾}_{(dom A \cap ran D)})) \circ D \subseteq (A \circ (B \circ C)) \circ D$
3	1 2	syl	$⊢ {I ↾}_{(dom A \cap ran D)} \subseteq B \circ C \to (A \circ ({I ↾}_{(dom A \cap ran D)})) \circ D \subseteq (A \circ (B \circ C)) \circ D$
4		coires1	$⊢ A \circ ({I ↾}_{(dom A \cap ran D)}) = {A ↾}_{(dom A \cap ran D)}$
5		incom	$⊢ dom A \cap ran D = ran D \cap dom A$
6	5	reseq2i	$⊢ {A ↾}_{(dom A \cap ran D)} = {A ↾}_{(ran D \cap dom A)}$
7		resindm	$⊢ {A ↾}_{(ran D \cap dom A)} = {A ↾}_{ran D}$
8	6 7	eqtri	$⊢ {A ↾}_{(dom A \cap ran D)} = {A ↾}_{ran D}$
9	4 8	eqtri	$⊢ A \circ ({I ↾}_{(dom A \cap ran D)}) = {A ↾}_{ran D}$
10	9	coeq1i	$⊢ (A \circ ({I ↾}_{(dom A \cap ran D)})) \circ D = ({A ↾}_{ran D}) \circ D$
11		coresrn	$⊢ ({A ↾}_{ran D}) \circ D = A \circ D$
12	10 11	eqtri	$⊢ (A \circ ({I ↾}_{(dom A \cap ran D)})) \circ D = A \circ D$
13		coass	$⊢ (A \circ B) \circ C = A \circ (B \circ C)$
14	13	coeq1i	$⊢ ((A \circ B) \circ C) \circ D = (A \circ (B \circ C)) \circ D$
15		coass	$⊢ ((A \circ B) \circ C) \circ D = (A \circ B) \circ (C \circ D)$
16	14 15	eqtr3i	$⊢ (A \circ (B \circ C)) \circ D = (A \circ B) \circ (C \circ D)$
17	3 12 16	3sstr3g	$⊢ {I ↾}_{(dom A \cap ran D)} \subseteq B \circ C \to A \circ D \subseteq (A \circ B) \circ (C \circ D)$