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

Theorem 0lmhm 15813
 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 2296 . 2
3 eqid 2296 . 2
4 0lmhm.s . 2 Scalar
5 0lmhm.t . 2 Scalar
6 eqid 2296 . 2
7 simp1 955 . 2
8 simp2 956 . 2
9 simp3 957 . . 3
109eqcomd 2301 . 2
11 lmodgrp 15650 . . . 4
12 lmodgrp 15650 . . . 4
13 0lmhm.z . . . . 5
1413, 10ghm 14713 . . . 4
1511, 12, 14syl2an 463 . . 3
17 simpl2 959 . . . 4
18 simprl 732 . . . . 5
19 simpl3 960 . . . . . 6
2019fveq2d 5545 . . . . 5
2118, 20eleqtrd 2372 . . . 4
22 eqid 2296 . . . . 5
235, 3, 22, 13lmodvs0 15680 . . . 4
2417, 21, 23syl2anc 642 . . 3
25 fvex 5555 . . . . . . 7
2613, 25eqeltri 2366 . . . . . 6
2726fvconst2 5745 . . . . 5
2827oveq2d 5890 . . . 4