Step |
Hyp |
Ref |
Expression |
1 |
|
df-plq |
|- +Q = ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) |
2 |
1
|
fveq1i |
|- ( +Q ` <. A , B >. ) = ( ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) |
3 |
2
|
a1i |
|- ( ( A e. Q. /\ B e. Q. ) -> ( +Q ` <. A , B >. ) = ( ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) ) |
4 |
|
opelxpi |
|- ( ( A e. Q. /\ B e. Q. ) -> <. A , B >. e. ( Q. X. Q. ) ) |
5 |
4
|
fvresd |
|- ( ( A e. Q. /\ B e. Q. ) -> ( ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) = ( ( /Q o. +pQ ) ` <. A , B >. ) ) |
6 |
|
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 ) ) >. ) |
7 |
|
opex |
|- <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. _V |
8 |
6 7
|
fnmpoi |
|- +pQ Fn ( ( N. X. N. ) X. ( N. X. N. ) ) |
9 |
|
elpqn |
|- ( A e. Q. -> A e. ( N. X. N. ) ) |
10 |
|
elpqn |
|- ( B e. Q. -> B e. ( N. X. N. ) ) |
11 |
|
opelxpi |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) ) |
12 |
9 10 11
|
syl2an |
|- ( ( A e. Q. /\ B e. Q. ) -> <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) ) |
13 |
|
fvco2 |
|- ( ( +pQ Fn ( ( N. X. N. ) X. ( N. X. N. ) ) /\ <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) ) -> ( ( /Q o. +pQ ) ` <. A , B >. ) = ( /Q ` ( +pQ ` <. A , B >. ) ) ) |
14 |
8 12 13
|
sylancr |
|- ( ( A e. Q. /\ B e. Q. ) -> ( ( /Q o. +pQ ) ` <. A , B >. ) = ( /Q ` ( +pQ ` <. A , B >. ) ) ) |
15 |
3 5 14
|
3eqtrd |
|- ( ( A e. Q. /\ B e. Q. ) -> ( +Q ` <. A , B >. ) = ( /Q ` ( +pQ ` <. A , B >. ) ) ) |
16 |
|
df-ov |
|- ( A +Q B ) = ( +Q ` <. A , B >. ) |
17 |
|
df-ov |
|- ( A +pQ B ) = ( +pQ ` <. A , B >. ) |
18 |
17
|
fveq2i |
|- ( /Q ` ( A +pQ B ) ) = ( /Q ` ( +pQ ` <. A , B >. ) ) |
19 |
15 16 18
|
3eqtr4g |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( /Q ` ( A +pQ B ) ) ) |