Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isaddrv Unicode version

 Description: Addition of complex vectors. Experimental. (Contributed by FL, 14-Sep-2013.)
Hypothesis
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isaddrv.1 . . . . 5
2 oveq2 5866 . . . . . . . 8
32oveq2d 5874 . . . . . . 7
4 eqidd 2284 . . . . . . . 8
52, 4mpteq12dv 4098 . . . . . . 7
63, 3, 5mpt2eq123dv 5910 . . . . . 6
7 df-addcv 25645 . . . . . 6
8 ovex 5883 . . . . . . 7
98, 8mpt2ex 6198 . . . . . 6
106, 7, 9fvmpt 5602 . . . . 5
111, 10syl5eq 2327 . . . 4
1312oveqd 5875 . 2
14 fveq1 5524 . . . . . 6
1514oveq1d 5873 . . . . 5
1615mpteq2dv 4107 . . . 4
17 fveq1 5524 . . . . . 6
1817oveq2d 5874 . . . . 5
1918mpteq2dv 4107 . . . 4
20 eqid 2283 . . . 4
21 ovex 5883 . . . . 5
2221mptex 5746 . . . 4
2316, 19, 20, 22ovmpt2 5983 . . 3