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

Theorem mulmulvec 25790
 Description: Connection between multiplication of complex numbers and scalar multiplication. (Contributed by FL, 29-May-2014.)
Hypothesis
Ref Expression
mulone.1
Assertion
Ref Expression
mulmulvec

Proof of Theorem mulmulvec
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . . . . . 7
2 ovex 5899 . . . . . . 7
3 eqid 2296 . . . . . . . 8
43fvmpt2 5624 . . . . . . 7
51, 2, 4sylancl 643 . . . . . 6
65eqcomd 2301 . . . . 5
76oveq2d 5890 . . . 4
8 simpl2 959 . . . . 5
9 simpl3l 1010 . . . . 5
10 elmapi 6808 . . . . . . . 8
1110adantl 452 . . . . . . 7
12113ad2ant3 978 . . . . . 6
13 ffvelrn 5679 . . . . . 6
1412, 13sylan 457 . . . . 5
158, 9, 14mulassd 8874 . . . 4
16 simpl1 958 . . . . . . 7
17 simpl3r 1011 . . . . . . 7
18 mulone.1 . . . . . . . 8
1918ismulcv 25784 . . . . . . 7
2016, 9, 17, 19syl3anc 1182 . . . . . 6
2120fveq1d 5543 . . . . 5
2221oveq2d 5890 . . . 4
237, 15, 223eqtr4d 2338 . . 3
2423mpteq2dva 4122 . 2
25 simp1 955 . . 3
26 mulcl 8837 . . . . 5
2726adantrr 697 . . . 4