1arithufdlem1

Description: Lemma for 1arithufd . The set S of elements which can be written as a product of primes is not empty. (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\}$
Assertion	1arithufdlem1	$⊢ φ \to S \neq \emptyset$

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		eqeq1	$⊢ x = p \to (x = \sum_{M} f \leftrightarrow p = \sum_{M} f)$
10	9	rexbidv	$⊢ x = p \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P p = \sum_{M} f)$
11	6	ad2antrr	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to R \in UFD$
12	11	ad2antrr	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to R \in UFD$
13		simplr	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to p \in P$
14	1 4 12 13	rprmcl	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to p \in B$
15		oveq2	$⊢ f = ⟨“ p ”⟩ \to \sum_{M} f = \sum_{M} ⟨“ p ”⟩$
16	15	eqeq2d	$⊢ f = ⟨“ p ”⟩ \to (p = \sum_{M} f \leftrightarrow p = \sum_{M} ⟨“ p ”⟩)$
17	13	s1cld	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to ⟨“ p ”⟩ \in Word P$
18	5 1	mgpbas	$⊢ B = {Base}_{M}$
19	18	gsumws1	$⊢ p \in B \to \sum_{M} ⟨“ p ”⟩ = p$
20	14 19	syl	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to \sum_{M} ⟨“ p ”⟩ = p$
21	20	eqcomd	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to p = \sum_{M} ⟨“ p ”⟩$
22	16 17 21	rspcedvdw	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to \exists f \in Word P p = \sum_{M} f$
23	10 14 22	elrabd	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to p \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
24	23 8	eleqtrrdi	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to p \in S$
25	24	ne0d	$⊢ ((((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \land p \in P) \land p \in m) \to S \neq \emptyset$
26		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
27	6	ufdidom	$⊢ φ \to R \in IDomn$
28	27	idomcringd	$⊢ φ \to R \in CRing$
29	28	ad2antrr	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to R \in CRing$
30		simplr	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to m \in MaxIdeal (R)$
31		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
32	31	mxidlprm	$⊢ (R \in CRing \land m \in MaxIdeal (R)) \to m \in PrmIdeal (R)$
33	29 30 32	syl2anc	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to m \in PrmIdeal (R)$
34		simpr	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to m \neq \{\underset{˙}{0}\}$
35	26 4 2 11 33 34	ufdprmidl	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to \exists p \in P p \in m$
36	25 35	r19.29a	$⊢ ((φ \land m \in MaxIdeal (R)) \land m \neq \{\underset{˙}{0}\}) \to S \neq \emptyset$
37	27	idomdomd	$⊢ φ \to R \in Domn$
38		domnnzr	$⊢ R \in Domn \to R \in NzRing$
39	37 38	syl	$⊢ φ \to R \in NzRing$
40	2 39 7	krullndrng	$⊢ φ \to \exists m \in MaxIdeal (R) m \neq \{\underset{˙}{0}\}$
41	36 40	r19.29a	$⊢ φ \to S \neq \emptyset$

Metamath Proof Explorer

Theorem 1arithufdlem1

Proof