Metamath Proof Explorer


Theorem imasmnd2

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
imasmnd2.r φ R W
imasmnd2.1 φ x V y V x + ˙ y V
imasmnd2.2 φ x V y V z V F x + ˙ y + ˙ z = F x + ˙ y + ˙ z
imasmnd2.3 φ 0 ˙ V
imasmnd2.4 φ x V F 0 ˙ + ˙ x = F x
imasmnd2.5 φ x V F x + ˙ 0 ˙ = F x
Assertion imasmnd2 φ 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 imasmnd2.r φ R W
7 imasmnd2.1 φ x V y V x + ˙ y V
8 imasmnd2.2 φ x V y V z V F x + ˙ y + ˙ z = F x + ˙ y + ˙ z
9 imasmnd2.3 φ 0 ˙ V
10 imasmnd2.4 φ x V F 0 ˙ + ˙ x = F x
11 imasmnd2.5 φ x V F x + ˙ 0 ˙ = F x
12 1 2 4 6 imasbas φ B = Base U
13 eqidd φ + U = + U
14 eqid + U = + U
15 7 3expb φ x V y V x + ˙ y V
16 15 caovclg φ p V q V p + ˙ q V
17 4 5 1 2 6 3 14 16 imasaddf φ + U : B × B B
18 fovrn + U : B × B B u B v B u + U v B
19 17 18 syl3an1 φ u B v B u + U v B
20 forn F : V onto B ran F = B
21 4 20 syl φ ran F = B
22 21 eleq2d φ u ran F u B
23 21 eleq2d φ v ran F v B
24 21 eleq2d φ w ran F w B
25 22 23 24 3anbi123d φ u ran F v ran F w ran F u B v B w B
26 fofn F : V onto B F Fn V
27 4 26 syl φ F Fn V
28 fvelrnb F Fn V u ran F x V F x = u
29 fvelrnb F Fn V v ran F y V F y = v
30 fvelrnb F Fn V w ran F z V F z = w
31 28 29 30 3anbi123d F Fn V u ran F v ran F w ran F x V F x = u y V F y = v z V F z = w
32 27 31 syl φ u ran F v ran F w ran F x V F x = u y V F y = v z V F z = w
33 25 32 bitr3d φ u B v B w B x V F x = u y V F y = v z V F z = w
34 3reeanv x V y V z V F x = u F y = v F z = w x V F x = u y V F y = v z V F z = w
35 33 34 bitr4di φ u B v B w B x V y V z V F x = u F y = v F z = w
36 simpl φ x V y V z V φ
37 7 3adant3r3 φ x V y V z V x + ˙ y V
38 simpr3 φ x V y V z V z V
39 4 5 1 2 6 3 14 imasaddval φ x + ˙ y V z V F x + ˙ y + U F z = F x + ˙ y + ˙ z
40 36 37 38 39 syl3anc φ x V y V z V F x + ˙ y + U F z = F x + ˙ y + ˙ z
41 simpr1 φ x V y V z V x V
42 16 caovclg φ y V z V y + ˙ z V
43 42 3adantr1 φ x V y V z V y + ˙ z V
44 4 5 1 2 6 3 14 imasaddval φ x V y + ˙ z V F x + U F y + ˙ z = F x + ˙ y + ˙ z
45 36 41 43 44 syl3anc φ x V y V z V F x + U F y + ˙ z = F x + ˙ y + ˙ z
46 8 40 45 3eqtr4d φ x V y V z V F x + ˙ y + U F z = F x + U F y + ˙ z
47 4 5 1 2 6 3 14 imasaddval φ x V y V F x + U F y = F x + ˙ y
48 47 3adant3r3 φ x V y V z V F x + U F y = F x + ˙ y
49 48 oveq1d φ x V y V z V F x + U F y + U F z = F x + ˙ y + U F z
50 4 5 1 2 6 3 14 imasaddval φ y V z V F y + U F z = F y + ˙ z
51 50 3adant3r1 φ x V y V z V F y + U F z = F y + ˙ z
52 51 oveq2d φ x V y V z V F x + U F y + U F z = F x + U F y + ˙ z
53 46 49 52 3eqtr4d φ x V y V z V F x + U F y + U F z = F x + U F y + U F z
54 simp1 F x = u F y = v F z = w F x = u
55 simp2 F x = u F y = v F z = w F y = v
56 54 55 oveq12d F x = u F y = v F z = w F x + U F y = u + U v
57 simp3 F x = u F y = v F z = w F z = w
58 56 57 oveq12d F x = u F y = v F z = w F x + U F y + U F z = u + U v + U w
59 55 57 oveq12d F x = u F y = v F z = w F y + U F z = v + U w
60 54 59 oveq12d F x = u F y = v F z = w F x + U F y + U F z = u + U v + U w
61 58 60 eqeq12d F x = u F y = v F z = w F x + U F y + U F z = F x + U F y + U F z u + U v + U w = u + U v + U w
62 53 61 syl5ibcom φ x V y V z V F x = u F y = v F z = w u + U v + U w = u + U v + U w
63 62 3exp2 φ x V y V z V F x = u F y = v F z = w u + U v + U w = u + U v + U w
64 63 imp32 φ x V y V z V F x = u F y = v F z = w u + U v + U w = u + U v + U w
65 64 rexlimdv φ x V y V z V F x = u F y = v F z = w u + U v + U w = u + U v + U w
66 65 rexlimdvva φ x V y V z V F x = u F y = v F z = w u + U v + U w = u + U v + U w
67 35 66 sylbid φ u B v B w B u + U v + U w = u + U v + U w
68 67 imp φ u B v B w B u + U v + U w = u + U v + U w
69 fof F : V onto B F : V B
70 4 69 syl φ F : V B
71 70 9 ffvelrnd φ F 0 ˙ B
72 27 28 syl φ u ran F x V F x = u
73 22 72 bitr3d φ u B x V F x = u
74 simpl φ x V φ
75 9 adantr φ x V 0 ˙ V
76 simpr φ x V x V
77 4 5 1 2 6 3 14 imasaddval φ 0 ˙ V x V F 0 ˙ + U F x = F 0 ˙ + ˙ x
78 74 75 76 77 syl3anc φ x V F 0 ˙ + U F x = F 0 ˙ + ˙ x
79 78 10 eqtrd φ x V F 0 ˙ + U F x = F x
80 oveq2 F x = u F 0 ˙ + U F x = F 0 ˙ + U u
81 id F x = u F x = u
82 80 81 eqeq12d F x = u F 0 ˙ + U F x = F x F 0 ˙ + U u = u
83 79 82 syl5ibcom φ x V F x = u F 0 ˙ + U u = u
84 83 rexlimdva φ x V F x = u F 0 ˙ + U u = u
85 73 84 sylbid φ u B F 0 ˙ + U u = u
86 85 imp φ u B F 0 ˙ + U u = u
87 4 5 1 2 6 3 14 imasaddval φ x V 0 ˙ V F x + U F 0 ˙ = F x + ˙ 0 ˙
88 75 87 mpd3an3 φ x V F x + U F 0 ˙ = F x + ˙ 0 ˙
89 88 11 eqtrd φ x V F x + U F 0 ˙ = F x
90 oveq1 F x = u F x + U F 0 ˙ = u + U F 0 ˙
91 90 81 eqeq12d F x = u F x + U F 0 ˙ = F x u + U F 0 ˙ = u
92 89 91 syl5ibcom φ x V F x = u u + U F 0 ˙ = u
93 92 rexlimdva φ x V F x = u u + U F 0 ˙ = u
94 73 93 sylbid φ u B u + U F 0 ˙ = u
95 94 imp φ u B u + U F 0 ˙ = u
96 12 13 19 68 71 86 95 ismndd φ U Mnd
97 12 13 71 86 95 grpidd φ F 0 ˙ = 0 U
98 96 97 jca φ U Mnd F 0 ˙ = 0 U