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 ffvelrnd ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ ( 𝐹𝐽 ) ) → ( 𝐹𝑎 ) ∈ ( Base ‘ 𝑆 ) )
45 simplr ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ ( 𝐹𝐽 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
46 42 45 ffvelrnd ( ( ( ( ( ( 𝑆 ∈ 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 ‘ 𝑆 ) ) → ( 𝐹𝐽 ) ∈ 𝑃 )