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 
|- B = ( Base ` R )
prmidlsubm.2 
|- ( ph -> R e. CRing )
prmidlsubm.3 
|- ( ph -> P e. ( PrmIdeal ` R ) )
Assertion prmidlsubm 
|- ( ph -> ( B \ P ) e. ( SubMnd ` ( mulGrp ` R ) ) )

Proof

Step Hyp Ref Expression
1 prmidlsubm.1 
 |-  B = ( Base ` R )
2 prmidlsubm.2 
 |-  ( ph -> R e. CRing )
3 prmidlsubm.3 
 |-  ( ph -> P e. ( PrmIdeal ` R ) )
4 crngring 
 |-  ( R e. CRing -> R e. Ring )
5 2 4 syl 
 |-  ( ph -> R e. Ring )
6 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
7 6 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
8 5 7 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
9 difss 
 |-  ( B \ P ) C_ B
10 9 a1i 
 |-  ( ph -> ( B \ P ) C_ B )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 1 11 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
13 5 12 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
14 prmidlidl 
 |-  ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) )
15 5 3 14 syl2anc 
 |-  ( ph -> P e. ( LIdeal ` R ) )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 1 16 prmidlnr 
 |-  ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P =/= B )
18 5 3 17 syl2anc 
 |-  ( ph -> P =/= B )
19 1 11 pridln1 
 |-  ( ( R e. Ring /\ P e. ( LIdeal ` R ) /\ P =/= B ) -> -. ( 1r ` R ) e. P )
20 5 15 18 19 syl3anc 
 |-  ( ph -> -. ( 1r ` R ) e. P )
21 13 20 eldifd 
 |-  ( ph -> ( 1r ` R ) e. ( B \ P ) )
22 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> R e. Ring )
23 simplr 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> x e. ( B \ P ) )
24 23 eldifad 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> x e. B )
25 simpr 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> y e. ( B \ P ) )
26 25 eldifad 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> y e. B )
27 1 16 22 24 26 ringcld 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> ( x ( .r ` R ) y ) e. B )
28 23 eldifbd 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> -. x e. P )
29 25 eldifbd 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> -. y e. P )
30 28 29 jca 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> ( -. x e. P /\ -. y e. P ) )
31 ioran 
 |-  ( -. ( x e. P \/ y e. P ) <-> ( -. x e. P /\ -. y e. P ) )
32 30 31 sylibr 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> -. ( x e. P \/ y e. P ) )
33 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) /\ ( x ( .r ` R ) y ) e. P ) -> R e. CRing )
34 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) /\ ( x ( .r ` R ) y ) e. P ) -> P e. ( PrmIdeal ` R ) )
35 24 adantr 
 |-  ( ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) /\ ( x ( .r ` R ) y ) e. P ) -> x e. B )
36 26 adantr 
 |-  ( ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) /\ ( x ( .r ` R ) y ) e. P ) -> y e. B )
37 simpr 
 |-  ( ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) /\ ( x ( .r ` R ) y ) e. P ) -> ( x ( .r ` R ) y ) e. P )
38 1 16 33 34 35 36 37 prmidlprop 
 |-  ( ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) /\ ( x ( .r ` R ) y ) e. P ) -> ( x e. P \/ y e. P ) )
39 32 38 mtand 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> -. ( x ( .r ` R ) y ) e. P )
40 27 39 eldifd 
 |-  ( ( ( ph /\ x e. ( B \ P ) ) /\ y e. ( B \ P ) ) -> ( x ( .r ` R ) y ) e. ( B \ P ) )
41 40 anasss 
 |-  ( ( ph /\ ( x e. ( B \ P ) /\ y e. ( B \ P ) ) ) -> ( x ( .r ` R ) y ) e. ( B \ P ) )
42 41 ralrimivva 
 |-  ( ph -> A. x e. ( B \ P ) A. y e. ( B \ P ) ( x ( .r ` R ) y ) e. ( B \ P ) )
43 6 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
44 6 11 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
45 6 16 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
46 43 44 45 issubm 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( ( B \ P ) e. ( SubMnd ` ( mulGrp ` R ) ) <-> ( ( B \ P ) C_ B /\ ( 1r ` R ) e. ( B \ P ) /\ A. x e. ( B \ P ) A. y e. ( B \ P ) ( x ( .r ` R ) y ) e. ( B \ P ) ) ) )
47 46 biimpar 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ ( ( B \ P ) C_ B /\ ( 1r ` R ) e. ( B \ P ) /\ A. x e. ( B \ P ) A. y e. ( B \ P ) ( x ( .r ` R ) y ) e. ( B \ P ) ) ) -> ( B \ P ) e. ( SubMnd ` ( mulGrp ` R ) ) )
48 8 10 21 42 47 syl13anc 
 |-  ( ph -> ( B \ P ) e. ( SubMnd ` ( mulGrp ` R ) ) )