Metamath Proof Explorer


Theorem dfpprod2

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

Ref Expression
Assertion 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

Step Hyp Ref Expression
1 df-pprod
 |-  pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
2 df-txp
 |-  ( ( 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
 |-  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 ) ) ) ) )