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	⊢ 𝐴 = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) 𝑃 ( 2nd ‘ 𝑔 ) ) ⟩ )
Assertion	dvhopaddN	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑈 ⟩ 𝐴 ⟨ 𝐺 , 𝑉 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑈 𝑃 𝑉 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		dvhopadd.a	⊢ 𝐴 = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) 𝑃 ( 2nd ‘ 𝑔 ) ) ⟩ )
2		opelxpi	⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ⟨ 𝐹 , 𝑈 ⟩ ∈ ( 𝑇 × 𝐸 ) )
3		opelxpi	⊢ ( ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) → ⟨ 𝐺 , 𝑉 ⟩ ∈ ( 𝑇 × 𝐸 ) )
4	1	dvhvaddval	⊢ ( ( ⟨ 𝐹 , 𝑈 ⟩ ∈ ( 𝑇 × 𝐸 ) ∧ ⟨ 𝐺 , 𝑉 ⟩ ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ 𝐹 , 𝑈 ⟩ 𝐴 ⟨ 𝐺 , 𝑉 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) 𝑃 ( 2nd ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) ⟩ )
5	2 3 4	syl2an	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑈 ⟩ 𝐴 ⟨ 𝐺 , 𝑉 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) 𝑃 ( 2nd ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) ⟩ )
6		op1stg	⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) = 𝐹 )
7	6	adantr	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) = 𝐹 )
8		op1stg	⊢ ( ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) → ( 1st ‘ ⟨ 𝐺 , 𝑉 ⟩ ) = 𝐺 )
9	8	adantl	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( 1st ‘ ⟨ 𝐺 , 𝑉 ⟩ ) = 𝐺 )
10	7 9	coeq12d	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) = ( 𝐹 ∘ 𝐺 ) )
11		op2ndg	⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) = 𝑈 )
12		op2ndg	⊢ ( ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) → ( 2nd ‘ ⟨ 𝐺 , 𝑉 ⟩ ) = 𝑉 )
13	11 12	oveqan12d	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) 𝑃 ( 2nd ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) = ( 𝑈 𝑃 𝑉 ) )
14	10 13	opeq12d	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) 𝑃 ( 2nd ‘ ⟨ 𝐺 , 𝑉 ⟩ ) ) ⟩ = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑈 𝑃 𝑉 ) ⟩ )
15	5 14	eqtrd	⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑈 ⟩ 𝐴 ⟨ 𝐺 , 𝑉 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑈 𝑃 𝑉 ) ⟩ )