Theorem rncoeq

Description: Range of a composition. (Contributed by NM, 19-Mar-1998)

	Ref	Expression
Assertion	rncoeq	$$⊢\mathrm{dom}A=\mathrm{ran}B\to \mathrm{ran}\left(A\circ B\right)=\mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		dmcoeq	$$⊢\mathrm{dom}{B}^{-1}=\mathrm{ran}{A}^{-1}\to \mathrm{dom}\left(B^{-1}\circ A^{-1}\right)=\mathrm{dom}{A}^{-1}$$
2		eqcom	$$⊢\mathrm{dom}A=\mathrm{ran}B\leftrightarrow \mathrm{ran}B=\mathrm{dom}A$$
3		df-rn	$$⊢\mathrm{ran}B=\mathrm{dom}{B}^{-1}$$
4		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
5	3 4	eqeq12i	$$⊢\mathrm{ran}B=\mathrm{dom}A\leftrightarrow \mathrm{dom}{B}^{-1}=\mathrm{ran}{A}^{-1}$$
6	2 5	bitri	$$⊢\mathrm{dom}A=\mathrm{ran}B\leftrightarrow \mathrm{dom}{B}^{-1}=\mathrm{ran}{A}^{-1}$$
7		df-rn	$$⊢\mathrm{ran}\left(A\circ B\right)=\mathrm{dom}{\left(A\circ B\right)}^{-1}$$
8		cnvco	$$⊢{\left(A\circ B\right)}^{-1}=B^{-1}\circ A^{-1}$$
9	8	dmeqi	$$⊢\mathrm{dom}{\left(A\circ B\right)}^{-1}=\mathrm{dom}\left(B^{-1}\circ A^{-1}\right)$$
10	7 9	eqtri	$$⊢\mathrm{ran}\left(A\circ B\right)=\mathrm{dom}\left(B^{-1}\circ A^{-1}\right)$$
11		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
12	10 11	eqeq12i	$$⊢\mathrm{ran}\left(A\circ B\right)=\mathrm{ran}A\leftrightarrow \mathrm{dom}\left(B^{-1}\circ A^{-1}\right)=\mathrm{dom}{A}^{-1}$$
13	1 6 12	3imtr4i	$$⊢\mathrm{dom}A=\mathrm{ran}B\to \mathrm{ran}\left(A\circ B\right)=\mathrm{ran}A$$