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

Theorem 0lmhm 16154
 Description: The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Hypotheses
Ref Expression
0lmhm.z
0lmhm.b
0lmhm.s Scalar
0lmhm.t Scalar
Assertion
Ref Expression
0lmhm LMHom

Proof of Theorem 0lmhm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0lmhm.b . 2
2 eqid 2443 . 2
3 eqid 2443 . 2
4 0lmhm.s . 2 Scalar
5 0lmhm.t . 2 Scalar
6 eqid 2443 . 2
7 simp1 958 . 2
8 simp2 959 . 2
9 simp3 960 . . 3
109eqcomd 2448 . 2
11 lmodgrp 15995 . . . 4
12 lmodgrp 15995 . . . 4
13 0lmhm.z . . . . 5
1413, 10ghm 15058 . . . 4
1511, 12, 14syl2an 465 . . 3
17 simpl2 962 . . . 4
18 simprl 734 . . . . 5
19 simpl3 963 . . . . . 6
2019fveq2d 5767 . . . . 5
2118, 20eleqtrd 2519 . . . 4
22 eqid 2443 . . . . 5
235, 3, 22, 13lmodvs0 16022 . . . 4
2417, 21, 23syl2anc 644 . . 3
25 fvex 5773 . . . . . . 7
2613, 25eqeltri 2513 . . . . . 6
2726fvconst2 5983 . . . . 5
2827oveq2d 6133 . . . 4