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 ∈ T × E , g ∈ T × E ⟼ 1 st ⁡ f ∘ 1 st ⁡ g 2 nd ⁡ f P 2 nd ⁡ g
Assertion dvhopaddN ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → F U A G V = F ∘ G U P V

Proof

Step Hyp Ref Expression
1 dvhopadd.a ⊢ A = f ∈ T × E , g ∈ T × E ⟼ 1 st ⁡ f ∘ 1 st ⁡ g 2 nd ⁡ f P 2 nd ⁡ g
2 opelxpi ⊢ F ∈ T ∧ U ∈ E → F U ∈ T × E
3 opelxpi ⊢ G ∈ T ∧ V ∈ E → G V ∈ T × E
4 1 dvhvaddval ⊢ F U ∈ T × E ∧ G V ∈ T × E → F U A G V = 1 st ⁡ F U ∘ 1 st ⁡ G V 2 nd ⁡ F U P 2 nd ⁡ G V
5 2 3 4 syl2an ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → F U A G V = 1 st ⁡ F U ∘ 1 st ⁡ G V 2 nd ⁡ F U P 2 nd ⁡ G V
6 op1stg ⊢ F ∈ T ∧ U ∈ E → 1 st ⁡ F U = F
7 6 adantr ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → 1 st ⁡ F U = F
8 op1stg ⊢ G ∈ T ∧ V ∈ E → 1 st ⁡ G V = G
9 8 adantl ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → 1 st ⁡ G V = G
10 7 9 coeq12d ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → 1 st ⁡ F U ∘ 1 st ⁡ G V = F ∘ G
11 op2ndg ⊢ F ∈ T ∧ U ∈ E → 2 nd ⁡ F U = U
12 op2ndg ⊢ G ∈ T ∧ V ∈ E → 2 nd ⁡ G V = V
13 11 12 oveqan12d ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → 2 nd ⁡ F U P 2 nd ⁡ G V = U P V
14 10 13 opeq12d ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → 1 st ⁡ F U ∘ 1 st ⁡ G V 2 nd ⁡ F U P 2 nd ⁡ G V = F ∘ G U P V
15 5 14 eqtrd ⊢ F ∈ T ∧ U ∈ E ∧ G ∈ T ∧ V ∈ E → F U A G V = F ∘ G U P V