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	$⊢ φ \to R \in CRing$
	prmidlsubm.3	$⊢ φ \to P \in PrmIdeal (R)$
Assertion	prmidlsubm	$⊢ φ \to B ∖ P \in SubMnd ({mulGrp}_{R})$

Proof

Step	Hyp	Ref	Expression
1		prmidlsubm.1	$⊢ B = {Base}_{R}$
2		prmidlsubm.2	$⊢ φ \to R \in CRing$
3		prmidlsubm.3	$⊢ φ \to P \in PrmIdeal (R)$
4		crngring	$⊢ R \in CRing \to R \in Ring$
5	2 4	syl	$⊢ φ \to R \in Ring$
6		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
7	6	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
8	5 7	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
9		difss	$⊢ B ∖ P \subseteq B$
10	9	a1i	$⊢ φ \to B ∖ P \subseteq B$
11		eqid	$⊢ 1_{R} = 1_{R}$
12	1 11	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
13	5 12	syl	$⊢ φ \to 1_{R} \in B$
14		prmidlidl	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to P \in LIdeal (R)$
15	5 3 14	syl2anc	$⊢ φ \to P \in LIdeal (R)$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	1 16	prmidlnr	$⊢ (R \in Ring \land P \in PrmIdeal (R)) \to P \neq B$
18	5 3 17	syl2anc	$⊢ φ \to P \neq B$
19	1 11	pridln1	$⊢ (R \in Ring \land P \in LIdeal (R) \land P \neq B) \to \neg 1_{R} \in P$
20	5 15 18 19	syl3anc	$⊢ φ \to \neg 1_{R} \in P$
21	13 20	eldifd	$⊢ φ \to 1_{R} \in (B ∖ P)$
22	5	ad2antrr	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to R \in Ring$
23		simplr	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to x \in (B ∖ P)$
24	23	eldifad	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to x \in B$
25		simpr	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to y \in (B ∖ P)$
26	25	eldifad	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to y \in B$
27	1 16 22 24 26	ringcld	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to x \cdot_{R} y \in B$
28	23	eldifbd	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to \neg x \in P$
29	25	eldifbd	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to \neg y \in P$
30	28 29	jca	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to (\neg x \in P \land \neg y \in P)$
31		ioran	$⊢ \neg (x \in P \lor y \in P) \leftrightarrow (\neg x \in P \land \neg y \in P)$
32	30 31	sylibr	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to \neg (x \in P \lor y \in P)$
33	2	ad3antrrr	$⊢ (((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \land x \cdot_{R} y \in P) \to R \in CRing$
34	3	ad3antrrr	$⊢ (((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \land x \cdot_{R} y \in P) \to P \in PrmIdeal (R)$
35	24	adantr	$⊢ (((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \land x \cdot_{R} y \in P) \to x \in B$
36	26	adantr	$⊢ (((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \land x \cdot_{R} y \in P) \to y \in B$
37		simpr	$⊢ (((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \land x \cdot_{R} y \in P) \to x \cdot_{R} y \in P$
38	1 16 33 34 35 36 37	prmidlprop	$⊢ (((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \land x \cdot_{R} y \in P) \to (x \in P \lor y \in P)$
39	32 38	mtand	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to \neg x \cdot_{R} y \in P$
40	27 39	eldifd	$⊢ ((φ \land x \in (B ∖ P)) \land y \in (B ∖ P)) \to x \cdot_{R} y \in (B ∖ P)$
41	40	anasss	$⊢ (φ \land (x \in (B ∖ P) \land y \in (B ∖ P))) \to x \cdot_{R} y \in (B ∖ P)$
42	41	ralrimivva	$⊢ φ \to \forall x \in (B ∖ P) \forall y \in (B ∖ P) x \cdot_{R} y \in (B ∖ P)$
43	6 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
44	6 11	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
45	6 16	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
46	43 44 45	issubm	$⊢ {mulGrp}_{R} \in Mnd \to (B ∖ P \in SubMnd ({mulGrp}_{R}) \leftrightarrow (B ∖ P \subseteq B \land 1_{R} \in (B ∖ P) \land \forall x \in (B ∖ P) \forall y \in (B ∖ P) x \cdot_{R} y \in (B ∖ P)))$
47	46	biimpar	$⊢ ({mulGrp}_{R} \in Mnd \land (B ∖ P \subseteq B \land 1_{R} \in (B ∖ P) \land \forall x \in (B ∖ P) \forall y \in (B ∖ P) x \cdot_{R} y \in (B ∖ P))) \to B ∖ P \in SubMnd ({mulGrp}_{R})$
48	8 10 21 42 47	syl13anc	$⊢ φ \to B ∖ P \in SubMnd ({mulGrp}_{R})$

Metamath Proof Explorer

Theorem prmidlsubm

Proof