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 ⊢ 𝐶 = ( 𝑁 ↾s ( 𝐹 “ 𝑆 ) )
imacrhmcl.h ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) )
imacrhmcl.m ⊢ ( 𝜑 → 𝑀 ∈ CRing )
imacrhmcl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑀 ) )
Assertion imacrhmcl ( 𝜑 → 𝐶 ∈ CRing )

Proof

Step Hyp Ref Expression
1 imacrhmcl.c ⊢ 𝐶 = ( 𝑁 ↾s ( 𝐹 “ 𝑆 ) )
2 imacrhmcl.h ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) )
3 imacrhmcl.m ⊢ ( 𝜑 → 𝑀 ∈ CRing )
4 imacrhmcl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑀 ) )
5 rhmima ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑆 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑆 ) ∈ ( SubRing ‘ 𝑁 ) )
6 2 4 5 syl2anc ⊢ ( 𝜑 → ( 𝐹 “ 𝑆 ) ∈ ( SubRing ‘ 𝑁 ) )
7 1 subrgring ⊢ ( ( 𝐹 “ 𝑆 ) ∈ ( SubRing ‘ 𝑁 ) → 𝐶 ∈ Ring )
8 6 7 syl ⊢ ( 𝜑 → 𝐶 ∈ Ring )
9 1 ressbasss2 ⊢ ( Base ‘ 𝐶 ) ⊆ ( 𝐹 “ 𝑆 )
10 9 sseli ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) → 𝑥 ∈ ( 𝐹 “ 𝑆 ) )
11 9 sseli ⊢ ( 𝑦 ∈ ( Base ‘ 𝐶 ) → 𝑦 ∈ ( 𝐹 “ 𝑆 ) )
12 10 11 anim12i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) )
13 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
14 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
15 13 14 rhmf ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
16 2 15 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
17 16 ffund ⊢ ( 𝜑 → Fun 𝐹 )
18 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑎 ∈ 𝑆 ( 𝐹 ‘ 𝑎 ) = 𝑥 )
19 17 18 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑎 ∈ 𝑆 ( 𝐹 ‘ 𝑎 ) = 𝑥 )
20 19 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) → ∃ 𝑎 ∈ 𝑆 ( 𝐹 ‘ 𝑎 ) = 𝑥 )
21 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑏 ∈ 𝑆 ( 𝐹 ‘ 𝑏 ) = 𝑦 )
22 17 21 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑏 ∈ 𝑆 ( 𝐹 ‘ 𝑏 ) = 𝑦 )
23 22 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) → ∃ 𝑏 ∈ 𝑆 ( 𝐹 ‘ 𝑏 ) = 𝑦 )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) → ∃ 𝑏 ∈ 𝑆 ( 𝐹 ‘ 𝑏 ) = 𝑦 )
25 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝑀 ∈ CRing )
26 13 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
27 4 26 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
28 27 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
29 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝑎 ∈ 𝑆 )
30 28 29 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝑎 ∈ ( Base ‘ 𝑀 ) )
31 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝑏 ∈ 𝑆 )
32 28 31 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝑏 ∈ ( Base ‘ 𝑀 ) )
33 eqid ⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 )
34 13 33 crngcom ⊢ ( ( 𝑀 ∈ CRing ∧ 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑎 ( .r ‘ 𝑀 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑀 ) 𝑎 ) )
35 25 30 32 34 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝑎 ( .r ‘ 𝑀 ) 𝑏 ) = ( 𝑏 ( .r ‘ 𝑀 ) 𝑎 ) )
36 35 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑀 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑏 ( .r ‘ 𝑀 ) 𝑎 ) ) )
37 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) )
38 eqid ⊢ ( .r ‘ 𝑁 ) = ( .r ‘ 𝑁 )
39 13 33 38 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑏 ) ) )
40 37 30 32 39 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑏 ) ) )
41 13 33 38 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ∧ 𝑎 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑏 ( .r ‘ 𝑀 ) 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑎 ) ) )
42 37 32 30 41 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝐹 ‘ ( 𝑏 ( .r ‘ 𝑀 ) 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑎 ) ) )
43 36 40 42 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑎 ) ) )
44 imaexg ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( 𝐹 “ 𝑆 ) ∈ V )
45 1 38 ressmulr ⊢ ( ( 𝐹 “ 𝑆 ) ∈ V → ( .r ‘ 𝑁 ) = ( .r ‘ 𝐶 ) )
46 2 44 45 3syl ⊢ ( 𝜑 → ( .r ‘ 𝑁 ) = ( .r ‘ 𝐶 ) )
47 46 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( .r ‘ 𝑁 ) = ( .r ‘ 𝐶 ) )
48 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑎 ) = 𝑥 )
49 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑏 ) = 𝑦 )
50 47 48 49 oveq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) )
51 47 49 48 oveq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑁 ) ( 𝐹 ‘ 𝑎 ) ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
52 43 50 51 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) ∧ ( 𝑏 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
53 24 52 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
54 20 53 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐹 “ 𝑆 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
55 12 54 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
56 55 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
57 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
58 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
59 57 58 iscrng2 ⊢ ( 𝐶 ∈ CRing ↔ ( 𝐶 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ) )
60 8 56 59 sylanbrc ⊢ ( 𝜑 → 𝐶 ∈ CRing )