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 
|- ( ph -> U = ( F "s R ) )
imasmnd.v 
|- ( ph -> V = ( Base ` R ) )
imasmnd.p 
|- .+ = ( +g ` R )
imasmnd.f 
|- ( ph -> F : V -onto-> B )
imasmnd.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasmnd2.r 
|- ( ph -> R e. W )
imasmnd2.1 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
imasmnd2.2 
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )
imasmnd2.3 
|- ( ph -> .0. e. V )
imasmnd2.4 
|- ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
imasmnd2.5 
|- ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) )
Assertion imasmnd2 
|- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )

Proof

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