Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvhvaddcomN Structured version   Visualization 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 459 . . . 4
2 xp1st 6823 . . . . 5
32ad2antrl 734 . . . 4
4 xp1st 6823 . . . . 5
54ad2antll 735 . . . 4
6 dvhvaddcl.h . . . . 5
7 dvhvaddcl.t . . . . 5
86, 7ltrncom 34305 . . . 4
91, 3, 5, 8syl3anc 1268 . . 3
10 xp2nd 6824 . . . . . 6
11 xp2nd 6824 . . . . . 6
1210, 11anim12i 570 . . . . 5
13 dvhvaddcl.e . . . . . . 7
14 eqid 2451 . . . . . . 7
156, 7, 13, 14tendoplcom 34349 . . . . . 6
16153expb 1209 . . . . 5
1712, 16sylan2 477 . . . 4
18 dvhvaddcl.u . . . . . . 7
19 dvhvaddcl.d . . . . . . 7 Scalar
20 dvhvaddcl.p . . . . . . 7
216, 7, 13, 18, 19, 14, 20dvhfplusr 34652 . . . . . 6
2221adantr 467 . . . . 5
2322oveqd 6307 . . . 4
2422oveqd 6307 . . . 4
2517, 23, 243eqtr4d 2495 . . 3
269, 25opeq12d 4174 . 2