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	$⊢ φ \to M \in MaxIdeal (R)$
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	$⊢ φ \to M \in MaxIdeal (R)$
9	5	idomringd	$⊢ φ \to R \in Ring$
10	1	mxidlnr	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \neq B$
11	9 8 10	syl2anc	$⊢ φ \to M \neq B$
12		eqid	$⊢ Unit (R) = Unit (R)$
13	5	idomcringd	$⊢ φ \to R \in CRing$
14	12 2 4 1 6 13	unitpidl1	$⊢ φ \to (M = B \leftrightarrow X \in Unit (R))$
15	14	necon3abid	$⊢ φ \to (M \neq B \leftrightarrow \neg X \in Unit (R))$
16	11 15	mpbid	$⊢ φ \to \neg X \in Unit (R)$
17	6 16	eldifd	$⊢ φ \to X \in (B ∖ Unit (R))$
18	9	ad3antrrr	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to R \in Ring$
19	8	ad3antrrr	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to M \in MaxIdeal (R)$
20		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))$
21	20	eldifad	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in B$
22	21	snssd	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to \{g\} \subseteq B$
23		eqid	$⊢ LIdeal (R) = LIdeal (R)$
24	2 1 23	rspcl	$⊢ (R \in Ring \land \{g\} \subseteq B) \to K (\{g\}) \in LIdeal (R)$
25	18 22 24	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)$
26	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$
27	26	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$
28		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))$
29	28	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$
30		oveq1	$⊢ y = q \cdot_{R} f \to y \cdot_{R} g = (q \cdot_{R} f) \cdot_{R} g$
31	30	eqeq2d	$⊢ y = q \cdot_{R} f \to (x = y \cdot_{R} g \leftrightarrow x = (q \cdot_{R} f) \cdot_{R} g)$
32		eqid	$⊢ \cdot_{R} = \cdot_{R}$
33		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$
34		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))$
35	34	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$
36	1 32 27 33 35	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$
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 32 27 33 35 29	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	31 36 41	rspcedvdw	$⊢ ((((((φ \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 32 2	elrspsn	$⊢ (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	27 29 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 32 2	elrspsn	$⊢ (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	26 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	18 22 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	13	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$
61		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$
62		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))$
63	62	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$
64	18	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$
65	64	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$
66	1 32 65 61 63	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$
67		eqid	$⊢ 1_{R} = 1_{R}$
68	1 67 9	ringidcld	$⊢ φ \to 1_{R} \in B$
69	68	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$
70	21	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$
71		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}$
72	71	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}$
73		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$
74	64	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$
75	63	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$
76	1 32 3 74 75	ringrzd	$⊢ (((((((φ \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}$
77	72 73 76	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}$
78	7	neneqd	$⊢ φ \to \neg X = \underset{˙}{0}$
79	78	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}$
80	77 79	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}$
81	80	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}$
82	70 81	eldifsnd	$⊢ ((((((φ \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	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$
84	1 32 67 65 70	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$
85		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$
86	1 32 65 61 63 70	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)$
87		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$
88	87	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$
89	86 88	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$
90	84 85 89	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$
91	1 3 32 66 69 82 83 90	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}$
92	12 67	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
93	9 92	syl	$⊢ φ \to 1_{R} \in Unit (R)$
94	93	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)$
95	91 94	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)$
96	12 32 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)))$
97	96	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)$
98	60 61 63 95 97	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)$
99	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$
100		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$
101	100 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\})$
102	1 32 2	elrspsn	$⊢ (R \in Ring \land X \in B) \to (g \in K (\{X\}) \leftrightarrow \exists r \in B g = r \cdot_{R} X)$
103	102	biimpa	$⊢ ((R \in Ring \land X \in B) \land g \in K (\{X\})) \to \exists r \in B g = r \cdot_{R} X$
104	64 99 101 103	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$
105	98 104	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)$
106		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))$
107	106	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)$
108	105 107	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$
109	59 108	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)$
110	1 18 19 25 54 109	mxidlmaxv	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to K (\{g\}) = B$
111		eqid	$⊢ K (\{g\}) = K (\{g\})$
112	13	ad3antrrr	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to R \in CRing$
113	12 2 111 1 21 112	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))$
114	110 113	mpbid	$⊢ (((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \land f \cdot_{R} g = X) \to g \in Unit (R)$
115	20	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)$
116	114 115	pm2.65da	$⊢ ((φ \land f \in (B ∖ Unit (R))) \land g \in (B ∖ Unit (R))) \to \neg f \cdot_{R} g = X$
117	116	anasss	$⊢ (φ \land (f \in (B ∖ Unit (R)) \land g \in (B ∖ Unit (R)))) \to \neg f \cdot_{R} g = X$
118	117	neqned	$⊢ (φ \land (f \in (B ∖ Unit (R)) \land g \in (B ∖ Unit (R)))) \to f \cdot_{R} g \neq X$
119	118	ralrimivva	$⊢ φ \to \forall f \in (B ∖ Unit (R)) \forall g \in (B ∖ Unit (R)) f \cdot_{R} g \neq X$
120		eqid	$⊢ Irred (R) = Irred (R)$
121		eqid	$⊢ B ∖ Unit (R) = B ∖ Unit (R)$
122	1 12 120 121 32	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)$
123	17 119 122	sylanbrc	$⊢ φ \to X \in Irred (R)$

Metamath Proof Explorer

Theorem mxidlirredi

Proof