mxidlirred

Description: In a principal ideal domain, maximal ideals are exactly the ideals generated by irreducible elements. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	mxidlirred.b	$⊢ B = {Base}_{R}$
	mxidlirred.k	$⊢ K = RSpan (R)$
	mxidlirred.0	$⊢ \underset{˙}{0} = 0_{R}$
	mxidlirred.m	$⊢ M = K (\{X\})$
	mxidlirred.r	$⊢ φ \to R \in PID$
	mxidlirred.x	$⊢ φ \to X \in B$
	mxidlirred.y	$⊢ φ \to X \neq \underset{˙}{0}$
	mxidlirred.1	$⊢ φ \to M \in LIdeal (R)$
Assertion	mxidlirred	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow X \in Irred (R))$

Proof

Step	Hyp	Ref	Expression
1		mxidlirred.b	$⊢ B = {Base}_{R}$
2		mxidlirred.k	$⊢ K = RSpan (R)$
3		mxidlirred.0	$⊢ \underset{˙}{0} = 0_{R}$
4		mxidlirred.m	$⊢ M = K (\{X\})$
5		mxidlirred.r	$⊢ φ \to R \in PID$
6		mxidlirred.x	$⊢ φ \to X \in B$
7		mxidlirred.y	$⊢ φ \to X \neq \underset{˙}{0}$
8		mxidlirred.1	$⊢ φ \to M \in LIdeal (R)$
9		df-pid	$⊢ PID = IDomn \cap LPIR$
10	5 9	eleqtrdi	$⊢ φ \to R \in (IDomn \cap LPIR)$
11	10	elin1d	$⊢ φ \to R \in IDomn$
12	11	adantr	$⊢ (φ \land M \in MaxIdeal (R)) \to R \in IDomn$
13	6	adantr	$⊢ (φ \land M \in MaxIdeal (R)) \to X \in B$
14	7	adantr	$⊢ (φ \land M \in MaxIdeal (R)) \to X \neq \underset{˙}{0}$
15		simpr	$⊢ (φ \land M \in MaxIdeal (R)) \to M \in MaxIdeal (R)$
16	1 2 3 4 12 13 14 15	mxidlirredi	$⊢ (φ \land M \in MaxIdeal (R)) \to X \in Irred (R)$
17		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
18		simplr	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to x \in B$
19	18	ad2antrr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to x \in B$
20	6	ad8antr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to X \in B$
21		eqid	$⊢ Unit (R) = Unit (R)$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23	11	idomringd	$⊢ φ \to R \in Ring$
24	23	ad4antr	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to R \in Ring$
25	24	ad2antrr	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to R \in Ring$
26	25	ad2antrr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to R \in Ring$
27		simplr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to t \in B$
28		simpr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to X = t \cdot_{R} x$
29		simp-8r	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to X \in Irred (R)$
30	28 29	eqeltrrd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to t \cdot_{R} x \in Irred (R)$
31		eqid	$⊢ Irred (R) = Irred (R)$
32	31 1 21 22	irredmul	$⊢ (t \in B \land x \in B \land t \cdot_{R} x \in Irred (R)) \to (t \in Unit (R) \lor x \in Unit (R))$
33	27 19 30 32	syl3anc	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to (t \in Unit (R) \lor x \in Unit (R))$
34		simpr	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to k = K (\{x\})$
35	34	ad2antrr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to k = K (\{x\})$
36		simpr	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to \neg (M \subseteq k \to (k = M \lor k = B))$
37		annim	$⊢ (M \subseteq k \land \neg (k = M \lor k = B)) \leftrightarrow \neg (M \subseteq k \to (k = M \lor k = B))$
38	36 37	sylibr	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to (M \subseteq k \land \neg (k = M \lor k = B))$
39	38	simprd	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to \neg (k = M \lor k = B)$
40		ioran	$⊢ \neg (k = M \lor k = B) \leftrightarrow (\neg k = M \land \neg k = B)$
41	39 40	sylib	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to (\neg k = M \land \neg k = B)$
42	41	simprd	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to \neg k = B$
43	42	neqned	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to k \neq B$
44	43	ad4antr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to k \neq B$
45	35 44	eqnetrrd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to K (\{x\}) \neq B$
46	45	neneqd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to \neg K (\{x\}) = B$
47		eqid	$⊢ K (\{x\}) = K (\{x\})$
48	11	ad8antr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to R \in IDomn$
49	48	idomcringd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to R \in CRing$
50	21 2 47 1 19 49	unitpidl1	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to (K (\{x\}) = B \leftrightarrow x \in Unit (R))$
51	46 50	mtbid	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to \neg x \in Unit (R)$
52	33 51	olcnd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to t \in Unit (R)$
53	28	eqcomd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to t \cdot_{R} x = X$
54	1 2 17 19 20 21 22 26 52 53	dvdsruassoi	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to (x ∥_{r} (R) X \land X ∥_{r} (R) x)$
55	1 2 17 19 20 26	rspsnasso	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to ((x ∥_{r} (R) X \land X ∥_{r} (R) x) \leftrightarrow K (\{X\}) = K (\{x\}))$
56	54 55	mpbid	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to K (\{X\}) = K (\{x\})$
57	56 35	eqtr4d	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to K (\{X\}) = k$
58	4 57	eqtr2id	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to k = M$
59	41	simpld	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to \neg k = M$
60	59	ad4antr	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to \neg k = M$
61	58 60	pm2.21dd	$⊢ ((((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \land t \in B) \land X = t \cdot_{R} x) \to M \in MaxIdeal (R)$
62	38	simpld	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to M \subseteq k$
63	62	ad2antrr	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to M \subseteq k$
64	6	snssd	$⊢ φ \to \{X\} \subseteq B$
65	2 1	rspssid	$⊢ (R \in Ring \land \{X\} \subseteq B) \to \{X\} \subseteq K (\{X\})$
66	23 64 65	syl2anc	$⊢ φ \to \{X\} \subseteq K (\{X\})$
67	66 4	sseqtrrdi	$⊢ φ \to \{X\} \subseteq M$
68		snssg	$⊢ X \in B \to (X \in M \leftrightarrow \{X\} \subseteq M)$
69	68	biimpar	$⊢ (X \in B \land \{X\} \subseteq M) \to X \in M$
70	6 67 69	syl2anc	$⊢ φ \to X \in M$
71	70	ad6antr	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to X \in M$
72	63 71	sseldd	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to X \in k$
73	72 34	eleqtrd	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to X \in K (\{x\})$
74	1 22 2	elrspsn	$⊢ (R \in Ring \land x \in B) \to (X \in K (\{x\}) \leftrightarrow \exists t \in B X = t \cdot_{R} x)$
75	74	biimpa	$⊢ ((R \in Ring \land x \in B) \land X \in K (\{x\})) \to \exists t \in B X = t \cdot_{R} x$
76	25 18 73 75	syl21anc	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to \exists t \in B X = t \cdot_{R} x$
77	61 76	r19.29a	$⊢ ((((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \land x \in B) \land k = K (\{x\})) \to M \in MaxIdeal (R)$
78		simplr	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to k \in LIdeal (R)$
79	10	elin2d	$⊢ φ \to R \in LPIR$
80		eqid	$⊢ LPIdeal (R) = LPIdeal (R)$
81		eqid	$⊢ LIdeal (R) = LIdeal (R)$
82	80 81	islpir	$⊢ R \in LPIR \leftrightarrow (R \in Ring \land LIdeal (R) = LPIdeal (R))$
83	82	simprbi	$⊢ R \in LPIR \to LIdeal (R) = LPIdeal (R)$
84	79 83	syl	$⊢ φ \to LIdeal (R) = LPIdeal (R)$
85	84	ad4antr	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to LIdeal (R) = LPIdeal (R)$
86	78 85	eleqtrd	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to k \in LPIdeal (R)$
87	80 2 1	islpidl	$⊢ R \in Ring \to (k \in LPIdeal (R) \leftrightarrow \exists x \in B k = K (\{x\}))$
88	87	biimpa	$⊢ (R \in Ring \land k \in LPIdeal (R)) \to \exists x \in B k = K (\{x\})$
89	24 86 88	syl2anc	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to \exists x \in B k = K (\{x\})$
90	77 89	r19.29a	$⊢ ((((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \land k \in LIdeal (R)) \land \neg (M \subseteq k \to (k = M \lor k = B))) \to M \in MaxIdeal (R)$
91	8	ad2antrr	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to M \in LIdeal (R)$
92	31 21	irrednu	$⊢ X \in Irred (R) \to \neg X \in Unit (R)$
93	92	adantl	$⊢ (φ \land X \in Irred (R)) \to \neg X \in Unit (R)$
94	11	idomcringd	$⊢ φ \to R \in CRing$
95	21 2 4 1 6 94	unitpidl1	$⊢ φ \to (M = B \leftrightarrow X \in Unit (R))$
96	95	adantr	$⊢ (φ \land X \in Irred (R)) \to (M = B \leftrightarrow X \in Unit (R))$
97	96	necon3abid	$⊢ (φ \land X \in Irred (R)) \to (M \neq B \leftrightarrow \neg X \in Unit (R))$
98	93 97	mpbird	$⊢ (φ \land X \in Irred (R)) \to M \neq B$
99	98	adantr	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to M \neq B$
100	91 99	jca	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to (M \in LIdeal (R) \land M \neq B)$
101	1	ismxidl	$⊢ R \in Ring \to (M \in MaxIdeal (R) \leftrightarrow (M \in LIdeal (R) \land M \neq B \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))))$
102	23 101	syl	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow (M \in LIdeal (R) \land M \neq B \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))))$
103		df-3an	$⊢ (M \in LIdeal (R) \land M \neq B \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))) \leftrightarrow ((M \in LIdeal (R) \land M \neq B) \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B)))$
104	102 103	bitrdi	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow ((M \in LIdeal (R) \land M \neq B) \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))))$
105	104	notbid	$⊢ φ \to (\neg M \in MaxIdeal (R) \leftrightarrow \neg ((M \in LIdeal (R) \land M \neq B) \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))))$
106	105	biimpa	$⊢ (φ \land \neg M \in MaxIdeal (R)) \to \neg ((M \in LIdeal (R) \land M \neq B) \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B)))$
107	106	adantlr	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to \neg ((M \in LIdeal (R) \land M \neq B) \land \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B)))$
108	100 107	mpnanrd	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to \neg \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))$
109		rexnal	$⊢ \exists k \in LIdeal (R) \neg (M \subseteq k \to (k = M \lor k = B)) \leftrightarrow \neg \forall k \in LIdeal (R) (M \subseteq k \to (k = M \lor k = B))$
110	108 109	sylibr	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to \exists k \in LIdeal (R) \neg (M \subseteq k \to (k = M \lor k = B))$
111	90 110	r19.29a	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to M \in MaxIdeal (R)$
112	111	pm2.18da	$⊢ (φ \land X \in Irred (R)) \to M \in MaxIdeal (R)$
113	16 112	impbida	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow X \in Irred (R))$

Metamath Proof Explorer

Theorem mxidlirred

Proof