1arithufdlem4

Description: Lemma for 1arithufd . Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	1arithufd.b	$⊢ B = {Base}_{R}$
	1arithufd.0	$⊢ \underset{˙}{0} = 0_{R}$
	1arithufd.u	$⊢ U = Unit (R)$
	1arithufd.p	$⊢ P = RPrime (R)$
	1arithufd.m	$⊢ M = {mulGrp}_{R}$
	1arithufd.r	$⊢ φ \to R \in UFD$
	1arithufdlem.2	$⊢ φ \to \neg R \in DivRing$
	1arithufdlem.s	$⊢ S = \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
	1arithufdlem.3	$⊢ φ \to X \in B$
	1arithufdlem.4	$⊢ φ \to \neg X \in U$
	1arithufdlem.5	$⊢ φ \to X \neq \underset{˙}{0}$
Assertion	1arithufdlem4	$⊢ φ \to X \in S$

Proof

Step	Hyp	Ref	Expression
1		1arithufd.b	$⊢ B = {Base}_{R}$
2		1arithufd.0	$⊢ \underset{˙}{0} = 0_{R}$
3		1arithufd.u	$⊢ U = Unit (R)$
4		1arithufd.p	$⊢ P = RPrime (R)$
5		1arithufd.m	$⊢ M = {mulGrp}_{R}$
6		1arithufd.r	$⊢ φ \to R \in UFD$
7		1arithufdlem.2	$⊢ φ \to \neg R \in DivRing$
8		1arithufdlem.s	$⊢ S = \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
9		1arithufdlem.3	$⊢ φ \to X \in B$
10		1arithufdlem.4	$⊢ φ \to \neg X \in U$
11		1arithufdlem.5	$⊢ φ \to X \neq \underset{˙}{0}$
12		eqeq1	$⊢ x = a \to (x = \sum_{M} f \leftrightarrow a = \sum_{M} f)$
13	12	rexbidv	$⊢ x = a \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P a = \sum_{M} f)$
14		eqcom	$⊢ a = \sum_{M} f \leftrightarrow \sum_{M} f = a$
15	14	rexbii	$⊢ \exists f \in Word P a = \sum_{M} f \leftrightarrow \exists f \in Word P \sum_{M} f = a$
16	13 15	bitrdi	$⊢ x = a \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P \sum_{M} f = a)$
17	6	adantr	$⊢ (φ \land a \in P) \to R \in UFD$
18		simpr	$⊢ (φ \land a \in P) \to a \in P$
19	1 4 17 18	rprmcl	$⊢ (φ \land a \in P) \to a \in B$
20		oveq2	$⊢ f = ⟨“ a ”⟩ \to \sum_{M} f = \sum_{M} ⟨“ a ”⟩$
21	20	eqeq1d	$⊢ f = ⟨“ a ”⟩ \to (\sum_{M} f = a \leftrightarrow \sum_{M} ⟨“ a ”⟩ = a)$
22	18	s1cld	$⊢ (φ \land a \in P) \to ⟨“ a ”⟩ \in Word P$
23	5 1	mgpbas	$⊢ B = {Base}_{M}$
24	23	gsumws1	$⊢ a \in B \to \sum_{M} ⟨“ a ”⟩ = a$
25	19 24	syl	$⊢ (φ \land a \in P) \to \sum_{M} ⟨“ a ”⟩ = a$
26	21 22 25	rspcedvdw	$⊢ (φ \land a \in P) \to \exists f \in Word P \sum_{M} f = a$
27	16 19 26	elrabd	$⊢ (φ \land a \in P) \to a \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
28	27 8	eleqtrrdi	$⊢ (φ \land a \in P) \to a \in S$
29	28	ex	$⊢ φ \to (a \in P \to a \in S)$
30	29	ssrdv	$⊢ φ \to P \subseteq S$
31	30	adantr	$⊢ (φ \land \neg X \in S) \to P \subseteq S$
32		anass	$⊢ (((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \leftrightarrow ((φ \land \neg X \in S) \land (i \in LIdeal (R) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)))$
33		ineq2	$⊢ p = i \to S \cap p = S \cap i$
34	33	eqeq1d	$⊢ p = i \to (S \cap p = \emptyset \leftrightarrow S \cap i = \emptyset)$
35		sseq2	$⊢ p = i \to (RSpan (R) (\{X\}) \subseteq p \leftrightarrow RSpan (R) (\{X\}) \subseteq i)$
36	34 35	anbi12d	$⊢ p = i \to ((S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p) \leftrightarrow (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i))$
37	36	elrab	$⊢ i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \leftrightarrow (i \in LIdeal (R) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i))$
38	37	anbi2i	$⊢ ((φ \land \neg X \in S) \land i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\}) \leftrightarrow ((φ \land \neg X \in S) \land (i \in LIdeal (R) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)))$
39	32 38	bitr4i	$⊢ (((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \leftrightarrow ((φ \land \neg X \in S) \land i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\})$
40	39	anbi1i	$⊢ ((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \leftrightarrow (((φ \land \neg X \in S) \land i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\}) \land i \in PrmIdeal (R))$
41		incom	$⊢ i \cap S = S \cap i$
42		simpllr	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)$
43	42	simpld	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to S \cap i = \emptyset$
44	41 43	eqtrid	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to i \cap S = \emptyset$
45	6	ad5antr	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to R \in UFD$
46		simplr	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to i \in PrmIdeal (R)$
47	42	simprd	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to RSpan (R) (\{X\}) \subseteq i$
48	6	ufdidom	$⊢ φ \to R \in IDomn$
49	48	idomringd	$⊢ φ \to R \in Ring$
50		eqid	$⊢ RSpan (R) = RSpan (R)$
51	1 50	rspsnid	$⊢ (R \in Ring \land X \in B) \to X \in RSpan (R) (\{X\})$
52	49 9 51	syl2anc	$⊢ φ \to X \in RSpan (R) (\{X\})$
53	52	ad5antr	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to X \in RSpan (R) (\{X\})$
54	47 53	sseldd	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to X \in i$
55		nelsn	$⊢ X \neq \underset{˙}{0} \to \neg X \in \{\underset{˙}{0}\}$
56	11 55	syl	$⊢ φ \to \neg X \in \{\underset{˙}{0}\}$
57	56	ad5antr	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to \neg X \in \{\underset{˙}{0}\}$
58		nelne1	$⊢ (X \in i \land \neg X \in \{\underset{˙}{0}\}) \to i \neq \{\underset{˙}{0}\}$
59	54 57 58	syl2anc	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to i \neq \{\underset{˙}{0}\}$
60	46 59	eldifsnd	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})$
61		ineq1	$⊢ j = i \to j \cap P = i \cap P$
62	61	neeq1d	$⊢ j = i \to (j \cap P \neq \emptyset \leftrightarrow i \cap P \neq \emptyset)$
63		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
64	63 4 2	isufd	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall j \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\}) j \cap P \neq \emptyset)$
65	64	simprbi	$⊢ R \in UFD \to \forall j \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\}) j \cap P \neq \emptyset$
66	65	adantr	$⊢ (R \in UFD \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to \forall j \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\}) j \cap P \neq \emptyset$
67		simpr	$⊢ (R \in UFD \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})$
68	62 66 67	rspcdva	$⊢ (R \in UFD \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \cap P \neq \emptyset$
69	45 60 68	syl2anc	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to i \cap P \neq \emptyset$
70		sseq0	$⊢ (i \cap P \subseteq i \cap S \land i \cap S = \emptyset) \to i \cap P = \emptyset$
71	70	expcom	$⊢ i \cap S = \emptyset \to (i \cap P \subseteq i \cap S \to i \cap P = \emptyset)$
72	71	necon3ad	$⊢ i \cap S = \emptyset \to (i \cap P \neq \emptyset \to \neg i \cap P \subseteq i \cap S)$
73		sslin	$⊢ P \subseteq S \to i \cap P \subseteq i \cap S$
74	73	con3i	$⊢ \neg i \cap P \subseteq i \cap S \to \neg P \subseteq S$
75	72 74	syl6	$⊢ i \cap S = \emptyset \to (i \cap P \neq \emptyset \to \neg P \subseteq S)$
76	44 69 75	sylc	$⊢ (((((φ \land \neg X \in S) \land i \in LIdeal (R)) \land (S \cap i = \emptyset \land RSpan (R) (\{X\}) \subseteq i)) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to \neg P \subseteq S$
77	40 76	sylanbr	$⊢ ((((φ \land \neg X \in S) \land i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\}) \land i \in PrmIdeal (R)) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j) \to \neg P \subseteq S$
78	77	anasss	$⊢ (((φ \land \neg X \in S) \land i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\}) \land (i \in PrmIdeal (R) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j)) \to \neg P \subseteq S$
79	48	idomcringd	$⊢ φ \to R \in CRing$
80	79	adantr	$⊢ (φ \land \neg X \in S) \to R \in CRing$
81	49	adantr	$⊢ (φ \land \neg X \in S) \to R \in Ring$
82	9	adantr	$⊢ (φ \land \neg X \in S) \to X \in B$
83	82	snssd	$⊢ (φ \land \neg X \in S) \to \{X\} \subseteq B$
84		eqid	$⊢ LIdeal (R) = LIdeal (R)$
85	50 1 84	rspcl	$⊢ (R \in Ring \land \{X\} \subseteq B) \to RSpan (R) (\{X\}) \in LIdeal (R)$
86	81 83 85	syl2anc	$⊢ (φ \land \neg X \in S) \to RSpan (R) (\{X\}) \in LIdeal (R)$
87	5	ringmgp	$⊢ R \in Ring \to M \in Mnd$
88	49 87	syl	$⊢ φ \to M \in Mnd$
89	8	ssrab3	$⊢ S \subseteq B$
90	89	a1i	$⊢ φ \to S \subseteq B$
91		eqeq1	$⊢ x = 1_{R} \to (x = \sum_{M} f \leftrightarrow 1_{R} = \sum_{M} f)$
92	91	rexbidv	$⊢ x = 1_{R} \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P 1_{R} = \sum_{M} f)$
93		eqcom	$⊢ 1_{R} = \sum_{M} f \leftrightarrow \sum_{M} f = 1_{R}$
94	93	rexbii	$⊢ \exists f \in Word P 1_{R} = \sum_{M} f \leftrightarrow \exists f \in Word P \sum_{M} f = 1_{R}$
95	92 94	bitrdi	$⊢ x = 1_{R} \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P \sum_{M} f = 1_{R})$
96		eqid	$⊢ 1_{R} = 1_{R}$
97	1 96	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
98	49 97	syl	$⊢ φ \to 1_{R} \in B$
99		oveq2	$⊢ f = \emptyset \to \sum_{M} f = \sum_{M} \emptyset$
100	99	eqeq1d	$⊢ f = \emptyset \to (\sum_{M} f = 1_{R} \leftrightarrow \sum_{M} \emptyset = 1_{R})$
101		wrd0	$⊢ \emptyset \in Word P$
102	101	a1i	$⊢ φ \to \emptyset \in Word P$
103	5 96	ringidval	$⊢ 1_{R} = 0_{M}$
104	103	gsum0	$⊢ \sum_{M} \emptyset = 1_{R}$
105	104	a1i	$⊢ φ \to \sum_{M} \emptyset = 1_{R}$
106	100 102 105	rspcedvdw	$⊢ φ \to \exists f \in Word P \sum_{M} f = 1_{R}$
107	95 98 106	elrabd	$⊢ φ \to 1_{R} \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
108	107 8	eleqtrrdi	$⊢ φ \to 1_{R} \in S$
109	6	ad2antrr	$⊢ ((φ \land a \in S) \land b \in S) \to R \in UFD$
110	7	ad2antrr	$⊢ ((φ \land a \in S) \land b \in S) \to \neg R \in DivRing$
111		eqid	$⊢ \cdot_{R} = \cdot_{R}$
112		simplr	$⊢ ((φ \land a \in S) \land b \in S) \to a \in S$
113		simpr	$⊢ ((φ \land a \in S) \land b \in S) \to b \in S$
114	1 2 3 4 5 109 110 8 111 112 113	1arithufdlem2	$⊢ ((φ \land a \in S) \land b \in S) \to a \cdot_{R} b \in S$
115	114	anasss	$⊢ (φ \land (a \in S \land b \in S)) \to a \cdot_{R} b \in S$
116	115	ralrimivva	$⊢ φ \to \forall a \in S \forall b \in S a \cdot_{R} b \in S$
117	5 111	mgpplusg	$⊢ \cdot_{R} = +_{M}$
118	23 103 117	issubm	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land 1_{R} \in S \land \forall a \in S \forall b \in S a \cdot_{R} b \in S))$
119	118	biimpar	$⊢ (M \in Mnd \land (S \subseteq B \land 1_{R} \in S \land \forall a \in S \forall b \in S a \cdot_{R} b \in S)) \to S \in SubMnd (M)$
120	88 90 108 116 119	syl13anc	$⊢ φ \to S \in SubMnd (M)$
121	120	adantr	$⊢ (φ \land \neg X \in S) \to S \in SubMnd (M)$
122		neq0	$⊢ \neg S \cap RSpan (R) (\{X\}) = \emptyset \leftrightarrow \exists u u \in (S \cap RSpan (R) (\{X\}))$
123	122	bilani	$⊢ (φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \to \exists u u \in (S \cap RSpan (R) (\{X\}))$
124	6	ad4antr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to R \in UFD$
125	7	ad4antr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to \neg R \in DivRing$
126	9	ad4antr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to X \in B$
127	10	ad4antr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to \neg X \in U$
128	11	ad4antr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to X \neq \underset{˙}{0}$
129		simplr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to y \in B$
130		simpr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to u = y \cdot_{R} X$
131		simpllr	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to u \in (S \cap RSpan (R) (\{X\}))$
132	131	elin1d	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to u \in S$
133	130 132	eqeltrrd	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to y \cdot_{R} X \in S$
134	1 2 3 4 5 124 125 8 126 127 128 111 129 133	1arithufdlem3	$⊢ ((((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \land y \in B) \land u = y \cdot_{R} X) \to X \in S$
135	49	ad2antrr	$⊢ ((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \to R \in Ring$
136	9	ad2antrr	$⊢ ((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \to X \in B$
137		simpr	$⊢ ((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \to u \in (S \cap RSpan (R) (\{X\}))$
138	137	elin2d	$⊢ ((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \to u \in RSpan (R) (\{X\})$
139	1 111 50	elrspsn	$⊢ (R \in Ring \land X \in B) \to (u \in RSpan (R) (\{X\}) \leftrightarrow \exists y \in B u = y \cdot_{R} X)$
140	139	biimpa	$⊢ ((R \in Ring \land X \in B) \land u \in RSpan (R) (\{X\})) \to \exists y \in B u = y \cdot_{R} X$
141	135 136 138 140	syl21anc	$⊢ ((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \to \exists y \in B u = y \cdot_{R} X$
142	134 141	r19.29a	$⊢ ((φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \land u \in (S \cap RSpan (R) (\{X\}))) \to X \in S$
143	123 142	exlimddv	$⊢ (φ \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \to X \in S$
144	143	adantlr	$⊢ ((φ \land \neg X \in S) \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \to X \in S$
145		simplr	$⊢ ((φ \land \neg X \in S) \land \neg S \cap RSpan (R) (\{X\}) = \emptyset) \to \neg X \in S$
146	144 145	condan	$⊢ (φ \land \neg X \in S) \to S \cap RSpan (R) (\{X\}) = \emptyset$
147		eqid	$⊢ \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} = \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\}$
148	1 80 86 121 5 146 147	ssdifidlprm	$⊢ (φ \land \neg X \in S) \to \exists i \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} (i \in PrmIdeal (R) \land \forall j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land RSpan (R) (\{X\}) \subseteq p)\} \neg i \subset j)$
149	78 148	r19.29a	$⊢ (φ \land \neg X \in S) \to \neg P \subseteq S$
150	31 149	condan	$⊢ φ \to X \in S$

Metamath Proof Explorer

Theorem 1arithufdlem4

Proof