Metamath Proof Explorer


Theorem rhmpreimacnlem

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

Ref Expression
Hypotheses rhmpreimacn.t No typesetting found for |- T = ( Spec ` R ) with typecode |-
rhmpreimacn.u No typesetting found for |- U = ( Spec ` S ) with typecode |-
rhmpreimacn.a No typesetting found for |- A = ( PrmIdeal ` R ) with typecode |-
rhmpreimacn.b No typesetting found for |- B = ( PrmIdeal ` S ) with typecode |-
rhmpreimacn.j J = TopOpen T
rhmpreimacn.k K = TopOpen U
rhmpreimacn.g G = i B F -1 i
rhmpreimacn.r φ R CRing
rhmpreimacn.s φ S CRing
rhmpreimacn.f φ F R RingHom S
rhmpreimacn.1 φ ran F = Base S
rhmpreimacnlem.1 φ I LIdeal R
rhmpreimacnlem.v V = j LIdeal R k A | j k
rhmpreimacnlem.w W = j LIdeal S k B | j k
Assertion rhmpreimacnlem φ W F I = G -1 V I

Proof

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