mxidlirredi

Description: In an integral domain, the generator of a maximal ideal is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	mxidlirredi.b	$⊢ B = {Base}_{R}$
	mxidlirredi.k	$⊢ K = RSpan (R)$
	mxidlirredi.0	$⊢ \underset{˙}{0} = 0_{R}$
	mxidlirredi.m	$⊢ M = K (\{X\})$
	mxidlirredi.r	$⊢ φ \to R \in IDomn$
	mxidlirredi.x	$⊢ φ \to X \in B$
	mxidlirredi.y	$⊢ φ \to X \neq \underset{˙}{0}$
	mxidlirredi.1	No typesetting found for \|- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode \|-
Assertion	mxidlirredi	$⊢ φ \to X \in Irred (R)$

Proof

Step	Hyp	Ref	Expression
1		mxidlirredi.b	$⊢ B = {Base}_{R}$
2		mxidlirredi.k	$⊢ K = RSpan (R)$
3		mxidlirredi.0	$⊢ \underset{˙}{0} = 0_{R}$
4		mxidlirredi.m	$⊢ M = K (\{X\})$
5		mxidlirredi.r	$⊢ φ \to R \in IDomn$
6		mxidlirredi.x	$⊢ φ \to X \in B$
7		mxidlirredi.y	$⊢ φ \to X \neq \underset{˙}{0}$
8		mxidlirredi.1	Could not format ( ph -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode \|-
9	5	idomringd	$⊢ φ \to R \in Ring$
10	1	mxidlnr	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) : No typesetting found for \|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) with typecode \|-
11	9 8 10	syl2anc	$⊢ φ \to M \neq B$
12		eqid	$⊢ Unit (R) = Unit (R)$
13	12 2 4 1 6 5	unitpidl1	$⊢ φ \to (M = B \leftrightarrow X \in Unit (R))$
14	13	necon3abid	$⊢ φ \to (M \neq B \leftrightarrow \neg X \in Unit (R))$
15	11 14	mpbid	$⊢ φ \to \neg X \in Unit (R)$
16	6 15	eldifd	$⊢ φ \to X \in (B ∖ Unit (R))$
17	9	ad3antrrr	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to R \in Ring$
18	8	ad3antrrr	Could not format ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> M e. ( MaxIdeal ` R ) ) with typecode \|-
19		simplr	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in (B ∖ Unit (R))$
20	19	eldifad	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in B$
21	20	snssd	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to \{g\} \subseteq B$
22		eqid	$⊢ LIdeal (R) = LIdeal (R)$
23	2 1 22	rspcl	$⊢ (R \in Ring \land \{g\} \subseteq B) \to K (\{g\}) \in LIdeal (R)$
24	17 21 23	syl2anc	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to K (\{g\}) \in LIdeal (R)$
25	9	ad4antr	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \to R \in Ring$
26	25	ad2antrr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to R \in Ring$
27		simp-5r	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to g \in (B ∖ Unit (R))$
28	27	eldifad	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to g \in B$
29		eqid	$⊢ \cdot_{R} = \cdot_{R}$
30		simplr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to q \in B$
31		simp-6r	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to f \in (B ∖ Unit (R))$
32	31	eldifad	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to f \in B$
33	1 29 26 30 32	ringcld	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to q \cdot_{R} f \in B$
34		oveq1	$⊢ y = q \cdot_{R} f \to y \cdot_{R} g = (q \cdot_{R} f) \cdot_{R} g$
35	34	eqeq2d	$⊢ y = q \cdot_{R} f \to (x = y \cdot_{R} g \leftrightarrow x = (q \cdot_{R} f) \cdot_{R} g)$
36	35	adantl	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \land y = q \cdot_{R} f) \to (x = y \cdot_{R} g \leftrightarrow x = (q \cdot_{R} f) \cdot_{R} g)$
37		simp-4r	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to f \cdot_{R} g = X$
38	37	oveq2d	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to q \cdot_{R} (f \cdot_{R} g) = q \cdot_{R} X$
39	1 29 26 30 32 28	ringassd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to (q \cdot_{R} f) \cdot_{R} g = q \cdot_{R} (f \cdot_{R} g)$
40		simpr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to x = q \cdot_{R} X$
41	38 39 40	3eqtr4rd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to x = (q \cdot_{R} f) \cdot_{R} g$
42	33 36 41	rspcedvd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to \exists y \in B x = y \cdot_{R} g$
43	1 29 2	rspsnel	$⊢ (R \in Ring \land g \in B) \to (x \in K (\{g\}) \leftrightarrow \exists y \in B x = y \cdot_{R} g)$
44	43	biimpar	$⊢ ((R \in Ring \land g \in B) \land \exists y \in B x = y \cdot_{R} g) \to x \in K (\{g\})$
45	26 28 42 44	syl21anc	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \land q \in B) \land x = q \cdot_{R} X) \to x \in K (\{g\})$
46	6	ad4antr	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \to X \in B$
47		simpr	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \to x \in M$
48	47 4	eleqtrdi	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \to x \in K (\{X\})$
49	1 29 2	rspsnel	$⊢ (R \in Ring \land X \in B) \to (x \in K (\{X\}) \leftrightarrow \exists q \in B x = q \cdot_{R} X)$
50	49	biimpa	$⊢ ((R \in Ring \land X \in B) \land x \in K (\{X\})) \to \exists q \in B x = q \cdot_{R} X$
51	25 46 48 50	syl21anc	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \to \exists q \in B x = q \cdot_{R} X$
52	45 51	r19.29a	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land x \in M) \to x \in K (\{g\})$
53	52	ex	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to (x \in M \to x \in K (\{g\}))$
54	53	ssrdv	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to M \subseteq K (\{g\})$
55	2 1	rspssid	$⊢ (R \in Ring \land \{g\} \subseteq B) \to \{g\} \subseteq K (\{g\})$
56		vex	$⊢ g \in V$
57	56	snss	$⊢ g \in K (\{g\}) \leftrightarrow \{g\} \subseteq K (\{g\})$
58	55 57	sylibr	$⊢ (R \in Ring \land \{g\} \subseteq B) \to g \in K (\{g\})$
59	17 21 58	syl2anc	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in K (\{g\})$
60		df-idom	$⊢ IDomn = CRing \cap Domn$
61	5 60	eleqtrdi	$⊢ φ \to R \in (CRing \cap Domn)$
62	61	elin1d	$⊢ φ \to R \in CRing$
63	62	ad6antr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to R \in CRing$
64		simplr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to r \in B$
65		simp-6r	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to f \in (B ∖ Unit (R))$
66	65	eldifad	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to f \in B$
67	20	ad3antrrr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to g \in B$
68		simpr	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to g = \underset{˙}{0}$
69	68	oveq2d	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to f \cdot_{R} g = f \cdot_{R} \underset{˙}{0}$
70		simp-5r	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to f \cdot_{R} g = X$
71	17	adantr	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to R \in Ring$
72	71	ad3antrrr	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to R \in Ring$
73	66	adantr	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to f \in B$
74	1 29 3	ringrz	$⊢ (R \in Ring \land f \in B) \to f \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
75	72 73 74	syl2anc	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to f \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
76	69 70 75	3eqtr3d	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to X = \underset{˙}{0}$
77	7	neneqd	$⊢ φ \to \neg X = \underset{˙}{0}$
78	77	ad7antr	$⊢ (((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \land g = \underset{˙}{0}) \to \neg X = \underset{˙}{0}$
79	76 78	pm2.65da	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to \neg g = \underset{˙}{0}$
80	79	neqned	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to g \neq \underset{˙}{0}$
81		eldifsn	$⊢ g \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (g \in B \land g \neq \underset{˙}{0})$
82	67 80 81	sylanbrc	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to g \in (B ∖ \{\underset{˙}{0}\})$
83	71	ad2antrr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to R \in Ring$
84	1 29 83 64 66	ringcld	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to r \cdot_{R} f \in B$
85		eqid	$⊢ 1_{R} = 1_{R}$
86	1 85	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
87	9 86	syl	$⊢ φ \to 1_{R} \in B$
88	87	ad6antr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to 1_{R} \in B$
89	5	ad6antr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to R \in IDomn$
90	1 29 85 83 67	ringlidmd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to 1_{R} \cdot_{R} g = g$
91		simpr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to g = r \cdot_{R} X$
92	1 29 83 64 66 67	ringassd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to (r \cdot_{R} f) \cdot_{R} g = r \cdot_{R} (f \cdot_{R} g)$
93		simp-4r	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to f \cdot_{R} g = X$
94	93	oveq2d	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to r \cdot_{R} (f \cdot_{R} g) = r \cdot_{R} X$
95	92 94	eqtr2d	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to r \cdot_{R} X = (r \cdot_{R} f) \cdot_{R} g$
96	90 91 95	3eqtrrd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to (r \cdot_{R} f) \cdot_{R} g = 1_{R} \cdot_{R} g$
97	1 3 29 82 84 88 89 96	idomrcan	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to r \cdot_{R} f = 1_{R}$
98	12 85	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
99	9 98	syl	$⊢ φ \to 1_{R} \in Unit (R)$
100	99	ad6antr	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to 1_{R} \in Unit (R)$
101	97 100	eqeltrd	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to r \cdot_{R} f \in Unit (R)$
102	12 29 1	unitmulclb	$⊢ (R \in CRing \land r \in B \land f \in B) \to (r \cdot_{R} f \in Unit (R) \leftrightarrow (r \in Unit (R) \land f \in Unit (R)))$
103	102	simplbda	$⊢ ((R \in CRing \land r \in B \land f \in B) \land r \cdot_{R} f \in Unit (R)) \to f \in Unit (R)$
104	63 64 66 101 103	syl31anc	$⊢ ((((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \land r \in B) \land g = r \cdot_{R} X) \to f \in Unit (R)$
105	6	ad4antr	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to X \in B$
106		simpr	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to g \in M$
107	106 4	eleqtrdi	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to g \in K (\{X\})$
108	1 29 2	rspsnel	$⊢ (R \in Ring \land X \in B) \to (g \in K (\{X\}) \leftrightarrow \exists r \in B g = r \cdot_{R} X)$
109	108	biimpa	$⊢ ((R \in Ring \land X \in B) \land g \in K (\{X\})) \to \exists r \in B g = r \cdot_{R} X$
110	71 105 107 109	syl21anc	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to \exists r \in B g = r \cdot_{R} X$
111	104 110	r19.29a	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to f \in Unit (R)$
112		simp-4r	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to f \in (B ∖ Unit (R))$
113	112	eldifbd	$⊢ ((((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \land g \in M) \to \neg f \in Unit (R)$
114	111 113	pm2.65da	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to \neg g \in M$
115	59 114	eldifd	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in (K (\{g\}) ∖ M)$
116	1 17 18 24 54 115	mxidlmaxv	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to K (\{g\}) = B$
117		eqid	$⊢ K (\{g\}) = K (\{g\})$
118	5	ad3antrrr	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to R \in IDomn$
119	12 2 117 1 20 118	unitpidl1	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to (K (\{g\}) = B \leftrightarrow g \in Unit (R))$
120	116 119	mpbid	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in Unit (R)$
121	19	eldifbd	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to \neg g \in Unit (R)$
122	120 121	pm2.65da	$⊢ ((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \to \neg f \cdot_{R} g = X$
123	122	anasss	$⊢ (φ \land (f \in (B ∖ Unit (R)) \land g \in (B ∖ Unit (R)))) \to \neg f \cdot_{R} g = X$
124	123	neqned	$⊢ (φ \land (f \in (B ∖ Unit (R)) \land g \in (B ∖ Unit (R)))) \to f \cdot_{R} g \neq X$
125	124	ralrimivva	$⊢ φ \to \forall f \in (B ∖ Unit (R)) \forall g \in (B ∖ Unit (R)) f \cdot_{R} g \neq X$
126		eqid	$⊢ Irred (R) = Irred (R)$
127		eqid	$⊢ B ∖ Unit (R) = B ∖ Unit (R)$
128	1 12 126 127 29	isirred	$⊢ X \in Irred (R) \leftrightarrow (X \in (B ∖ Unit (R)) \land \forall f \in (B ∖ Unit (R)) \forall g \in (B ∖ Unit (R)) f \cdot_{R} g \neq X)$
129	16 125 128	sylanbrc	$⊢ φ \to X \in Irred (R)$

Metamath Proof Explorer

Theorem mxidlirredi

Proof