Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvhvaddcomN Structured version   Unicode version

 Description: Commutativity of vector sum. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 444 . . . 4
2 xp1st 6376 . . . . 5
32ad2antrl 709 . . . 4
4 xp1st 6376 . . . . 5
54ad2antll 710 . . . 4
6 dvhvaddcl.h . . . . 5
7 dvhvaddcl.t . . . . 5
86, 7ltrncom 31535 . . . 4
91, 3, 5, 8syl3anc 1184 . . 3
10 xp2nd 6377 . . . . . 6
11 xp2nd 6377 . . . . . 6
1210, 11anim12i 550 . . . . 5
13 dvhvaddcl.e . . . . . . 7
14 eqid 2436 . . . . . . 7
156, 7, 13, 14tendoplcom 31579 . . . . . 6
16153expb 1154 . . . . 5
1712, 16sylan2 461 . . . 4
18 dvhvaddcl.u . . . . . . 7
19 dvhvaddcl.d . . . . . . 7 Scalar
20 dvhvaddcl.p . . . . . . 7
216, 7, 13, 18, 19, 14, 20dvhfplusr 31882 . . . . . 6
2221adantr 452 . . . . 5
2322oveqd 6098 . . . 4
2422oveqd 6098 . . . 4
2517, 23, 243eqtr4d 2478 . . 3
269, 25opeq12d 3992 . 2