Metamath Proof Explorer

Theorem rhmpreimaprmidl

Description: The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024)

Ref Expression
Hypothesis rhmpreimaprmidl.p ⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
Assertion rhmpreimaprmidl ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 rhmpreimaprmidl.p ⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
2 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
3 2 ad2antlr ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
4 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
5 prmidlidl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑆 ) )
6 4 5 sylan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑆 ) )
7 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
8 7 rhmpreimaidl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )
9 6 8 syldan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )
10 9 adantll ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )
11 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝑆 ∈ Ring )
12 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
14 12 13 prmidlnr ⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ≠ ( Base ‘ 𝑆 ) )
15 4 14 sylan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ≠ ( Base ‘ 𝑆 ) )
16 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
17 12 16 pridln1 ⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ∧ 𝐽 ≠ ( Base ‘ 𝑆 ) ) → ¬ ( 1r ‘ 𝑆 ) ∈ 𝐽 )
18 11 6 15 17 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ¬ ( 1r ‘ 𝑆 ) ∈ 𝐽 )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 19 16 rhm1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
21 20 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
22 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 22 12 rhmf ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
24 23 ffnd ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
25 24 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
26 22 19 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27 2 26 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
28 27 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) )
30 28 29 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
31 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ↔ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) ) )
32 31 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) )
33 25 30 32 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) )
34 33 simprd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 )
35 21 34 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) ∈ 𝐽 )
36 18 35 mtand ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ¬ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) )
37 36 neqned ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ≠ ( Base ‘ 𝑅 ) )
38 37 adantll ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ≠ ( Base ‘ 𝑅 ) )
39 simp-5l ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑆 ∈ CRing )
40 simp-4r ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) )
41 simp-5r ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
42 41 23 syl ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
43 simpllr ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
44 42 43 ffvelcdmd ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) )
45 simplr ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
46 42 45 ffvelcdmd ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
47 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
48 22 47 13 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
49 41 43 45 48 syl3anc ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
50 24 ad5antlr ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
51 simpr ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) )
52 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 ) ) )
53 52 simplbda ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑅 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 )
54 50 51 53 syl2anc ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 )
55 49 54 eqeltrrd ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝐽 )
56 12 13 prmidlc ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ∨ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) )
57 39 40 44 46 55 56 syl23anc ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ∨ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) )
58 50 adantr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
59 43 adantr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
60 simpr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 )
61 58 59 60 elpreimad ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) )
62 61 ex ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 → 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) )
63 50 adantr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
64 simpllr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
65 simpr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 )
66 63 64 65 elpreimad ⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) )
67 66 ex ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 → 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) )
68 62 67 orim12d ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ∨ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) )
69 57 68 mpd ⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) )
70 69 ex ⊢ ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) )
71 70 anasss ⊢ ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) )
72 71 ralrimivva ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ∀ 𝑎 ∈ ( Base ‘ 𝑅 ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) )
73 22 47 prmidl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( ◡ 𝐹 “ 𝐽 ) ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑅 ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( PrmIdeal ‘ 𝑅 ) )
74 3 10 38 72 73 syl22anc ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( PrmIdeal ‘ 𝑅 ) )
75 74 1 eleqtrrdi ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝑃 )