This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasrhm

Description: Given a function F with homomorphic properties, build the image of a ring. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses imasmhm.b 
|- B = ( Base ` W )
imasmhm.f 
|- ( ph -> F : B --> C )
imasmhm.1 
|- .+ = ( +g ` W )
imasmhm.2 
|- ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasrhm.3 
|- .x. = ( .r ` W )
imasrhm.4 
|- ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
imasrhm.w 
|- ( ph -> W e. Ring )
Assertion imasrhm 
|- ( ph -> ( ( F "s W ) e. Ring /\ F e. ( W RingHom ( F "s W ) ) ) )

Proof

Step Hyp Ref Expression
1 imasmhm.b 
 |-  B = ( Base ` W )
2 imasmhm.f 
 |-  ( ph -> F : B --> C )
3 imasmhm.1 
 |-  .+ = ( +g ` W )
4 imasmhm.2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
5 imasrhm.3 
 |-  .x. = ( .r ` W )
6 imasrhm.4 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
7 imasrhm.w 
 |-  ( ph -> W e. Ring )
8 eqidd 
 |-  ( ph -> ( F "s W ) = ( F "s W ) )
9 1 a1i 
 |-  ( ph -> B = ( Base ` W ) )
10 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
11 fimadmfo 
 |-  ( F : B --> C -> F : B -onto-> ( F " B ) )
12 2 11 syl 
 |-  ( ph -> F : B -onto-> ( F " B ) )
13 8 9 3 5 10 12 4 6 7 imasring 
 |-  ( ph -> ( ( F "s W ) e. Ring /\ ( F ` ( 1r ` W ) ) = ( 1r ` ( F "s W ) ) ) )
14 13 simpld 
 |-  ( ph -> ( F "s W ) e. Ring )
15 eqid 
 |-  ( 1r ` ( F "s W ) ) = ( 1r ` ( F "s W ) )
16 eqid 
 |-  ( .r ` ( F "s W ) ) = ( .r ` ( F "s W ) )
17 13 simprd 
 |-  ( ph -> ( F ` ( 1r ` W ) ) = ( 1r ` ( F "s W ) ) )
18 12 6 8 9 7 5 16 imasmulval 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( F ` x ) ( .r ` ( F "s W ) ) ( F ` y ) ) = ( F ` ( x .x. y ) ) )
19 18 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) ( .r ` ( F "s W ) ) ( F ` y ) ) = ( F ` ( x .x. y ) ) )
20 19 eqcomd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) ( .r ` ( F "s W ) ) ( F ` y ) ) )
21 eqid 
 |-  ( Base ` ( F "s W ) ) = ( Base ` ( F "s W ) )
22 eqid 
 |-  ( +g ` ( F "s W ) ) = ( +g ` ( F "s W ) )
23 fof 
 |-  ( F : B -onto-> ( F " B ) -> F : B --> ( F " B ) )
24 12 23 syl 
 |-  ( ph -> F : B --> ( F " B ) )
25 8 9 12 7 imasbas 
 |-  ( ph -> ( F " B ) = ( Base ` ( F "s W ) ) )
26 25 feq3d 
 |-  ( ph -> ( F : B --> ( F " B ) <-> F : B --> ( Base ` ( F "s W ) ) ) )
27 24 26 mpbid 
 |-  ( ph -> F : B --> ( Base ` ( F "s W ) ) )
28 12 4 8 9 7 3 22 imasaddval 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( F ` x ) ( +g ` ( F "s W ) ) ( F ` y ) ) = ( F ` ( x .+ y ) ) )
29 28 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) ( +g ` ( F "s W ) ) ( F ` y ) ) = ( F ` ( x .+ y ) ) )
30 29 eqcomd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) ( +g ` ( F "s W ) ) ( F ` y ) ) )
31 1 10 15 5 16 7 14 17 20 21 3 22 27 30 isrhmd 
 |-  ( ph -> F e. ( W RingHom ( F "s W ) ) )
32 14 31 jca 
 |-  ( ph -> ( ( F "s W ) e. Ring /\ F e. ( W RingHom ( F "s W ) ) ) )