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

Theorem islmhm 16104
 Description: Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
Hypotheses
Ref Expression
islmhm.k Scalar
islmhm.l Scalar
islmhm.b
islmhm.e
islmhm.m
islmhm.n
Assertion
Ref Expression
islmhm LMHom
Distinct variable groups:   ,   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,)   ()   (,)   (,)

Proof of Theorem islmhm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-lmhm 16099 . . 3 LMHom Scalar Scalar
21elmpt2cl 6289 . 2 LMHom
3 oveq12 6091 . . . . . 6
4 fvex 5743 . . . . . . . 8 Scalar
54a1i 11 . . . . . . 7 Scalar
6 simplr 733 . . . . . . . . . . 11 Scalar
76fveq2d 5733 . . . . . . . . . 10 Scalar Scalar Scalar
8 islmhm.l . . . . . . . . . 10 Scalar
97, 8syl6eqr 2487 . . . . . . . . 9 Scalar Scalar
10 simpr 449 . . . . . . . . . . 11 Scalar Scalar
11 simpll 732 . . . . . . . . . . . 12 Scalar
1211fveq2d 5733 . . . . . . . . . . 11 Scalar Scalar Scalar
1310, 12eqtrd 2469 . . . . . . . . . 10 Scalar Scalar
14 islmhm.k . . . . . . . . . 10 Scalar
1513, 14syl6eqr 2487 . . . . . . . . 9 Scalar
169, 15eqeq12d 2451 . . . . . . . 8 Scalar Scalar
1715fveq2d 5733 . . . . . . . . . 10 Scalar
18 islmhm.b . . . . . . . . . 10
1917, 18syl6eqr 2487 . . . . . . . . 9 Scalar
2011fveq2d 5733 . . . . . . . . . . 11 Scalar
21 islmhm.e . . . . . . . . . . 11
2220, 21syl6eqr 2487 . . . . . . . . . 10 Scalar
2311fveq2d 5733 . . . . . . . . . . . . . 14 Scalar
24 islmhm.m . . . . . . . . . . . . . 14
2523, 24syl6eqr 2487 . . . . . . . . . . . . 13 Scalar
2625oveqd 6099 . . . . . . . . . . . 12 Scalar
2726fveq2d 5733 . . . . . . . . . . 11 Scalar
286fveq2d 5733 . . . . . . . . . . . . 13 Scalar
29 islmhm.n . . . . . . . . . . . . 13
3028, 29syl6eqr 2487 . . . . . . . . . . . 12 Scalar
3130oveqd 6099 . . . . . . . . . . 11 Scalar
3227, 31eqeq12d 2451 . . . . . . . . . 10 Scalar
3322, 32raleqbidv 2917 . . . . . . . . 9 Scalar
3419, 33raleqbidv 2917 . . . . . . . 8 Scalar
3516, 34anbi12d 693 . . . . . . 7 Scalar Scalar
365, 35sbcied 3198 . . . . . 6 Scalar Scalar
373, 36rabeqbidv 2952 . . . . 5 Scalar Scalar
38 ovex 6107 . . . . . 6
3938rabex 4355 . . . . 5
4037, 1, 39ovmpt2a 6205 . . . 4 LMHom
4140eleq2d 2504 . . 3 LMHom
42 fveq1 5728 . . . . . . . 8
43 fveq1 5728 . . . . . . . . 9
4443oveq2d 6098 . . . . . . . 8
4542, 44eqeq12d 2451 . . . . . . 7
46452ralbidv 2748 . . . . . 6
4746anbi2d 686 . . . . 5
4847elrab 3093 . . . 4
49 3anass 941 . . . 4
5048, 49bitr4i 245 . . 3
5141, 50syl6bb 254 . 2 LMHom