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