Metamath Proof Explorer


Theorem imasmnd

Description: The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasmnd.u φ U = F 𝑠 R
imasmnd.v φ V = Base R
imasmnd.p + ˙ = + R
imasmnd.f φ F : V onto B
imasmnd.e φ a V b V p V q V F a = F p F b = F q F a + ˙ b = F p + ˙ q
imasmnd.r φ R Mnd
imasmnd.z 0 ˙ = 0 R
Assertion imasmnd φ U Mnd F 0 ˙ = 0 U

Proof

Step Hyp Ref Expression
1 imasmnd.u φ U = F 𝑠 R
2 imasmnd.v φ V = Base R
3 imasmnd.p + ˙ = + R
4 imasmnd.f φ F : V onto B
5 imasmnd.e φ a V b V p V q V F a = F p F b = F q F a + ˙ b = F p + ˙ q
6 imasmnd.r φ R Mnd
7 imasmnd.z 0 ˙ = 0 R
8 6 3ad2ant1 φ x V y V R Mnd
9 simp2 φ x V y V x V
10 2 3ad2ant1 φ x V y V V = Base R
11 9 10 eleqtrd φ x V y V x Base R
12 simp3 φ x V y V y V
13 12 10 eleqtrd φ x V y V y Base R
14 eqid Base R = Base R
15 14 3 mndcl R Mnd x Base R y Base R x + ˙ y Base R
16 8 11 13 15 syl3anc φ x V y V x + ˙ y Base R
17 16 10 eleqtrrd φ x V y V x + ˙ y V
18 6 adantr φ x V y V z V R Mnd
19 11 3adant3r3 φ x V y V z V x Base R
20 13 3adant3r3 φ x V y V z V y Base R
21 simpr3 φ x V y V z V z V
22 2 adantr φ x V y V z V V = Base R
23 21 22 eleqtrd φ x V y V z V z Base R
24 14 3 mndass R Mnd x Base R y Base R z Base R x + ˙ y + ˙ z = x + ˙ y + ˙ z
25 18 19 20 23 24 syl13anc φ x V y V z V x + ˙ y + ˙ z = x + ˙ y + ˙ z
26 25 fveq2d φ x V y V z V F x + ˙ y + ˙ z = F x + ˙ y + ˙ z
27 14 7 mndidcl R Mnd 0 ˙ Base R
28 6 27 syl φ 0 ˙ Base R
29 28 2 eleqtrrd φ 0 ˙ V
30 2 eleq2d φ x V x Base R
31 30 biimpa φ x V x Base R
32 14 3 7 mndlid R Mnd x Base R 0 ˙ + ˙ x = x
33 6 31 32 syl2an2r φ x V 0 ˙ + ˙ x = x
34 33 fveq2d φ x V F 0 ˙ + ˙ x = F x
35 14 3 7 mndrid R Mnd x Base R x + ˙ 0 ˙ = x
36 6 31 35 syl2an2r φ x V x + ˙ 0 ˙ = x
37 36 fveq2d φ x V F x + ˙ 0 ˙ = F x
38 1 2 3 4 5 6 17 26 29 34 37 imasmnd2 φ U Mnd F 0 ˙ = 0 U