Metamath Proof Explorer

Theorem imasmgm2

Description: The image structure of a unital magma is a unital magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses imasmgm.u 
|- ( ph -> U = ( F "s R ) )
imasmgm.v 
|- ( ph -> V = ( Base ` R ) )
imasmgm.p 
|- .+ = ( +g ` R )
imasmgm.f 
|- ( ph -> F : V -onto-> B )
imasmgm.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 ) ) ) )
imasmgm2.r 
|- ( ph -> R e. W )
imasmgm2.1 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
imasmgm2.2 
|- ( ph -> .0. e. V )
imasmgm2.3 
|- ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
imasmgm2.4 
|- ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) )
Assertion imasmgm2 
|- ( ph -> ( U e. Mgm /\ ( F ` .0. ) = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 imasmgm.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasmgm.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasmgm.p 
 |-  .+ = ( +g ` R )
4 imasmgm.f 
 |-  ( ph -> F : V -onto-> B )
5 imasmgm.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 imasmgm2.r 
 |-  ( ph -> R e. W )
7 imasmgm2.1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
8 imasmgm2.2 
 |-  ( ph -> .0. e. V )
9 imasmgm2.3 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
10 imasmgm2.4 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) )
11 1 2 4 6 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
12 ovex 
 |-  ( F "s R ) e. _V
13 1 12 eqeltrdi 
 |-  ( ph -> U e. _V )
14 eqidd 
 |-  ( ph -> ( +g ` U ) = ( +g ` U ) )
15 eqid 
 |-  ( +g ` U ) = ( +g ` U )
16 7 3expb 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V )
17 16 caovclg 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .+ q ) e. V )
18 4 5 1 2 6 3 15 17 imasaddf 
 |-  ( ph -> ( +g ` U ) : ( B X. B ) --> B )
19 18 fovcld 
 |-  ( ( ph /\ u e. B /\ v e. B ) -> ( u ( +g ` U ) v ) e. B )
20 11 13 14 19 ismgmd 
 |-  ( ph -> U e. Mgm )
21 fof 
 |-  ( F : V -onto-> B -> F : V --> B )
22 4 21 syl 
 |-  ( ph -> F : V --> B )
23 22 8 ffvelcdmd 
 |-  ( ph -> ( F ` .0. ) e. B )
24 forn 
 |-  ( F : V -onto-> B -> ran F = B )
25 4 24 syl 
 |-  ( ph -> ran F = B )
26 25 eleq2d 
 |-  ( ph -> ( u e. ran F <-> u e. B ) )
27 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
28 fvelrnb 
 |-  ( F Fn V -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) )
29 4 27 28 3syl 
 |-  ( ph -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) )
30 26 29 bitr3d 
 |-  ( ph -> ( u e. B <-> E. x e. V ( F ` x ) = u ) )
31 simpl 
 |-  ( ( ph /\ x e. V ) -> ph )
32 8 adantr 
 |-  ( ( ph /\ x e. V ) -> .0. e. V )
33 simpr 
 |-  ( ( ph /\ x e. V ) -> x e. V )
34 4 5 1 2 6 3 15 imasaddval 
 |-  ( ( ph /\ .0. e. V /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` ( .0. .+ x ) ) )
35 31 32 33 34 syl3anc 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` ( .0. .+ x ) ) )
36 35 9 eqtrd 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` x ) )
37 oveq2 
 |-  ( ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( ( F ` .0. ) ( +g ` U ) u ) )
38 id 
 |-  ( ( F ` x ) = u -> ( F ` x ) = u )
39 37 38 eqeq12d 
 |-  ( ( F ` x ) = u -> ( ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` x ) <-> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
40 36 39 syl5ibcom 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
41 40 rexlimdva 
 |-  ( ph -> ( E. x e. V ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
42 30 41 sylbid 
 |-  ( ph -> ( u e. B -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
43 42 imp 
 |-  ( ( ph /\ u e. B ) -> ( ( F ` .0. ) ( +g ` U ) u ) = u )
44 4 5 1 2 6 3 15 imasaddval 
 |-  ( ( ph /\ x e. V /\ .0. e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` ( x .+ .0. ) ) )
45 32 44 mpd3an3 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` ( x .+ .0. ) ) )
46 45 10 eqtrd 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` x ) )
47 oveq1 
 |-  ( ( F ` x ) = u -> ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( u ( +g ` U ) ( F ` .0. ) ) )
48 47 38 eqeq12d 
 |-  ( ( F ` x ) = u -> ( ( ( F ` x ) ( +g ` U ) ( F ` .0. ) ) = ( F ` x ) <-> ( u ( +g ` U ) ( F ` .0. ) ) = u ) )
49 46 48 syl5ibcom 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` x ) = u -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) )
50 49 rexlimdva 
 |-  ( ph -> ( E. x e. V ( F ` x ) = u -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) )
51 30 50 sylbid 
 |-  ( ph -> ( u e. B -> ( u ( +g ` U ) ( F ` .0. ) ) = u ) )
52 51 imp 
 |-  ( ( ph /\ u e. B ) -> ( u ( +g ` U ) ( F ` .0. ) ) = u )
53 11 14 23 43 52 grpidd 
 |-  ( ph -> ( F ` .0. ) = ( 0g ` U ) )
54 20 53 jca 
 |-  ( ph -> ( U e. Mgm /\ ( F ` .0. ) = ( 0g ` U ) ) )