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 fovrn
 |-  ( ( ( +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 ffvelrnd
 |-  ( 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 ) ) )