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