Metamath Proof Explorer


Theorem rhmimaidl

Description: The image of an ideal I by a surjective ring homomorphism F is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024)

Ref Expression
Hypotheses rhmimaidl.b 𝐵 = ( Base ‘ 𝑆 )
rhmimaidl.t 𝑇 = ( LIdeal ‘ 𝑅 )
rhmimaidl.u 𝑈 = ( LIdeal ‘ 𝑆 )
Assertion rhmimaidl ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵𝐼𝑇 ) → ( 𝐹𝐼 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 rhmimaidl.b 𝐵 = ( Base ‘ 𝑆 )
2 rhmimaidl.t 𝑇 = ( LIdeal ‘ 𝑅 )
3 rhmimaidl.u 𝑈 = ( LIdeal ‘ 𝑆 )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 4 1 rhmf ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐵 )
6 fimass ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐵 → ( 𝐹𝐼 ) ⊆ 𝐵 )
7 5 6 syl ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹𝐼 ) ⊆ 𝐵 )
8 7 ad2antrr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ( 𝐹𝐼 ) ⊆ 𝐵 )
9 5 ffnd ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
10 9 ad2antrr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
11 rhmrcl1 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
12 11 ad2antrr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → 𝑅 ∈ Ring )
13 eqid ( 0g𝑅 ) = ( 0g𝑅 )
14 4 13 ring0cl ( 𝑅 ∈ Ring → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
15 12 14 syl ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
16 simpr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → 𝐼𝑇 )
17 2 13 lidl0cl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑇 ) → ( 0g𝑅 ) ∈ 𝐼 )
18 12 16 17 syl2anc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ( 0g𝑅 ) ∈ 𝐼 )
19 10 15 18 fnfvimad ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ( 𝐹 ‘ ( 0g𝑅 ) ) ∈ ( 𝐹𝐼 ) )
20 19 ne0d ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ( 𝐹𝐼 ) ≠ ∅ )
21 rhmghm ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
22 21 ad4antr ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
23 11 ad4antr ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
24 simpr ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
25 4 2 lidlss ( 𝐼𝑇𝐼 ⊆ ( Base ‘ 𝑅 ) )
26 25 ad4antlr ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
27 simplr ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝑖𝐼 )
28 26 27 sseldd ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝑖 ∈ ( Base ‘ 𝑅 ) )
29 eqid ( .r𝑅 ) = ( .r𝑅 )
30 4 29 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑧 ( .r𝑅 ) 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
31 23 24 28 30 syl3anc ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑧 ( .r𝑅 ) 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
32 simpllr ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝑗𝐼 )
33 26 32 sseldd ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝑗 ∈ ( Base ‘ 𝑅 ) )
34 eqid ( +g𝑅 ) = ( +g𝑅 )
35 eqid ( +g𝑆 ) = ( +g𝑆 )
36 4 34 35 ghmlin ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( 𝑧 ( .r𝑅 ) 𝑖 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑗 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( 𝐹 ‘ ( 𝑧 ( .r𝑅 ) 𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
37 22 31 33 36 syl3anc ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( 𝐹 ‘ ( 𝑧 ( .r𝑅 ) 𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
38 simp-4l ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
39 eqid ( .r𝑆 ) = ( .r𝑆 )
40 4 29 39 rhmmul ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑧 ( .r𝑅 ) 𝑖 ) ) = ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) )
41 38 24 28 40 syl3anc ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑧 ( .r𝑅 ) 𝑖 ) ) = ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) )
42 41 oveq1d ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑧 ( .r𝑅 ) 𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
43 37 42 eqtrd ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
44 43 adantl4r ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
45 44 adantl3r ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
46 45 adantl3r ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
47 46 adantl3r ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
48 47 adantllr ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
49 48 ad4ant13 ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) )
50 simpr ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( 𝐹𝑧 ) = 𝑥 )
51 simpllr ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( 𝐹𝑖 ) = 𝑎 )
52 50 51 oveq12d ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) = ( 𝑥 ( .r𝑆 ) 𝑎 ) )
53 simp-5r ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( 𝐹𝑗 ) = 𝑏 )
54 52 53 oveq12d ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( ( ( 𝐹𝑧 ) ( .r𝑆 ) ( 𝐹𝑖 ) ) ( +g𝑆 ) ( 𝐹𝑗 ) ) = ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) )
55 49 54 eqtrd ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) = ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) )
56 10 ad9antr ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
57 16 25 syl ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
58 57 ad9antr ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
59 16 ad9antr ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → 𝐼𝑇 )
60 simplr ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
61 simp-4r ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → 𝑖𝐼 )
62 simp-6r ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → 𝑗𝐼 )
63 2 4 34 29 islidl ( 𝐼𝑇 ↔ ( 𝐼 ⊆ ( Base ‘ 𝑅 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝐼𝑗𝐼 ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ 𝐼 ) )
64 63 simp3bi ( 𝐼𝑇 → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖𝐼𝑗𝐼 ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ 𝐼 )
65 64 r19.21bi ( ( 𝐼𝑇𝑧 ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑖𝐼𝑗𝐼 ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ 𝐼 )
66 65 r19.21bi ( ( ( 𝐼𝑇𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖𝐼 ) → ∀ 𝑗𝐼 ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ 𝐼 )
67 66 r19.21bi ( ( ( ( 𝐼𝑇𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖𝐼 ) ∧ 𝑗𝐼 ) → ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ 𝐼 )
68 59 60 61 62 67 syl1111anc ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ 𝐼 )
69 58 68 sseldd ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
70 56 69 68 fnfvimad ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( 𝐹 ‘ ( ( 𝑧 ( .r𝑅 ) 𝑖 ) ( +g𝑅 ) 𝑗 ) ) ∈ ( 𝐹𝐼 ) )
71 55 70 eqeltrrd ( ( ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐹𝑧 ) = 𝑥 ) → ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
72 5 ad2antrr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐵 )
73 72 ffund ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → Fun 𝐹 )
74 73 ad7antr ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) → Fun 𝐹 )
75 5 fdmd ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → dom 𝐹 = ( Base ‘ 𝑅 ) )
76 75 imaeq2d ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ ( Base ‘ 𝑅 ) ) )
77 imadmrn ( 𝐹 “ dom 𝐹 ) = ran 𝐹
78 76 77 eqtr3di ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 “ ( Base ‘ 𝑅 ) ) = ran 𝐹 )
79 78 eqeq1d ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹 “ ( Base ‘ 𝑅 ) ) = 𝐵 ↔ ran 𝐹 = 𝐵 ) )
80 79 biimpar ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) → ( 𝐹 “ ( Base ‘ 𝑅 ) ) = 𝐵 )
81 80 eleq2d ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) → ( 𝑥 ∈ ( 𝐹 “ ( Base ‘ 𝑅 ) ) ↔ 𝑥𝐵 ) )
82 81 biimpar ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝑥𝐵 ) → 𝑥 ∈ ( 𝐹 “ ( Base ‘ 𝑅 ) ) )
83 82 adantlr ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) → 𝑥 ∈ ( 𝐹 “ ( Base ‘ 𝑅 ) ) )
84 83 ad6antr ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) → 𝑥 ∈ ( 𝐹 “ ( Base ‘ 𝑅 ) ) )
85 fvelima ( ( Fun 𝐹𝑥 ∈ ( 𝐹 “ ( Base ‘ 𝑅 ) ) ) → ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝐹𝑧 ) = 𝑥 )
86 74 84 85 syl2anc ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) → ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝐹𝑧 ) = 𝑥 )
87 71 86 r19.29a ( ( ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) ∧ 𝑖𝐼 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) → ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
88 73 ad5antr ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) → Fun 𝐹 )
89 simp-4r ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) → 𝑎 ∈ ( 𝐹𝐼 ) )
90 fvelima ( ( Fun 𝐹𝑎 ∈ ( 𝐹𝐼 ) ) → ∃ 𝑖𝐼 ( 𝐹𝑖 ) = 𝑎 )
91 88 89 90 syl2anc ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) → ∃ 𝑖𝐼 ( 𝐹𝑖 ) = 𝑎 )
92 87 91 r19.29a ( ( ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ∧ 𝑗𝐼 ) ∧ ( 𝐹𝑗 ) = 𝑏 ) → ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
93 73 ad3antrrr ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) → Fun 𝐹 )
94 simpr ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) → 𝑏 ∈ ( 𝐹𝐼 ) )
95 fvelima ( ( Fun 𝐹𝑏 ∈ ( 𝐹𝐼 ) ) → ∃ 𝑗𝐼 ( 𝐹𝑗 ) = 𝑏 )
96 93 94 95 syl2anc ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) → ∃ 𝑗𝐼 ( 𝐹𝑗 ) = 𝑏 )
97 92 96 r19.29a ( ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ 𝑎 ∈ ( 𝐹𝐼 ) ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) → ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
98 97 anasss ( ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) ∧ ( 𝑎 ∈ ( 𝐹𝐼 ) ∧ 𝑏 ∈ ( 𝐹𝐼 ) ) ) → ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
99 98 ralrimivva ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) ∧ 𝑥𝐵 ) → ∀ 𝑎 ∈ ( 𝐹𝐼 ) ∀ 𝑏 ∈ ( 𝐹𝐼 ) ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
100 99 ralrimiva ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ∀ 𝑥𝐵𝑎 ∈ ( 𝐹𝐼 ) ∀ 𝑏 ∈ ( 𝐹𝐼 ) ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) )
101 3 1 35 39 islidl ( ( 𝐹𝐼 ) ∈ 𝑈 ↔ ( ( 𝐹𝐼 ) ⊆ 𝐵 ∧ ( 𝐹𝐼 ) ≠ ∅ ∧ ∀ 𝑥𝐵𝑎 ∈ ( 𝐹𝐼 ) ∀ 𝑏 ∈ ( 𝐹𝐼 ) ( ( 𝑥 ( .r𝑆 ) 𝑎 ) ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝐼 ) ) )
102 8 20 100 101 syl3anbrc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵 ) ∧ 𝐼𝑇 ) → ( 𝐹𝐼 ) ∈ 𝑈 )
103 102 3impa ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = 𝐵𝐼𝑇 ) → ( 𝐹𝐼 ) ∈ 𝑈 )