1arithufdlem2

Description: Lemma for 1arithufd . The set S of elements which can be written as a product of primes is multiplicatively closed. (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\}$
	1arithufdlem2.1	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	1arithufdlem2.2	$⊢ φ \to X \in S$
	1arithufdlem2.3	$⊢ φ \to Y \in S$
Assertion	1arithufdlem2	$⊢ φ \to X \underset{˙}{\cdot} Y \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		1arithufdlem2.1	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
10		1arithufdlem2.2	$⊢ φ \to X \in S$
11		1arithufdlem2.3	$⊢ φ \to Y \in S$
12		eqeq1	$⊢ x = X \underset{˙}{\cdot} Y \to (x = \sum_{M} f \leftrightarrow X \underset{˙}{\cdot} Y = \sum_{M} f)$
13	12	rexbidv	$⊢ x = X \underset{˙}{\cdot} Y \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P X \underset{˙}{\cdot} Y = \sum_{M} f)$
14	6	ufdidom	$⊢ φ \to R \in IDomn$
15	14	idomringd	$⊢ φ \to R \in Ring$
16	8	ssrab3	$⊢ S \subseteq B$
17	16 10	sselid	$⊢ φ \to X \in B$
18	16 11	sselid	$⊢ φ \to Y \in B$
19	1 9 15 17 18	ringcld	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
20		oveq2	$⊢ f = g ++ h \to \sum_{M} f = \sum_{M} (g ++ h)$
21	20	eqeq2d	$⊢ f = g ++ h \to (X \underset{˙}{\cdot} Y = \sum_{M} f \leftrightarrow X \underset{˙}{\cdot} Y = \sum_{M} (g ++ h))$
22		ccatcl	$⊢ (g \in Word P \land h \in Word P) \to g ++ h \in Word P$
23	22	ad5ant24	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to g ++ h \in Word P$
24		simpllr	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to X = \sum_{M} g$
25		simpr	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to Y = \sum_{M} h$
26	24 25	oveq12d	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to X \underset{˙}{\cdot} Y = (\sum_{M}, g) \underset{˙}{\cdot} (\sum_{M}, h)$
27	5	ringmgp	$⊢ R \in Ring \to M \in Mnd$
28	15 27	syl	$⊢ φ \to M \in Mnd$
29	28	ad4antr	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to M \in Mnd$
30	6	adantr	$⊢ (φ \land x \in P) \to R \in UFD$
31		simpr	$⊢ (φ \land x \in P) \to x \in P$
32	1 4 30 31	rprmcl	$⊢ (φ \land x \in P) \to x \in B$
33	32	ex	$⊢ φ \to (x \in P \to x \in B)$
34	33	ssrdv	$⊢ φ \to P \subseteq B$
35		sswrd	$⊢ P \subseteq B \to Word P \subseteq Word B$
36	34 35	syl	$⊢ φ \to Word P \subseteq Word B$
37	36	ad4antr	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to Word P \subseteq Word B$
38		simp-4r	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to g \in Word P$
39	37 38	sseldd	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to g \in Word B$
40		simplr	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to h \in Word P$
41	37 40	sseldd	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to h \in Word B$
42	5 1	mgpbas	$⊢ B = {Base}_{M}$
43	5 9	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{M}$
44	42 43	gsumccat	$⊢ (M \in Mnd \land g \in Word B \land h \in Word B) \to \sum_{M} (g ++ h) = (\sum_{M}, g) \underset{˙}{\cdot} (\sum_{M}, h)$
45	29 39 41 44	syl3anc	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to \sum_{M} (g ++ h) = (\sum_{M}, g) \underset{˙}{\cdot} (\sum_{M}, h)$
46	26 45	eqtr4d	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to X \underset{˙}{\cdot} Y = \sum_{M} (g ++ h)$
47	21 23 46	rspcedvdw	$⊢ ((((φ \land g \in Word P) \land X = \sum_{M} g) \land h \in Word P) \land Y = \sum_{M} h) \to \exists f \in Word P X \underset{˙}{\cdot} Y = \sum_{M} f$
48	11 8	eleqtrdi	$⊢ φ \to Y \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
49		oveq2	$⊢ f = h \to \sum_{M} f = \sum_{M} h$
50	49	eqeq2d	$⊢ f = h \to (x = \sum_{M} f \leftrightarrow x = \sum_{M} h)$
51	50	cbvrexvw	$⊢ \exists f \in Word P x = \sum_{M} f \leftrightarrow \exists h \in Word P x = \sum_{M} h$
52		eqeq1	$⊢ x = Y \to (x = \sum_{M} h \leftrightarrow Y = \sum_{M} h)$
53	52	rexbidv	$⊢ x = Y \to (\exists h \in Word P x = \sum_{M} h \leftrightarrow \exists h \in Word P Y = \sum_{M} h)$
54	51 53	bitrid	$⊢ x = Y \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists h \in Word P Y = \sum_{M} h)$
55	54	elrab3	$⊢ Y \in B \to (Y \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\} \leftrightarrow \exists h \in Word P Y = \sum_{M} h)$
56	55	biimpa	$⊢ (Y \in B \land Y \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}) \to \exists h \in Word P Y = \sum_{M} h$
57	18 48 56	syl2anc	$⊢ φ \to \exists h \in Word P Y = \sum_{M} h$
58	57	ad2antrr	$⊢ ((φ \land g \in Word P) \land X = \sum_{M} g) \to \exists h \in Word P Y = \sum_{M} h$
59	47 58	r19.29a	$⊢ ((φ \land g \in Word P) \land X = \sum_{M} g) \to \exists f \in Word P X \underset{˙}{\cdot} Y = \sum_{M} f$
60	10 8	eleqtrdi	$⊢ φ \to X \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
61		oveq2	$⊢ f = g \to \sum_{M} f = \sum_{M} g$
62	61	eqeq2d	$⊢ f = g \to (x = \sum_{M} f \leftrightarrow x = \sum_{M} g)$
63	62	cbvrexvw	$⊢ \exists f \in Word P x = \sum_{M} f \leftrightarrow \exists g \in Word P x = \sum_{M} g$
64		eqeq1	$⊢ x = X \to (x = \sum_{M} g \leftrightarrow X = \sum_{M} g)$
65	64	rexbidv	$⊢ x = X \to (\exists g \in Word P x = \sum_{M} g \leftrightarrow \exists g \in Word P X = \sum_{M} g)$
66	63 65	bitrid	$⊢ x = X \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists g \in Word P X = \sum_{M} g)$
67	66	elrab3	$⊢ X \in B \to (X \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\} \leftrightarrow \exists g \in Word P X = \sum_{M} g)$
68	67	biimpa	$⊢ (X \in B \land X \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}) \to \exists g \in Word P X = \sum_{M} g$
69	17 60 68	syl2anc	$⊢ φ \to \exists g \in Word P X = \sum_{M} g$
70	59 69	r19.29a	$⊢ φ \to \exists f \in Word P X \underset{˙}{\cdot} Y = \sum_{M} f$
71	13 19 70	elrabd	$⊢ φ \to X \underset{˙}{\cdot} Y \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
72	71 8	eleqtrrdi	$⊢ φ \to X \underset{˙}{\cdot} Y \in S$

Metamath Proof Explorer

Theorem 1arithufdlem2

Proof