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 , `' S )

Proof

Step	Hyp	Ref	Expression
1		dfpprod2	\|- pprod ( R , S ) = ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( S o. ( 2nd \|` ( _V X. _V ) ) ) ) )
2		dfpprod2	\|- pprod ( `' R , `' S ) = ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) )
3	2	cnveqi	\|- `' pprod ( `' R , `' S ) = `' ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) )
4		cnvin	\|- `' ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) ) = ( `' ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i `' ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) )
5		cnvco1	\|- `' ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) = ( `' ( `' R o. ( 1st \|` ( _V X. _V ) ) ) o. ( 1st \|` ( _V X. _V ) ) )
6		cnvco1	\|- `' ( `' R o. ( 1st \|` ( _V X. _V ) ) ) = ( `' ( 1st \|` ( _V X. _V ) ) o. R )
7	6	coeq1i	\|- ( `' ( `' R o. ( 1st \|` ( _V X. _V ) ) ) o. ( 1st \|` ( _V X. _V ) ) ) = ( ( `' ( 1st \|` ( _V X. _V ) ) o. R ) o. ( 1st \|` ( _V X. _V ) ) )
8		coass	\|- ( ( `' ( 1st \|` ( _V X. _V ) ) o. R ) o. ( 1st \|` ( _V X. _V ) ) ) = ( `' ( 1st \|` ( _V X. _V ) ) o. ( R o. ( 1st \|` ( _V X. _V ) ) ) )
9	5 7 8	3eqtri	\|- `' ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) = ( `' ( 1st \|` ( _V X. _V ) ) o. ( R o. ( 1st \|` ( _V X. _V ) ) ) )
10		cnvco1	\|- `' ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) = ( `' ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) o. ( 2nd \|` ( _V X. _V ) ) )
11		cnvco1	\|- `' ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) = ( `' ( 2nd \|` ( _V X. _V ) ) o. S )
12	11	coeq1i	\|- ( `' ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) o. ( 2nd \|` ( _V X. _V ) ) ) = ( ( `' ( 2nd \|` ( _V X. _V ) ) o. S ) o. ( 2nd \|` ( _V X. _V ) ) )
13		coass	\|- ( ( `' ( 2nd \|` ( _V X. _V ) ) o. S ) o. ( 2nd \|` ( _V X. _V ) ) ) = ( `' ( 2nd \|` ( _V X. _V ) ) o. ( S o. ( 2nd \|` ( _V X. _V ) ) ) )
14	10 12 13	3eqtri	\|- `' ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) = ( `' ( 2nd \|` ( _V X. _V ) ) o. ( S o. ( 2nd \|` ( _V X. _V ) ) ) )
15	9 14	ineq12i	\|- ( `' ( `' ( 1st \|` ( _V X. _V ) ) o. ( `' R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i `' ( `' ( 2nd \|` ( _V X. _V ) ) o. ( `' S o. ( 2nd \|` ( _V X. _V ) ) ) ) ) = ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( S o. ( 2nd \|` ( _V X. _V ) ) ) ) )
16	3 4 15	3eqtri	\|- `' pprod ( `' R , `' S ) = ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( R o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( S o. ( 2nd \|` ( _V X. _V ) ) ) ) )
17	1 16	eqtr4i	\|- pprod ( R , S ) = `' pprod ( `' R , `' S )