Metamath Proof Explorer


Theorem 0mhm

Description: The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses 0mhm.z 0 ˙ = 0 N
0mhm.b B = Base M
Assertion 0mhm M Mnd N Mnd B × 0 ˙ M MndHom N

Proof

Step Hyp Ref Expression
1 0mhm.z 0 ˙ = 0 N
2 0mhm.b B = Base M
3 id M Mnd N Mnd M Mnd N Mnd
4 eqid Base N = Base N
5 4 1 mndidcl N Mnd 0 ˙ Base N
6 5 adantl M Mnd N Mnd 0 ˙ Base N
7 fconst6g 0 ˙ Base N B × 0 ˙ : B Base N
8 6 7 syl M Mnd N Mnd B × 0 ˙ : B Base N
9 simpr M Mnd N Mnd N Mnd
10 eqid + N = + N
11 4 10 1 mndlid N Mnd 0 ˙ Base N 0 ˙ + N 0 ˙ = 0 ˙
12 11 eqcomd N Mnd 0 ˙ Base N 0 ˙ = 0 ˙ + N 0 ˙
13 9 5 12 syl2anc2 M Mnd N Mnd 0 ˙ = 0 ˙ + N 0 ˙
14 13 adantr M Mnd N Mnd x B y B 0 ˙ = 0 ˙ + N 0 ˙
15 eqid + M = + M
16 2 15 mndcl M Mnd x B y B x + M y B
17 16 3expb M Mnd x B y B x + M y B
18 17 adantlr M Mnd N Mnd x B y B x + M y B
19 1 fvexi 0 ˙ V
20 19 fvconst2 x + M y B B × 0 ˙ x + M y = 0 ˙
21 18 20 syl M Mnd N Mnd x B y B B × 0 ˙ x + M y = 0 ˙
22 19 fvconst2 x B B × 0 ˙ x = 0 ˙
23 19 fvconst2 y B B × 0 ˙ y = 0 ˙
24 22 23 oveqan12d x B y B B × 0 ˙ x + N B × 0 ˙ y = 0 ˙ + N 0 ˙
25 24 adantl M Mnd N Mnd x B y B B × 0 ˙ x + N B × 0 ˙ y = 0 ˙ + N 0 ˙
26 14 21 25 3eqtr4d M Mnd N Mnd x B y B B × 0 ˙ x + M y = B × 0 ˙ x + N B × 0 ˙ y
27 26 ralrimivva M Mnd N Mnd x B y B B × 0 ˙ x + M y = B × 0 ˙ x + N B × 0 ˙ y
28 eqid 0 M = 0 M
29 2 28 mndidcl M Mnd 0 M B
30 29 adantr M Mnd N Mnd 0 M B
31 19 fvconst2 0 M B B × 0 ˙ 0 M = 0 ˙
32 30 31 syl M Mnd N Mnd B × 0 ˙ 0 M = 0 ˙
33 8 27 32 3jca M Mnd N Mnd B × 0 ˙ : B Base N x B y B B × 0 ˙ x + M y = B × 0 ˙ x + N B × 0 ˙ y B × 0 ˙ 0 M = 0 ˙
34 2 4 15 10 28 1 ismhm B × 0 ˙ M MndHom N M Mnd N Mnd B × 0 ˙ : B Base N x B y B B × 0 ˙ x + M y = B × 0 ˙ x + N B × 0 ˙ y B × 0 ˙ 0 M = 0 ˙
35 3 33 34 sylanbrc M Mnd N Mnd B × 0 ˙ M MndHom N