This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pprodcnveq

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

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

Proof

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