Metamath Proof Explorer

Theorem imacrhmcl

Description: The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025)

Ref Expression
Hypotheses imacrhmcl.c 
|- C = ( N |`s ( F " S ) )
imacrhmcl.h 
|- ( ph -> F e. ( M RingHom N ) )
imacrhmcl.m 
|- ( ph -> M e. CRing )
imacrhmcl.s 
|- ( ph -> S e. ( SubRing ` M ) )
Assertion imacrhmcl 
|- ( ph -> C e. CRing )

Proof

Step Hyp Ref Expression
1 imacrhmcl.c 
 |-  C = ( N |`s ( F " S ) )
2 imacrhmcl.h 
 |-  ( ph -> F e. ( M RingHom N ) )
3 imacrhmcl.m 
 |-  ( ph -> M e. CRing )
4 imacrhmcl.s 
 |-  ( ph -> S e. ( SubRing ` M ) )
5 rhmima 
 |-  ( ( F e. ( M RingHom N ) /\ S e. ( SubRing ` M ) ) -> ( F " S ) e. ( SubRing ` N ) )
6 2 4 5 syl2anc 
 |-  ( ph -> ( F " S ) e. ( SubRing ` N ) )
7 1 subrgring 
 |-  ( ( F " S ) e. ( SubRing ` N ) -> C e. Ring )
8 6 7 syl 
 |-  ( ph -> C e. Ring )
9 1 ressbasss2 
 |-  ( Base ` C ) C_ ( F " S )
10 9 sseli 
 |-  ( x e. ( Base ` C ) -> x e. ( F " S ) )
11 9 sseli 
 |-  ( y e. ( Base ` C ) -> y e. ( F " S ) )
12 10 11 anim12i 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x e. ( F " S ) /\ y e. ( F " S ) ) )
13 eqid 
 |-  ( Base ` M ) = ( Base ` M )
14 eqid 
 |-  ( Base ` N ) = ( Base ` N )
15 13 14 rhmf 
 |-  ( F e. ( M RingHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
16 2 15 syl 
 |-  ( ph -> F : ( Base ` M ) --> ( Base ` N ) )
17 16 ffund 
 |-  ( ph -> Fun F )
18 fvelima 
 |-  ( ( Fun F /\ x e. ( F " S ) ) -> E. a e. S ( F ` a ) = x )
19 17 18 sylan 
 |-  ( ( ph /\ x e. ( F " S ) ) -> E. a e. S ( F ` a ) = x )
20 19 adantrr 
 |-  ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) -> E. a e. S ( F ` a ) = x )
21 fvelima 
 |-  ( ( Fun F /\ y e. ( F " S ) ) -> E. b e. S ( F ` b ) = y )
22 17 21 sylan 
 |-  ( ( ph /\ y e. ( F " S ) ) -> E. b e. S ( F ` b ) = y )
23 22 adantrl 
 |-  ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) -> E. b e. S ( F ` b ) = y )
24 23 adantr 
 |-  ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> E. b e. S ( F ` b ) = y )
25 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> M e. CRing )
26 13 subrgss 
 |-  ( S e. ( SubRing ` M ) -> S C_ ( Base ` M ) )
27 4 26 syl 
 |-  ( ph -> S C_ ( Base ` M ) )
28 27 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> S C_ ( Base ` M ) )
29 simplrl 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> a e. S )
30 28 29 sseldd 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> a e. ( Base ` M ) )
31 simprl 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> b e. S )
32 28 31 sseldd 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> b e. ( Base ` M ) )
33 eqid 
 |-  ( .r ` M ) = ( .r ` M )
34 13 33 crngcom 
 |-  ( ( M e. CRing /\ a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( a ( .r ` M ) b ) = ( b ( .r ` M ) a ) )
35 25 30 32 34 syl3anc 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( a ( .r ` M ) b ) = ( b ( .r ` M ) a ) )
36 35 fveq2d 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( F ` ( a ( .r ` M ) b ) ) = ( F ` ( b ( .r ` M ) a ) ) )
37 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> F e. ( M RingHom N ) )
38 eqid 
 |-  ( .r ` N ) = ( .r ` N )
39 13 33 38 rhmmul 
 |-  ( ( F e. ( M RingHom N ) /\ a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( F ` ( a ( .r ` M ) b ) ) = ( ( F ` a ) ( .r ` N ) ( F ` b ) ) )
40 37 30 32 39 syl3anc 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( F ` ( a ( .r ` M ) b ) ) = ( ( F ` a ) ( .r ` N ) ( F ` b ) ) )
41 13 33 38 rhmmul 
 |-  ( ( F e. ( M RingHom N ) /\ b e. ( Base ` M ) /\ a e. ( Base ` M ) ) -> ( F ` ( b ( .r ` M ) a ) ) = ( ( F ` b ) ( .r ` N ) ( F ` a ) ) )
42 37 32 30 41 syl3anc 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( F ` ( b ( .r ` M ) a ) ) = ( ( F ` b ) ( .r ` N ) ( F ` a ) ) )
43 36 40 42 3eqtr3d 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( ( F ` a ) ( .r ` N ) ( F ` b ) ) = ( ( F ` b ) ( .r ` N ) ( F ` a ) ) )
44 imaexg 
 |-  ( F e. ( M RingHom N ) -> ( F " S ) e. _V )
45 1 38 ressmulr 
 |-  ( ( F " S ) e. _V -> ( .r ` N ) = ( .r ` C ) )
46 2 44 45 3syl 
 |-  ( ph -> ( .r ` N ) = ( .r ` C ) )
47 46 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( .r ` N ) = ( .r ` C ) )
48 simplrr 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( F ` a ) = x )
49 simprr 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( F ` b ) = y )
50 47 48 49 oveq123d 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( ( F ` a ) ( .r ` N ) ( F ` b ) ) = ( x ( .r ` C ) y ) )
51 47 49 48 oveq123d 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( ( F ` b ) ( .r ` N ) ( F ` a ) ) = ( y ( .r ` C ) x ) )
52 43 50 51 3eqtr3d 
 |-  ( ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ ( b e. S /\ ( F ` b ) = y ) ) -> ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
53 24 52 rexlimddv 
 |-  ( ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
54 20 53 rexlimddv 
 |-  ( ( ph /\ ( x e. ( F " S ) /\ y e. ( F " S ) ) ) -> ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
55 12 54 sylan2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
56 55 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
57 eqid 
 |-  ( Base ` C ) = ( Base ` C )
58 eqid 
 |-  ( .r ` C ) = ( .r ` C )
59 57 58 iscrng2 
 |-  ( C e. CRing <-> ( C e. Ring /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) ) )
60 8 56 59 sylanbrc 
 |-  ( ph -> C e. CRing )