Metamath Proof Explorer

Theorem rhmpreimacn

Description: The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of EGA, p. 83. Notice that the direction of the continuous map G is reverse: the original ring homomorphism F goes from R to S , but the continuous map G goes from B to A . This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024)

Ref Expression
Hypotheses rhmpreimacn.t ⊢ 𝑇 = ( Spec ‘ 𝑅 )
rhmpreimacn.u ⊢ 𝑈 = ( Spec ‘ 𝑆 )
rhmpreimacn.a ⊢ 𝐴 = ( PrmIdeal ‘ 𝑅 )
rhmpreimacn.b ⊢ 𝐵 = ( PrmIdeal ‘ 𝑆 )
rhmpreimacn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑇 )
rhmpreimacn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑈 )
rhmpreimacn.g ⊢ 𝐺 = ( 𝑖 ∈ 𝐵 ↦ ( ◡ 𝐹 “ 𝑖 ) )
rhmpreimacn.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rhmpreimacn.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
rhmpreimacn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
rhmpreimacn.1 ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑆 ) )
Assertion rhmpreimacn ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 rhmpreimacn.t ⊢ 𝑇 = ( Spec ‘ 𝑅 )
2 rhmpreimacn.u ⊢ 𝑈 = ( Spec ‘ 𝑆 )
3 rhmpreimacn.a ⊢ 𝐴 = ( PrmIdeal ‘ 𝑅 )
4 rhmpreimacn.b ⊢ 𝐵 = ( PrmIdeal ‘ 𝑆 )
5 rhmpreimacn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑇 )
6 rhmpreimacn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑈 )
7 rhmpreimacn.g ⊢ 𝐺 = ( 𝑖 ∈ 𝐵 ↦ ( ◡ 𝐹 “ 𝑖 ) )
8 rhmpreimacn.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 rhmpreimacn.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
10 rhmpreimacn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
11 rhmpreimacn.1 ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑆 ) )
12 2 6 4 zartopon ⊢ ( 𝑆 ∈ CRing → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
13 9 12 syl ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
14 1 5 3 zartopon ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ ( TopOn ‘ 𝐴 ) )
15 8 14 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐴 ) )
16 9 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑆 ∈ CRing )
17 10 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ 𝐵 )
19 18 4 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑆 ) )
20 3 rhmpreimaprmidl ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝑖 ) ∈ 𝐴 )
21 16 17 19 20 syl21anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → ( ◡ 𝐹 “ 𝑖 ) ∈ 𝐴 )
22 21 7 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
23 4 fvexi ⊢ 𝐵 ∈ V
24 23 rabex ⊢ { 𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘 } ∈ V
25 sseq1 ⊢ ( 𝑙 = 𝑗 → ( 𝑙 ⊆ 𝑘 ↔ 𝑗 ⊆ 𝑘 ) )
26 25 rabbidv ⊢ ( 𝑙 = 𝑗 → { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } = { 𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘 } )
27 26 cbvmptv ⊢ ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) = ( 𝑗 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘 } )
28 24 27 fnmpti ⊢ ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) Fn ( LIdeal ‘ 𝑆 )
29 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
30 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ran 𝐹 = ( Base ‘ 𝑆 ) )
31 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → 𝑎 ∈ ( LIdeal ‘ 𝑅 ) )
32 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
33 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
34 eqid ⊢ ( LIdeal ‘ 𝑆 ) = ( LIdeal ‘ 𝑆 )
35 32 33 34 rhmimaidl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = ( Base ‘ 𝑆 ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝐹 “ 𝑎 ) ∈ ( LIdeal ‘ 𝑆 ) )
36 29 30 31 35 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ( 𝐹 “ 𝑎 ) ∈ ( LIdeal ‘ 𝑆 ) )
37 fveqeq2 ⊢ ( 𝑏 = ( 𝐹 “ 𝑎 ) → ( ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑏 ) = ( ◡ 𝐺 “ 𝑥 ) ↔ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ ( 𝐹 “ 𝑎 ) ) = ( ◡ 𝐺 “ 𝑥 ) ) )
38 37 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) ∧ 𝑏 = ( 𝐹 “ 𝑎 ) ) → ( ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑏 ) = ( ◡ 𝐺 “ 𝑥 ) ↔ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ ( 𝐹 “ 𝑎 ) ) = ( ◡ 𝐺 “ 𝑥 ) ) )
39 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → 𝑅 ∈ CRing )
40 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → 𝑆 ∈ CRing )
41 25 rabbidv ⊢ ( 𝑙 = 𝑗 → { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } = { 𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘 } )
42 41 cbvmptv ⊢ ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) = ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘 } )
43 1 2 3 4 5 6 7 39 40 29 30 31 42 27 rhmpreimacnlem ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ ( 𝐹 “ 𝑎 ) ) = ( ◡ 𝐺 “ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) ) )
44 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 )
45 44 imaeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ( ◡ 𝐺 “ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) ) = ( ◡ 𝐺 “ 𝑥 ) )
46 43 45 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ ( 𝐹 “ 𝑎 ) ) = ( ◡ 𝐺 “ 𝑥 ) )
47 36 38 46 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) → ∃ 𝑏 ∈ ( LIdeal ‘ 𝑆 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑏 ) = ( ◡ 𝐺 “ 𝑥 ) )
48 3 fvexi ⊢ 𝐴 ∈ V
49 48 rabex ⊢ { 𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘 } ∈ V
50 49 42 fnmpti ⊢ ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) Fn ( LIdeal ‘ 𝑅 )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
52 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑅 ∈ CRing )
53 1 5 3 42 zartopn ⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ∧ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐽 ) ) )
54 53 simprd ⊢ ( 𝑅 ∈ CRing → ran ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐽 ) )
55 52 54 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ran ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐽 ) )
56 51 55 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) )
57 fvelrnb ⊢ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) Fn ( LIdeal ‘ 𝑅 ) → ( 𝑥 ∈ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ↔ ∃ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 ) )
58 57 biimpa ⊢ ( ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) Fn ( LIdeal ‘ 𝑅 ) ∧ 𝑥 ∈ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ) → ∃ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 )
59 50 56 58 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ∃ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑎 ) = 𝑥 )
60 47 59 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ∃ 𝑏 ∈ ( LIdeal ‘ 𝑆 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑏 ) = ( ◡ 𝐺 “ 𝑥 ) )
61 fvelrnb ⊢ ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) Fn ( LIdeal ‘ 𝑆 ) → ( ( ◡ 𝐺 “ 𝑥 ) ∈ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ↔ ∃ 𝑏 ∈ ( LIdeal ‘ 𝑆 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑏 ) = ( ◡ 𝐺 “ 𝑥 ) ) )
62 61 biimpar ⊢ ( ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) Fn ( LIdeal ‘ 𝑆 ) ∧ ∃ 𝑏 ∈ ( LIdeal ‘ 𝑆 ) ( ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) ‘ 𝑏 ) = ( ◡ 𝐺 “ 𝑥 ) ) → ( ◡ 𝐺 “ 𝑥 ) ∈ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) )
63 28 60 62 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ 𝐺 “ 𝑥 ) ∈ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) )
64 2 6 4 27 zartopn ⊢ ( 𝑆 ∈ CRing → ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐾 ) ) )
65 64 simprd ⊢ ( 𝑆 ∈ CRing → ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐾 ) )
66 9 65 syl ⊢ ( 𝜑 → ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐾 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ran ( 𝑙 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘 } ) = ( Clsd ‘ 𝐾 ) )
68 63 67 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ 𝐺 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
69 68 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ 𝐺 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
70 iscncl ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) → ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ 𝐺 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) ) )
71 70 biimpar ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) ∧ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ 𝐺 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
72 13 15 22 69 71 syl22anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )