Theorem dfpprod2 31989

Description: Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.)

Assertion

Ref	Expression
dfpprod2	|- pprod ( A , B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( A o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( B o. ( 2nd |` ( _V X. _V ) ) ) ) )

Proof of Theorem dfpprod2

Step	Hyp	Ref	Expression
1		df-pprod 31962	. 2 |- pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
2		df-txp 31961	. 2 |- ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( A o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( B o. ( 2nd |` ( _V X. _V ) ) ) ) )
3	1, 2	eqtri 2644	1 |- pprod ( A , B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( A o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( B o. ( 2nd |` ( _V X. _V ) ) ) ) )

Syntax hints:   = wceq 1483   _Vcvv 3200   i^i cin 3573   X. cxp 5112   `'ccnv 5113   |` cres 5116   o. ccom 5118   1stc1st 7166   2ndc2nd 7167   (x) ctxp 31937  pprodcpprod 31938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-txp 31961  df-pprod 31962

This theorem is referenced by:  pprodcnveq  31990