Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lnomul Unicode version

Theorem lnomul 21354
 Description: Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
lnomul.1
lnomul.5
lnomul.6
lnomul.7
Assertion
Ref Expression
lnomul

Proof of Theorem lnomul
StepHypRef Expression
1 simpl 443 . . 3
2 simprl 732 . . 3
3 simprr 733 . . 3
4 simpl1 958 . . . 4
5 lnomul.1 . . . . 5
6 eqid 2296 . . . . 5
75, 6nvzcl 21208 . . . 4
84, 7syl 15 . . 3
9 eqid 2296 . . . 4
10 eqid 2296 . . . 4
11 eqid 2296 . . . 4
12 lnomul.5 . . . 4
13 lnomul.6 . . . 4
14 lnomul.7 . . . 4
155, 9, 10, 11, 12, 13, 14lnolin 21348 . . 3
161, 2, 3, 8, 15syl13anc 1184 . 2
175, 12nvscl 21200 . . . . 5
184, 2, 3, 17syl3anc 1182 . . . 4
195, 10, 6nv0rid 21209 . . . 4
204, 18, 19syl2anc 642 . . 3
2120fveq2d 5545 . 2
22 eqid 2296 . . . . . 6
235, 9, 6, 22, 14lno0 21350 . . . . 5
2423oveq2d 5890 . . . 4