Theorem pprodcnveq

Description: A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014)

	Ref	Expression
Assertion	pprodcnveq	$$⊢pprod\left(R,S\right)={pprod\left(R^{-1},S^{-1}\right)}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		dfpprod2	$$⊢pprod\left(R,S\right)=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$
2		dfpprod2	$$⊢pprod\left(R^{-1},S^{-1}\right)=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$
3	2	cnveqi	$$⊢{pprod\left(R^{-1},S^{-1}\right)}^{-1}={\left(\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\right)}^{-1}$$
4		cnvin	$$⊢{\left(\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\right)}^{-1}={\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}\cap {\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}$$
5		cnvco1	$$⊢{\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}={\left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)}^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
6		cnvco1	$$⊢{\left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)}^{-1}={\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R$$
7	6	coeq1i	$$⊢{\left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)}^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
8		coass	$$⊢\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)={\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)$$
9	5 7 8	3eqtri	$$⊢{\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}={\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)$$
10		cnvco1	$$⊢{\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}={\left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)}^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
11		cnvco1	$$⊢{\left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)}^{-1}={\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S$$
12	11	coeq1i	$$⊢{\left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)}^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)=\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
13		coass	$$⊢\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)={\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)$$
14	10 12 13	3eqtri	$$⊢{\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}={\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)$$
15	9 14	ineq12i	$$⊢{\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R^{-1}\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}\cap {\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S^{-1}\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)}^{-1}=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$
16	3 4 15	3eqtri	$$⊢{pprod\left(R^{-1},S^{-1}\right)}^{-1}=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(R\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left(S\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$
17	1 16	eqtr4i	$$⊢pprod\left(R,S\right)={pprod\left(R^{-1},S^{-1}\right)}^{-1}$$