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 imadmrn ⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
76 5 fdmd ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → dom 𝐹 = ( Base ‘ 𝑅 ) )
77 76 imaeq2d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ ( Base ‘ 𝑅 ) ) )
78 75 77 syl5reqr ⊢ ( 𝐹 ∈ ( 𝑅 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 𝐹 = 𝐵 ∧ 𝐼 ∈ 𝑇 ) → ( 𝐹 “ 𝐼 ) ∈ 𝑈 )