Metamath Proof Explorer


Theorem dvhvaddval

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013)

Ref Expression
Hypothesis dvhvaddval.a + ˙ = f T × E , g T × E 1 st f 1 st g 2 nd f ˙ 2 nd g
Assertion dvhvaddval F T × E G T × E F + ˙ G = 1 st F 1 st G 2 nd F ˙ 2 nd G

Proof

Step Hyp Ref Expression
1 dvhvaddval.a + ˙ = f T × E , g T × E 1 st f 1 st g 2 nd f ˙ 2 nd g
2 fveq2 h = F 1 st h = 1 st F
3 2 coeq1d h = F 1 st h 1 st i = 1 st F 1 st i
4 fveq2 h = F 2 nd h = 2 nd F
5 4 oveq1d h = F 2 nd h ˙ 2 nd i = 2 nd F ˙ 2 nd i
6 3 5 opeq12d h = F 1 st h 1 st i 2 nd h ˙ 2 nd i = 1 st F 1 st i 2 nd F ˙ 2 nd i
7 fveq2 i = G 1 st i = 1 st G
8 7 coeq2d i = G 1 st F 1 st i = 1 st F 1 st G
9 fveq2 i = G 2 nd i = 2 nd G
10 9 oveq2d i = G 2 nd F ˙ 2 nd i = 2 nd F ˙ 2 nd G
11 8 10 opeq12d i = G 1 st F 1 st i 2 nd F ˙ 2 nd i = 1 st F 1 st G 2 nd F ˙ 2 nd G
12 1 dvhvaddcbv + ˙ = h T × E , i T × E 1 st h 1 st i 2 nd h ˙ 2 nd i
13 opex 1 st F 1 st G 2 nd F ˙ 2 nd G V
14 6 11 12 13 ovmpo F T × E G T × E F + ˙ G = 1 st F 1 st G 2 nd F ˙ 2 nd G