coires1

Description: Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011) (Revised by Stefan O'Rear, 7-Mar-2015)

		Ref	Expression
	Assertion	coires1	$⊢ A \circ ({I ↾}_{B}) = {A ↾}_{B}$

Step	Hyp	Ref	Expression
1		cocnvcnv1	$⊢ {A^{-1}}^{-1} \circ I = A \circ I$
2		relcnv	$⊢ Rel {A^{-1}}^{-1}$
3		coi1	$⊢ Rel {A^{-1}}^{-1} \to {A^{-1}}^{-1} \circ I = {A^{-1}}^{-1}$
4	2 3	ax-mp	$⊢ {A^{-1}}^{-1} \circ I = {A^{-1}}^{-1}$
5	1 4	eqtr3i	$⊢ A \circ I = {A^{-1}}^{-1}$
6	5	reseq1i	$⊢ {(A \circ I) ↾}_{B} = {{A^{-1}}^{-1} ↾}_{B}$
7		resco	$⊢ {(A \circ I) ↾}_{B} = A \circ ({I ↾}_{B})$
8	6 7	eqtr3i	$⊢ {{A^{-1}}^{-1} ↾}_{B} = A \circ ({I ↾}_{B})$
9		rescnvcnv	$⊢ {{A^{-1}}^{-1} ↾}_{B} = {A ↾}_{B}$
10	8 9	eqtr3i	$⊢ A \circ ({I ↾}_{B}) = {A ↾}_{B}$

Metamath Proof Explorer