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	21 2 47 1 19 48	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))$
50	46 49	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)$
51	33 50	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)$
52	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$
53	1 2 17 19 20 21 22 26 51 52	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)$
54	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\}))$
55	53 54	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\})$
56	55 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$
57	4 56	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$
58	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$
59	58	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$
60	57 59	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)$
61	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$
62	61	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$
63	6	snssd	$⊢ φ \to \{X\} \subseteq B$
64	2 1	rspssid	$⊢ (R \in Ring \land \{X\} \subseteq B) \to \{X\} \subseteq K (\{X\})$
65	23 63 64	syl2anc	$⊢ φ \to \{X\} \subseteq K (\{X\})$
66	65 4	sseqtrrdi	$⊢ φ \to \{X\} \subseteq M$
67		snssg	$⊢ X \in B \to (X \in M \leftrightarrow \{X\} \subseteq M)$
68	67	biimpar	$⊢ (X \in B \land \{X\} \subseteq M) \to X \in M$
69	6 66 68	syl2anc	$⊢ φ \to X \in M$
70	69	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$
71	62 70	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$
72	71 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\})$
73	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)$
74	73	biimpa	$⊢ ((R \in Ring \land x \in B) \land X \in K (\{x\})) \to \exists t \in B X = t \cdot_{R} x$
75	25 18 72 74	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$
76	60 75	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)$
77		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)$
78	10	elin2d	$⊢ φ \to R \in LPIR$
79		eqid	$⊢ LPIdeal (R) = LPIdeal (R)$
80		eqid	$⊢ LIdeal (R) = LIdeal (R)$
81	79 80	islpir	$⊢ R \in LPIR \leftrightarrow (R \in Ring \land LIdeal (R) = LPIdeal (R))$
82	81	simprbi	$⊢ R \in LPIR \to LIdeal (R) = LPIdeal (R)$
83	78 82	syl	$⊢ φ \to LIdeal (R) = LPIdeal (R)$
84	83	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)$
85	77 84	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)$
86	79 2 1	islpidl	$⊢ R \in Ring \to (k \in LPIdeal (R) \leftrightarrow \exists x \in B k = K (\{x\}))$
87	86	biimpa	$⊢ (R \in Ring \land k \in LPIdeal (R)) \to \exists x \in B k = K (\{x\})$
88	24 85 87	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\})$
89	76 88	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)$
90	8	ad2antrr	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to M \in LIdeal (R)$
91	31 21	irrednu	$⊢ X \in Irred (R) \to \neg X \in Unit (R)$
92	91	adantl	$⊢ (φ \land X \in Irred (R)) \to \neg X \in Unit (R)$
93	21 2 4 1 6 11	unitpidl1	$⊢ φ \to (M = B \leftrightarrow X \in Unit (R))$
94	93	adantr	$⊢ (φ \land X \in Irred (R)) \to (M = B \leftrightarrow X \in Unit (R))$
95	94	necon3abid	$⊢ (φ \land X \in Irred (R)) \to (M \neq B \leftrightarrow \neg X \in Unit (R))$
96	92 95	mpbird	$⊢ (φ \land X \in Irred (R)) \to M \neq B$
97	96	adantr	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to M \neq B$
98	90 97	jca	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to (M \in LIdeal (R) \land M \neq B)$
99	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))))$
100	23 99	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))))$
101		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)))$
102	100 101	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))))$
103	102	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))))$
104	103	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)))$
105	104	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)))$
106	98 105	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))$
107		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))$
108	106 107	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))$
109	89 108	r19.29a	$⊢ ((φ \land X \in Irred (R)) \land \neg M \in MaxIdeal (R)) \to M \in MaxIdeal (R)$
110	109	pm2.18da	$⊢ (φ \land X \in Irred (R)) \to M \in MaxIdeal (R)$
111	16 110	impbida	$⊢ φ \to (M \in MaxIdeal (R) \leftrightarrow X \in Irred (R))$

Metamath Proof Explorer

Theorem mxidlirred

Proof