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 ) |