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

Metamath Proof Explorer

Theorem rhmpreimaidl

Description: The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024)

Ref Expression
Hypothesis rhmpreimaidl.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
Assertion rhmpreimaidl ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 rhmpreimaidl.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
2 cnvimass ⊢ ( ◡ 𝐹 “ 𝐽 ) ⊆ dom 𝐹
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 3 4 rhmf ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
6 2 5 fssdm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ◡ 𝐹 “ 𝐽 ) ⊆ ( Base ‘ 𝑅 ) )
7 6 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ⊆ ( Base ‘ 𝑅 ) )
8 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
9 8 ffund ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → Fun 𝐹 )
10 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
11 10 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 3 12 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
14 11 13 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
15 8 fdmd ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → dom 𝐹 = ( Base ‘ 𝑅 ) )
16 14 15 eleqtrrd ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 0g ‘ 𝑅 ) ∈ dom 𝐹 )
17 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
18 ghmmhm ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) )
19 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
20 12 19 mhm0 ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
21 17 18 20 3syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
22 21 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
23 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
24 eqid ⊢ ( LIdeal ‘ 𝑆 ) = ( LIdeal ‘ 𝑆 )
25 24 19 lidl0cl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) ∈ 𝐽 )
26 23 25 sylan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) ∈ 𝐽 )
27 22 26 eqeltrd ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ∈ 𝐽 )
28 fvimacnv ⊢ ( ( Fun 𝐹 ∧ ( 0g ‘ 𝑅 ) ∈ dom 𝐹 ) → ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ∈ 𝐽 ↔ ( 0g ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) )
29 28 biimpa ⊢ ( ( ( Fun 𝐹 ∧ ( 0g ‘ 𝑅 ) ∈ dom 𝐹 ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ∈ 𝐽 ) → ( 0g ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
30 9 16 27 29 syl21anc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( 0g ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
31 30 ne0d ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ≠ ∅ )
32 8 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
33 32 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
34 11 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑅 ∈ Ring )
35 simpllr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
36 6 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ◡ 𝐹 “ 𝐽 ) ⊆ ( Base ‘ 𝑅 ) )
37 36 sselda ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
38 37 adantr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
39 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
40 3 39 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
41 34 35 38 40 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
42 36 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ◡ 𝐹 “ 𝐽 ) ⊆ ( Base ‘ 𝑅 ) )
43 42 sselda ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
44 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
45 3 44 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
46 34 41 43 45 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
47 17 ad4antr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
48 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
49 3 44 48 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
50 47 41 43 49 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
51 simp-4l ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
52 51 23 syl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑆 ∈ Ring )
53 simpr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑆 ) )
54 53 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑆 ) )
55 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
56 3 39 55 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
57 51 35 38 56 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) )
58 8 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
59 58 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
60 simplr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) )
61 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ↔ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) ) )
62 61 simplbda ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 )
63 33 60 62 syl2anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 )
64 24 4 55 lidlmcl ⊢ ( ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) ∈ 𝐽 )
65 52 54 59 63 64 syl22anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑎 ) ) ∈ 𝐽 )
66 57 65 eqeltrd ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) ∈ 𝐽 )
67 simpr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) )
68 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ↔ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) ) )
69 68 simplbda ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 )
70 33 67 69 syl2anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 )
71 24 48 lidlacl ⊢ ( ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) ∈ 𝐽 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝐽 )
72 52 54 66 70 71 syl22anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝐽 )
73 50 72 eqeltrd ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 )
74 33 46 73 elpreimad ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
75 74 anasss ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
76 75 ralrimivva ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∀ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
77 76 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∀ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
78 1 3 44 39 islidl ⊢ ( ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ↔ ( ( ◡ 𝐹 “ 𝐽 ) ⊆ ( Base ‘ 𝑅 ) ∧ ( ◡ 𝐹 “ 𝐽 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∀ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) )
79 7 31 77 78 syl3anbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 )