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 
|- B = ( Base ` S )
rhmimaidl.t 
|- T = ( LIdeal ` R )
rhmimaidl.u 
|- U = ( LIdeal ` S )
Assertion rhmimaidl 
|- ( ( F e. ( R RingHom S ) /\ ran F = B /\ I e. T ) -> ( F " I ) e. U )

Proof

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