Step |
Hyp |
Ref |
Expression |
1 |
|
dvhopadd.a |
|- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. ) |
2 |
|
opelxpi |
|- ( ( F e. T /\ U e. E ) -> <. F , U >. e. ( T X. E ) ) |
3 |
|
opelxpi |
|- ( ( G e. T /\ V e. E ) -> <. G , V >. e. ( T X. E ) ) |
4 |
1
|
dvhvaddval |
|- ( ( <. F , U >. e. ( T X. E ) /\ <. G , V >. e. ( T X. E ) ) -> ( <. F , U >. A <. G , V >. ) = <. ( ( 1st ` <. F , U >. ) o. ( 1st ` <. G , V >. ) ) , ( ( 2nd ` <. F , U >. ) P ( 2nd ` <. G , V >. ) ) >. ) |
5 |
2 3 4
|
syl2an |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( <. F , U >. A <. G , V >. ) = <. ( ( 1st ` <. F , U >. ) o. ( 1st ` <. G , V >. ) ) , ( ( 2nd ` <. F , U >. ) P ( 2nd ` <. G , V >. ) ) >. ) |
6 |
|
op1stg |
|- ( ( F e. T /\ U e. E ) -> ( 1st ` <. F , U >. ) = F ) |
7 |
6
|
adantr |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( 1st ` <. F , U >. ) = F ) |
8 |
|
op1stg |
|- ( ( G e. T /\ V e. E ) -> ( 1st ` <. G , V >. ) = G ) |
9 |
8
|
adantl |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( 1st ` <. G , V >. ) = G ) |
10 |
7 9
|
coeq12d |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( ( 1st ` <. F , U >. ) o. ( 1st ` <. G , V >. ) ) = ( F o. G ) ) |
11 |
|
op2ndg |
|- ( ( F e. T /\ U e. E ) -> ( 2nd ` <. F , U >. ) = U ) |
12 |
|
op2ndg |
|- ( ( G e. T /\ V e. E ) -> ( 2nd ` <. G , V >. ) = V ) |
13 |
11 12
|
oveqan12d |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( ( 2nd ` <. F , U >. ) P ( 2nd ` <. G , V >. ) ) = ( U P V ) ) |
14 |
10 13
|
opeq12d |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> <. ( ( 1st ` <. F , U >. ) o. ( 1st ` <. G , V >. ) ) , ( ( 2nd ` <. F , U >. ) P ( 2nd ` <. G , V >. ) ) >. = <. ( F o. G ) , ( U P V ) >. ) |
15 |
5 14
|
eqtrd |
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( <. F , U >. A <. G , V >. ) = <. ( F o. G ) , ( U P V ) >. ) |