Metamath Proof Explorer

Theorem prmidlsubm

Description: The complement of a prime ideal is multiplicatively closed. Converse of ssdifidlprm . (Contributed by Thierry Arnoux, 6-Jun-2026)

Ref Expression
Hypotheses prmidlsubm.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
prmidlsubm.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
prmidlsubm.3 ⊢ ( 𝜑 → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
Assertion prmidlsubm ( 𝜑 → ( 𝐵 ∖ 𝑃 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 prmidlsubm.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 prmidlsubm.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
3 prmidlsubm.3 ⊢ ( 𝜑 → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
4 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5 2 4 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
7 6 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
8 5 7 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
9 difss ⊢ ( 𝐵 ∖ 𝑃 ) ⊆ 𝐵
10 9 a1i ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑃 ) ⊆ 𝐵 )
11 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12 1 11 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
13 5 12 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
14 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃 ∈ ( LIdeal ‘ 𝑅 ) )
15 5 3 14 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ ( LIdeal ‘ 𝑅 ) )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 1 16 prmidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃 ≠ 𝐵 )
18 5 3 17 syl2anc ⊢ ( 𝜑 → 𝑃 ≠ 𝐵 )
19 1 11 pridln1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ) → ¬ ( 1r ‘ 𝑅 ) ∈ 𝑃 )
20 5 15 18 19 syl3anc ⊢ ( 𝜑 → ¬ ( 1r ‘ 𝑅 ) ∈ 𝑃 )
21 13 20 eldifd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑃 ) )
22 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → 𝑅 ∈ Ring )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) )
24 23 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → 𝑥 ∈ 𝐵 )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) )
26 25 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → 𝑦 ∈ 𝐵 )
27 1 16 22 24 26 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 )
28 23 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ¬ 𝑥 ∈ 𝑃 )
29 25 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ¬ 𝑦 ∈ 𝑃 )
30 28 29 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ( ¬ 𝑥 ∈ 𝑃 ∧ ¬ 𝑦 ∈ 𝑃 ) )
31 ioran ⊢ ( ¬ ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ↔ ( ¬ 𝑥 ∈ 𝑃 ∧ ¬ 𝑦 ∈ 𝑃 ) )
32 30 31 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ¬ ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) )
33 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → 𝑅 ∈ CRing )
34 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
35 24 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → 𝑥 ∈ 𝐵 )
36 26 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → 𝑦 ∈ 𝐵 )
37 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 )
38 1 16 33 34 35 36 37 prmidlprop ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) )
39 32 38 mtand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 )
40 27 39 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ 𝑃 ) )
41 40 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ 𝑃 ) )
42 41 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ 𝑃 ) )
43 6 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
44 6 11 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
45 6 16 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
46 43 44 45 issubm ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( ( 𝐵 ∖ 𝑃 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ↔ ( ( 𝐵 ∖ 𝑃 ) ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑃 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ 𝑃 ) ) ) )
47 46 biimpar ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( ( 𝐵 ∖ 𝑃 ) ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑃 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑃 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑃 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ 𝑃 ) ) ) → ( 𝐵 ∖ 𝑃 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
48 8 10 21 42 47 syl13anc ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑃 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )