Metamath Proof Explorer

Theorem rhmpreimacnlem

Description: Lemma for rhmpreimacn . (Contributed by Thierry Arnoux, 7-Jul-2024)

Ref Expression
Hypotheses rhmpreimacn.t 
|- T = ( Spec ` R )
rhmpreimacn.u 
|- U = ( Spec ` S )
rhmpreimacn.a 
|- A = ( PrmIdeal ` R )
rhmpreimacn.b 
|- B = ( PrmIdeal ` S )
rhmpreimacn.j 
|- J = ( TopOpen ` T )
rhmpreimacn.k 
|- K = ( TopOpen ` U )
rhmpreimacn.g 
|- G = ( i e. B |-> ( `' F " i ) )
rhmpreimacn.r 
|- ( ph -> R e. CRing )
rhmpreimacn.s 
|- ( ph -> S e. CRing )
rhmpreimacn.f 
|- ( ph -> F e. ( R RingHom S ) )
rhmpreimacn.1 
|- ( ph -> ran F = ( Base ` S ) )
rhmpreimacnlem.1 
|- ( ph -> I e. ( LIdeal ` R ) )
rhmpreimacnlem.v 
|- V = ( j e. ( LIdeal ` R ) |-> { k e. A | j C_ k } )
rhmpreimacnlem.w 
|- W = ( j e. ( LIdeal ` S ) |-> { k e. B | j C_ k } )
Assertion rhmpreimacnlem 
|- ( ph -> ( W ` ( F " I ) ) = ( `' G " ( V ` I ) ) )

Proof

Step Hyp Ref Expression
1 rhmpreimacn.t 
 |-  T = ( Spec ` R )
2 rhmpreimacn.u 
 |-  U = ( Spec ` S )
3 rhmpreimacn.a 
 |-  A = ( PrmIdeal ` R )
4 rhmpreimacn.b 
 |-  B = ( PrmIdeal ` S )
5 rhmpreimacn.j 
 |-  J = ( TopOpen ` T )
6 rhmpreimacn.k 
 |-  K = ( TopOpen ` U )
7 rhmpreimacn.g 
 |-  G = ( i e. B |-> ( `' F " i ) )
8 rhmpreimacn.r 
 |-  ( ph -> R e. CRing )
9 rhmpreimacn.s 
 |-  ( ph -> S e. CRing )
10 rhmpreimacn.f 
 |-  ( ph -> F e. ( R RingHom S ) )
11 rhmpreimacn.1 
 |-  ( ph -> ran F = ( Base ` S ) )
12 rhmpreimacnlem.1 
 |-  ( ph -> I e. ( LIdeal ` R ) )
13 rhmpreimacnlem.v 
 |-  V = ( j e. ( LIdeal ` R ) |-> { k e. A | j C_ k } )
14 rhmpreimacnlem.w 
 |-  W = ( j e. ( LIdeal ` S ) |-> { k e. B | j C_ k } )
15 imaeq2 
 |-  ( i = g -> ( `' F " i ) = ( `' F " g ) )
16 simpr 
 |-  ( ( ph /\ g e. B ) -> g e. B )
17 10 elexd 
 |-  ( ph -> F e. _V )
18 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
19 imaexg 
 |-  ( `' F e. _V -> ( `' F " g ) e. _V )
20 17 18 19 3syl 
 |-  ( ph -> ( `' F " g ) e. _V )
21 20 adantr 
 |-  ( ( ph /\ g e. B ) -> ( `' F " g ) e. _V )
22 7 15 16 21 fvmptd3 
 |-  ( ( ph /\ g e. B ) -> ( G ` g ) = ( `' F " g ) )
23 22 eleq1d 
 |-  ( ( ph /\ g e. B ) -> ( ( G ` g ) e. ( V ` I ) <-> ( `' F " g ) e. ( V ` I ) ) )
24 23 pm5.32da 
 |-  ( ph -> ( ( g e. B /\ ( G ` g ) e. ( V ` I ) ) <-> ( g e. B /\ ( `' F " g ) e. ( V ` I ) ) ) )
25 9 adantr 
 |-  ( ( ph /\ i e. B ) -> S e. CRing )
26 10 adantr 
 |-  ( ( ph /\ i e. B ) -> F e. ( R RingHom S ) )
27 simpr 
 |-  ( ( ph /\ i e. B ) -> i e. B )
28 27 4 eleqtrdi 
 |-  ( ( ph /\ i e. B ) -> i e. ( PrmIdeal ` S ) )
29 3 rhmpreimaprmidl 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ i e. ( PrmIdeal ` S ) ) -> ( `' F " i ) e. A )
30 25 26 28 29 syl21anc 
 |-  ( ( ph /\ i e. B ) -> ( `' F " i ) e. A )
31 30 7 fmptd 
 |-  ( ph -> G : B --> A )
32 31 ffnd 
 |-  ( ph -> G Fn B )
33 elpreima 
 |-  ( G Fn B -> ( g e. ( `' G " ( V ` I ) ) <-> ( g e. B /\ ( G ` g ) e. ( V ` I ) ) ) )
34 32 33 syl 
 |-  ( ph -> ( g e. ( `' G " ( V ` I ) ) <-> ( g e. B /\ ( G ` g ) e. ( V ` I ) ) ) )
35 sseq1 
 |-  ( j = ( F " I ) -> ( j C_ k <-> ( F " I ) C_ k ) )
36 35 rabbidv 
 |-  ( j = ( F " I ) -> { k e. B | j C_ k } = { k e. B | ( F " I ) C_ k } )
37 eqid 
 |-  ( Base ` S ) = ( Base ` S )
38 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
39 eqid 
 |-  ( LIdeal ` S ) = ( LIdeal ` S )
40 37 38 39 rhmimaidl 
 |-  ( ( F e. ( R RingHom S ) /\ ran F = ( Base ` S ) /\ I e. ( LIdeal ` R ) ) -> ( F " I ) e. ( LIdeal ` S ) )
41 10 11 12 40 syl3anc 
 |-  ( ph -> ( F " I ) e. ( LIdeal ` S ) )
42 4 fvexi 
 |-  B e. _V
43 42 rabex 
 |-  { k e. B | ( F " I ) C_ k } e. _V
44 43 a1i 
 |-  ( ph -> { k e. B | ( F " I ) C_ k } e. _V )
45 14 36 41 44 fvmptd3 
 |-  ( ph -> ( W ` ( F " I ) ) = { k e. B | ( F " I ) C_ k } )
46 45 eleq2d 
 |-  ( ph -> ( g e. ( W ` ( F " I ) ) <-> g e. { k e. B | ( F " I ) C_ k } ) )
47 sseq2 
 |-  ( k = g -> ( ( F " I ) C_ k <-> ( F " I ) C_ g ) )
48 47 elrab 
 |-  ( g e. { k e. B | ( F " I ) C_ k } <-> ( g e. B /\ ( F " I ) C_ g ) )
49 46 48 bitrdi 
 |-  ( ph -> ( g e. ( W ` ( F " I ) ) <-> ( g e. B /\ ( F " I ) C_ g ) ) )
50 eqid 
 |-  ( Base ` R ) = ( Base ` R )
51 50 37 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> ( Base ` S ) )
52 10 51 syl 
 |-  ( ph -> F : ( Base ` R ) --> ( Base ` S ) )
53 52 ffund 
 |-  ( ph -> Fun F )
54 50 38 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ ( Base ` R ) )
55 12 54 syl 
 |-  ( ph -> I C_ ( Base ` R ) )
56 52 fdmd 
 |-  ( ph -> dom F = ( Base ` R ) )
57 55 56 sseqtrrd 
 |-  ( ph -> I C_ dom F )
58 funimass3 
 |-  ( ( Fun F /\ I C_ dom F ) -> ( ( F " I ) C_ g <-> I C_ ( `' F " g ) ) )
59 53 57 58 syl2anc 
 |-  ( ph -> ( ( F " I ) C_ g <-> I C_ ( `' F " g ) ) )
60 59 anbi2d 
 |-  ( ph -> ( ( g e. B /\ ( F " I ) C_ g ) <-> ( g e. B /\ I C_ ( `' F " g ) ) ) )
61 9 adantr 
 |-  ( ( ph /\ g e. B ) -> S e. CRing )
62 10 adantr 
 |-  ( ( ph /\ g e. B ) -> F e. ( R RingHom S ) )
63 16 4 eleqtrdi 
 |-  ( ( ph /\ g e. B ) -> g e. ( PrmIdeal ` S ) )
64 3 rhmpreimaprmidl 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ g e. ( PrmIdeal ` S ) ) -> ( `' F " g ) e. A )
65 61 62 63 64 syl21anc 
 |-  ( ( ph /\ g e. B ) -> ( `' F " g ) e. A )
66 65 biantrurd 
 |-  ( ( ph /\ g e. B ) -> ( I C_ ( `' F " g ) <-> ( ( `' F " g ) e. A /\ I C_ ( `' F " g ) ) ) )
67 66 pm5.32da 
 |-  ( ph -> ( ( g e. B /\ I C_ ( `' F " g ) ) <-> ( g e. B /\ ( ( `' F " g ) e. A /\ I C_ ( `' F " g ) ) ) ) )
68 49 60 67 3bitrd 
 |-  ( ph -> ( g e. ( W ` ( F " I ) ) <-> ( g e. B /\ ( ( `' F " g ) e. A /\ I C_ ( `' F " g ) ) ) ) )
69 sseq2 
 |-  ( k = ( `' F " g ) -> ( I C_ k <-> I C_ ( `' F " g ) ) )
70 69 elrab 
 |-  ( ( `' F " g ) e. { k e. A | I C_ k } <-> ( ( `' F " g ) e. A /\ I C_ ( `' F " g ) ) )
71 70 anbi2i 
 |-  ( ( g e. B /\ ( `' F " g ) e. { k e. A | I C_ k } ) <-> ( g e. B /\ ( ( `' F " g ) e. A /\ I C_ ( `' F " g ) ) ) )
72 68 71 bitr4di 
 |-  ( ph -> ( g e. ( W ` ( F " I ) ) <-> ( g e. B /\ ( `' F " g ) e. { k e. A | I C_ k } ) ) )
73 sseq1 
 |-  ( j = I -> ( j C_ k <-> I C_ k ) )
74 73 rabbidv 
 |-  ( j = I -> { k e. A | j C_ k } = { k e. A | I C_ k } )
75 3 fvexi 
 |-  A e. _V
76 75 rabex 
 |-  { k e. A | I C_ k } e. _V
77 76 a1i 
 |-  ( ph -> { k e. A | I C_ k } e. _V )
78 13 74 12 77 fvmptd3 
 |-  ( ph -> ( V ` I ) = { k e. A | I C_ k } )
79 78 eleq2d 
 |-  ( ph -> ( ( `' F " g ) e. ( V ` I ) <-> ( `' F " g ) e. { k e. A | I C_ k } ) )
80 79 anbi2d 
 |-  ( ph -> ( ( g e. B /\ ( `' F " g ) e. ( V ` I ) ) <-> ( g e. B /\ ( `' F " g ) e. { k e. A | I C_ k } ) ) )
81 72 80 bitr4d 
 |-  ( ph -> ( g e. ( W ` ( F " I ) ) <-> ( g e. B /\ ( `' F " g ) e. ( V ` I ) ) ) )
82 24 34 81 3bitr4rd 
 |-  ( ph -> ( g e. ( W ` ( F " I ) ) <-> g e. ( `' G " ( V ` I ) ) ) )
83 82 eqrdv 
 |-  ( ph -> ( W ` ( F " I ) ) = ( `' G " ( V ` I ) ) )