Metamath Proof Explorer


Theorem dvhopaddN

Description: Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis dvhopadd.a
|- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. )
Assertion dvhopaddN
|- ( ( ( F e. T /\ U e. E ) /\ ( G e. T /\ V e. E ) ) -> ( <. F , U >. A <. G , V >. ) = <. ( F o. G ) , ( U P V ) >. )

Proof

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