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

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