Step |
Hyp |
Ref |
Expression |
1 |
|
xp1st |
|- ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. ) |
2 |
|
xp1st |
|- ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. ) |
3 |
|
mulclpi |
|- ( ( ( 1st ` x ) e. N. /\ ( 1st ` y ) e. N. ) -> ( ( 1st ` x ) .N ( 1st ` y ) ) e. N. ) |
4 |
1 2 3
|
syl2an |
|- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 1st ` x ) .N ( 1st ` y ) ) e. N. ) |
5 |
|
xp2nd |
|- ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. ) |
6 |
|
xp2nd |
|- ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. ) |
7 |
|
mulclpi |
|- ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) e. N. ) |
8 |
5 6 7
|
syl2an |
|- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) e. N. ) |
9 |
4 8
|
opelxpd |
|- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) ) |
10 |
9
|
rgen2 |
|- A. x e. ( N. X. N. ) A. y e. ( N. X. N. ) <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) |
11 |
|
df-mpq |
|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. ) |
12 |
11
|
fmpo |
|- ( A. x e. ( N. X. N. ) A. y e. ( N. X. N. ) <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) <-> .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) ) |
13 |
10 12
|
mpbi |
|- .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) |