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 𝑠 F S
imacrhmcl.h φ F M RingHom N
imacrhmcl.m φ M CRing
imacrhmcl.s φ S SubRing M
Assertion imacrhmcl φ C CRing

Proof

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