1arithufdlem3

Description: Lemma for 1arithufd . If a product ( Y .x. X ) can be written as a product of primes, with X non-unit, nonzero, so can X . (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}$
	1arithufdlem3.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	1arithufdlem3.y	$⊢ φ \to Y \in B$
	1arithufdlem3.1	$⊢ φ \to Y \underset{˙}{\cdot} X \in S$
Assertion	1arithufdlem3	$⊢ φ \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		1arithufdlem3.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
13		1arithufdlem3.y	$⊢ φ \to Y \in B$
14		1arithufdlem3.1	$⊢ φ \to Y \underset{˙}{\cdot} X \in S$
15		oveq1	$⊢ y = Y \to y \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X$
16	15	eqeq1d	$⊢ y = Y \to (y \underset{˙}{\cdot} X = \sum_{M} f \leftrightarrow Y \underset{˙}{\cdot} X = \sum_{M} f)$
17	13	ad2antrr	$⊢ ((φ \land f \in Word P) \land Y \underset{˙}{\cdot} X = \sum_{M} f) \to Y \in B$
18		simpr	$⊢ ((φ \land f \in Word P) \land Y \underset{˙}{\cdot} X = \sum_{M} f) \to Y \underset{˙}{\cdot} X = \sum_{M} f$
19	16 17 18	rspcedvdw	$⊢ ((φ \land f \in Word P) \land Y \underset{˙}{\cdot} X = \sum_{M} f) \to \exists y \in B y \underset{˙}{\cdot} X = \sum_{M} f$
20		oveq2	$⊢ z = X \to y \underset{˙}{\cdot} z = y \underset{˙}{\cdot} X$
21	20	eqeq1d	$⊢ z = X \to (y \underset{˙}{\cdot} z = \sum_{M} f \leftrightarrow y \underset{˙}{\cdot} X = \sum_{M} f)$
22	21	rexbidv	$⊢ z = X \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \leftrightarrow \exists y \in B y \underset{˙}{\cdot} X = \sum_{M} f)$
23		eleq1	$⊢ z = X \to (z \in S \leftrightarrow X \in S)$
24	22 23	imbi12d	$⊢ z = X \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} X = \sum_{M} f \to X \in S))$
25		oveq2	$⊢ c = \emptyset \to \sum_{M} c = \sum_{M} \emptyset$
26	25	eqeq2d	$⊢ c = \emptyset \to (y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow y \underset{˙}{\cdot} z = \sum_{M} \emptyset)$
27	26	rexbidv	$⊢ c = \emptyset \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow \exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset)$
28	27	imbi1d	$⊢ c = \emptyset \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset \to z \in S))$
29	28	ralbidv	$⊢ c = \emptyset \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset \to z \in S))$
30	29	imbi2d	$⊢ c = \emptyset \to ((φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S)) \leftrightarrow (φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset \to z \in S)))$
31		oveq2	$⊢ c = d \to \sum_{M} c = \sum_{M} d$
32	31	eqeq2d	$⊢ c = d \to (y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow y \underset{˙}{\cdot} z = \sum_{M} d)$
33	32	rexbidv	$⊢ c = d \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow \exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d)$
34	33	imbi1d	$⊢ c = d \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S))$
35	34	ralbidv	$⊢ c = d \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S))$
36	35	imbi2d	$⊢ c = d \to ((φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S)) \leftrightarrow (φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)))$
37		oveq2	$⊢ c = d ++ ⟨“ p ”⟩ \to \sum_{M} c = \sum_{M} (d ++ ⟨“ p ”⟩)$
38	37	eqeq2d	$⊢ c = d ++ ⟨“ p ”⟩ \to (y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩))$
39	38	rexbidv	$⊢ c = d ++ ⟨“ p ”⟩ \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow \exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩))$
40	39	imbi1d	$⊢ c = d ++ ⟨“ p ”⟩ \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S))$
41	40	ralbidv	$⊢ c = d ++ ⟨“ p ”⟩ \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S))$
42	41	imbi2d	$⊢ c = d ++ ⟨“ p ”⟩ \to ((φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S)) \leftrightarrow (φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S)))$
43		oveq2	$⊢ c = f \to \sum_{M} c = \sum_{M} f$
44	43	eqeq2d	$⊢ c = f \to (y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow y \underset{˙}{\cdot} z = \sum_{M} f)$
45	44	rexbidv	$⊢ c = f \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \leftrightarrow \exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f)$
46	45	imbi1d	$⊢ c = f \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \to z \in S))$
47	46	ralbidv	$⊢ c = f \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S) \leftrightarrow \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \to z \in S))$
48	47	imbi2d	$⊢ c = f \to ((φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} c \to z \in S)) \leftrightarrow (φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \to z \in S)))$
49	6	ufdidom	$⊢ φ \to R \in IDomn$
50	49	idomcringd	$⊢ φ \to R \in CRing$
51	50	ad4antr	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to R \in CRing$
52		simpllr	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to y \in B$
53		simp-4r	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
54	53	eldifad	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to z \in (B ∖ U)$
55	54	eldifad	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to z \in B$
56		simplr	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to y \underset{˙}{\cdot} z = \sum_{M} \emptyset$
57		eqid	$⊢ 1_{R} = 1_{R}$
58	5 57	ringidval	$⊢ 1_{R} = 0_{M}$
59	58	gsum0	$⊢ \sum_{M} \emptyset = 1_{R}$
60	56 59	eqtrdi	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to y \underset{˙}{\cdot} z = 1_{R}$
61	51	crngringd	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to R \in Ring$
62	3 57	1unit	$⊢ R \in Ring \to 1_{R} \in U$
63	61 62	syl	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to 1_{R} \in U$
64	60 63	eqeltrd	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to y \underset{˙}{\cdot} z \in U$
65	3 12 1	unitmulclb	$⊢ (R \in CRing \land y \in B \land z \in B) \to (y \underset{˙}{\cdot} z \in U \leftrightarrow (y \in U \land z \in U))$
66	65	simplbda	$⊢ ((R \in CRing \land y \in B \land z \in B) \land y \underset{˙}{\cdot} z \in U) \to z \in U$
67	51 52 55 64 66	syl31anc	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to z \in U$
68	54	eldifbd	$⊢ ((((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \land \neg z \in S) \to \neg z \in U$
69	67 68	condan	$⊢ (((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land y \in B) \land y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \to z \in S$
70	69	r19.29an	$⊢ ((φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land \exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset) \to z \in S$
71	70	ex	$⊢ (φ \land z \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset \to z \in S)$
72	71	ralrimiva	$⊢ φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} \emptyset \to z \in S)$
73		oveq1	$⊢ y = w \to y \underset{˙}{\cdot} t = w \underset{˙}{\cdot} t$
74	73	eqeq1d	$⊢ y = w \to (y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩) \leftrightarrow w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩))$
75	74	cbvrexvw	$⊢ \exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩) \leftrightarrow \exists w \in B w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)$
76		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
77	1 76 12	dvdsr	$⊢ p ∥_{r} (R) w \leftrightarrow (p \in B \land \exists k \in B k \underset{˙}{\cdot} p = w)$
78		oveq1	$⊢ v = k \to v \underset{˙}{\cdot} t = k \underset{˙}{\cdot} t$
79	78	eqeq1d	$⊢ v = k \to (v \underset{˙}{\cdot} t = \sum_{M} d \leftrightarrow k \underset{˙}{\cdot} t = \sum_{M} d)$
80		simplr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to k \in B$
81		eqid	$⊢ 0_{R} = 0_{R}$
82	6	adantr	$⊢ (φ \land p \in P) \to R \in UFD$
83		simpr	$⊢ (φ \land p \in P) \to p \in P$
84	1 4 82 83	rprmcl	$⊢ (φ \land p \in P) \to p \in B$
85	84	ex	$⊢ φ \to (p \in P \to p \in B)$
86	85	ssrdv	$⊢ φ \to P \subseteq B$
87	86	ad6antr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to P \subseteq B$
88		simp-5r	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to p \in P$
89	87 88	sseldd	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to p \in B$
90	89	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to p \in B$
91	6	ad6antr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to R \in UFD$
92	91	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to R \in UFD$
93	88	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to p \in P$
94	4 81 92 93	rprmnz	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to p \neq 0_{R}$
95	90 94	eldifsnd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to p \in (B ∖ \{0_{R}\})$
96	5 1	mgpbas	$⊢ B = {Base}_{M}$
97	5	crngmgp	$⊢ R \in CRing \to M \in CMnd$
98	50 97	syl	$⊢ φ \to M \in CMnd$
99	98	ad6antr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to M \in CMnd$
100		ovexd	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to (0 ..^\|d\|) \in V$
101		eqidd	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to \|d\| = \|d\|$
102		sswrd	$⊢ P \subseteq B \to Word P \subseteq Word B$
103	86 102	syl	$⊢ φ \to Word P \subseteq Word B$
104	103	sselda	$⊢ (φ \land d \in Word P) \to d \in Word B$
105	104	ad5antr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to d \in Word B$
106	101 105	wrdfd	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to d : (0 ..^\|d\|) ⟶ B$
107	50	crngringd	$⊢ φ \to R \in Ring$
108	107 62	syl	$⊢ φ \to 1_{R} \in U$
109	108	ad6antr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to 1_{R} \in U$
110		simp-6r	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to d \in Word P$
111	109 110	wrdfsupp	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to {finSupp}_{1_{R}} (d)$
112	96 58 99 100 106 111	gsumcl	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to \sum_{M} d \in B$
113	112	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to \sum_{M} d \in B$
114	107	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to R \in Ring$
115		simpllr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
116	115	eldifad	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to t \in (B ∖ U)$
117	116	eldifad	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to t \in B$
118	117	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to t \in B$
119	1 12 114 80 118	ringcld	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to k \underset{˙}{\cdot} t \in B$
120	49	idomdomd	$⊢ φ \to R \in Domn$
121	120	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to R \in Domn$
122	50	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to R \in CRing$
123	1 12 122 90 113	crngcomd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to p \underset{˙}{\cdot} (\sum_{M}, d) = (\sum_{M}, d) \underset{˙}{\cdot} p$
124		simpr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)$
125	5	ringmgp	$⊢ R \in Ring \to M \in Mnd$
126	107 125	syl	$⊢ φ \to M \in Mnd$
127	126	ad6antr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to M \in Mnd$
128	5 12	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{M}$
129	96 128	gsumccatsn	$⊢ (M \in Mnd \land d \in Word B \land p \in B) \to \sum_{M} (d ++ ⟨“ p ”⟩) = (\sum_{M}, d) \underset{˙}{\cdot} p$
130	127 105 89 129	syl3anc	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to \sum_{M} (d ++ ⟨“ p ”⟩) = (\sum_{M}, d) \underset{˙}{\cdot} p$
131	124 130	eqtrd	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to w \underset{˙}{\cdot} t = (\sum_{M}, d) \underset{˙}{\cdot} p$
132	131	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to w \underset{˙}{\cdot} t = (\sum_{M}, d) \underset{˙}{\cdot} p$
133	1 12 114 80 90 118	ringassd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to (k \underset{˙}{\cdot} p) \underset{˙}{\cdot} t = k \underset{˙}{\cdot} (p \underset{˙}{\cdot} t)$
134		simpr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to k \underset{˙}{\cdot} p = w$
135	134	oveq1d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to (k \underset{˙}{\cdot} p) \underset{˙}{\cdot} t = w \underset{˙}{\cdot} t$
136	1 12 122 80 90 118	crng12d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to k \underset{˙}{\cdot} (p \underset{˙}{\cdot} t) = p \underset{˙}{\cdot} (k \underset{˙}{\cdot} t)$
137	133 135 136	3eqtr3d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to w \underset{˙}{\cdot} t = p \underset{˙}{\cdot} (k \underset{˙}{\cdot} t)$
138	123 132 137	3eqtr2d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to p \underset{˙}{\cdot} (\sum_{M}, d) = p \underset{˙}{\cdot} (k \underset{˙}{\cdot} t)$
139	1 81 12 95 113 119 121 138	domnlcan	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to \sum_{M} d = k \underset{˙}{\cdot} t$
140	139	eqcomd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to k \underset{˙}{\cdot} t = \sum_{M} d$
141	79 80 140	rspcedvdw	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to \exists v \in B v \underset{˙}{\cdot} t = \sum_{M} d$
142		oveq1	$⊢ y = v \to y \underset{˙}{\cdot} t = v \underset{˙}{\cdot} t$
143	142	eqeq1d	$⊢ y = v \to (y \underset{˙}{\cdot} t = \sum_{M} d \leftrightarrow v \underset{˙}{\cdot} t = \sum_{M} d)$
144	143	cbvrexvw	$⊢ \exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d \leftrightarrow \exists v \in B v \underset{˙}{\cdot} t = \sum_{M} d$
145	141 144	sylibr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to \exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d$
146		simp-4r	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = w) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \to t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
147		oveq2	$⊢ z = t \to y \underset{˙}{\cdot} z = y \underset{˙}{\cdot} t$
148	147	eqeq1d	$⊢ z = t \to (y \underset{˙}{\cdot} z = \sum_{M} d \leftrightarrow y \underset{˙}{\cdot} t = \sum_{M} d)$
149	148	rexbidv	$⊢ z = t \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \leftrightarrow \exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d)$
150		eleq1w	$⊢ z = t \to (z \in S \leftrightarrow t \in S)$
151	149 150	imbi12d	$⊢ z = t \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d \to t \in S))$
152	151	adantl	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = w) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land z = t) \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d \to t \in S))$
153	146 152	rspcdv	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = w) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \to (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d \to t \in S))$
154	153	imp	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = w) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \to (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d \to t \in S)$
155	154	an72ds	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} d \to t \in S)$
156	145 155	mpd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = w) \to t \in S$
157	156	r19.29an	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land \exists k \in B k \underset{˙}{\cdot} p = w) \to t \in S$
158	157	adantrl	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land (p \in B \land \exists k \in B k \underset{˙}{\cdot} p = w)) \to t \in S$
159	77 158	sylan2b	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land p ∥_{r} (R) w) \to t \in S$
160	1 76 12	dvdsr	$⊢ p ∥_{r} (R) t \leftrightarrow (p \in B \land \exists k \in B k \underset{˙}{\cdot} p = t)$
161		eqeq1	$⊢ x = t \to (x = \sum_{M} f \leftrightarrow t = \sum_{M} f)$
162	161	rexbidv	$⊢ x = t \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P t = \sum_{M} f)$
163	117	ad3antrrr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to t \in B$
164		oveq2	$⊢ f = ⟨“ t ”⟩ \to \sum_{M} f = \sum_{M} ⟨“ t ”⟩$
165	164	eqeq2d	$⊢ f = ⟨“ t ”⟩ \to (t = \sum_{M} f \leftrightarrow t = \sum_{M} ⟨“ t ”⟩)$
166		simplr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to k \underset{˙}{\cdot} p = t$
167	49	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to R \in IDomn$
168	167	adantr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to R \in IDomn$
169		simpr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to k \in U$
170	88	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to p \in P$
171	170	adantr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to p \in P$
172	4 3 12 168 169 171	unitmulrprm	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to k \underset{˙}{\cdot} p \in P$
173	166 172	eqeltrrd	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to t \in P$
174	173	s1cld	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to ⟨“ t ”⟩ \in Word P$
175	96	gsumws1	$⊢ t \in B \to \sum_{M} ⟨“ t ”⟩ = t$
176	163 175	syl	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to \sum_{M} ⟨“ t ”⟩ = t$
177	176	eqcomd	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to t = \sum_{M} ⟨“ t ”⟩$
178	165 174 177	rspcedvdw	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to \exists f \in Word P t = \sum_{M} f$
179	162 163 178	elrabd	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to t \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
180	179 8	eleqtrrdi	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land k \in U) \to t \in S$
181		simplr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to k \underset{˙}{\cdot} p = t$
182	91	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to R \in UFD$
183	182	adantr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to R \in UFD$
184	7	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to \neg R \in DivRing$
185	184	adantr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to \neg R \in DivRing$
186		oveq1	$⊢ v = w \to v \underset{˙}{\cdot} k = w \underset{˙}{\cdot} k$
187	186	eqeq1d	$⊢ v = w \to (v \underset{˙}{\cdot} k = \sum_{M} d \leftrightarrow w \underset{˙}{\cdot} k = \sum_{M} d)$
188		simp-4r	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to w \in B$
189	107	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to R \in Ring$
190		simplr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to k \in B$
191	1 12 189 188 190	ringcld	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to w \underset{˙}{\cdot} k \in B$
192	112	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to \sum_{M} d \in B$
193	89	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to p \in B$
194	4 2 182 170	rprmnz	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to p \neq \underset{˙}{0}$
195	193 194	eldifsnd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to p \in (B ∖ \{\underset{˙}{0}\})$
196	1 12 189 188 190 193	ringassd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to (w \underset{˙}{\cdot} k) \underset{˙}{\cdot} p = w \underset{˙}{\cdot} (k \underset{˙}{\cdot} p)$
197		simpr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to k \underset{˙}{\cdot} p = t$
198	197	oveq2d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to w \underset{˙}{\cdot} (k \underset{˙}{\cdot} p) = w \underset{˙}{\cdot} t$
199	131	ad2antrr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to w \underset{˙}{\cdot} t = (\sum_{M}, d) \underset{˙}{\cdot} p$
200	196 198 199	3eqtrd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to (w \underset{˙}{\cdot} k) \underset{˙}{\cdot} p = (\sum_{M}, d) \underset{˙}{\cdot} p$
201	1 2 12 191 192 195 167 200	idomrcan	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to w \underset{˙}{\cdot} k = \sum_{M} d$
202	187 188 201	rspcedvdw	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to \exists v \in B v \underset{˙}{\cdot} k = \sum_{M} d$
203		oveq1	$⊢ y = v \to y \underset{˙}{\cdot} k = v \underset{˙}{\cdot} k$
204	203	eqeq1d	$⊢ y = v \to (y \underset{˙}{\cdot} k = \sum_{M} d \leftrightarrow v \underset{˙}{\cdot} k = \sum_{M} d)$
205	204	cbvrexvw	$⊢ \exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d \leftrightarrow \exists v \in B v \underset{˙}{\cdot} k = \sum_{M} d$
206	202 205	sylibr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to \exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d$
207	206	adantr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to \exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d$
208		simplr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land \neg k \in U) \to k \in B$
209		simpr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land \neg k \in U) \to \neg k \in U$
210	208 209	eldifd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land \neg k \in U) \to k \in (B ∖ U)$
211		simpr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to k = \underset{˙}{0}$
212	211	oveq1d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to k \underset{˙}{\cdot} p = \underset{˙}{0} \underset{˙}{\cdot} p$
213		simp-6r	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to k \underset{˙}{\cdot} p = t$
214	107	ad8antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to R \in Ring$
215	84	adantlr	$⊢ ((φ \land d \in Word P) \land p \in P) \to p \in B$
216	215	ad6antr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to p \in B$
217	1 12 2 214 216	ringlzd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{\cdot} p = \underset{˙}{0}$
218	212 213 217	3eqtr3d	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to t = \underset{˙}{0}$
219		simp-5r	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
220		eldifsni	$⊢ t \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \to t \neq \underset{˙}{0}$
221	219 220	syl	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to t \neq \underset{˙}{0}$
222	221	neneqd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k = \underset{˙}{0}) \to \neg t = \underset{˙}{0}$
223	218 222	pm2.65da	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \to \neg k = \underset{˙}{0}$
224	223	neqned	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \to k \neq \underset{˙}{0}$
225	224	adantr	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land \neg k \in U) \to k \neq \underset{˙}{0}$
226	210 225	eldifsnd	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land k \underset{˙}{\cdot} p = t) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land \neg k \in U) \to k \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
227	226	an72ds	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \neg k \in U) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to k \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
228		oveq2	$⊢ z = k \to y \underset{˙}{\cdot} z = y \underset{˙}{\cdot} k$
229	228	eqeq1d	$⊢ z = k \to (y \underset{˙}{\cdot} z = \sum_{M} d \leftrightarrow y \underset{˙}{\cdot} k = \sum_{M} d)$
230	229	rexbidv	$⊢ z = k \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \leftrightarrow \exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d)$
231		eleq1w	$⊢ z = k \to (z \in S \leftrightarrow k \in S)$
232	230 231	imbi12d	$⊢ z = k \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d \to k \in S))$
233	232	adantl	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \neg k \in U) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land z = k) \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d \to k \in S))$
234	227 233	rspcdv	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \neg k \in U) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \to (\exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d \to k \in S))$
235	234	imp	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \neg k \in U) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \to (\exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d \to k \in S)$
236	235	an82ds	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to (\exists y \in B y \underset{˙}{\cdot} k = \sum_{M} d \to k \in S)$
237	207 236	mpd	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to k \in S$
238		eqeq1	$⊢ x = p \to (x = \sum_{M} f \leftrightarrow p = \sum_{M} f)$
239	238	rexbidv	$⊢ x = p \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P p = \sum_{M} f)$
240		oveq2	$⊢ f = ⟨“ p ”⟩ \to \sum_{M} f = \sum_{M} ⟨“ p ”⟩$
241	240	eqeq2d	$⊢ f = ⟨“ p ”⟩ \to (p = \sum_{M} f \leftrightarrow p = \sum_{M} ⟨“ p ”⟩)$
242		simpr	$⊢ ((φ \land d \in Word P) \land p \in P) \to p \in P$
243	242	s1cld	$⊢ ((φ \land d \in Word P) \land p \in P) \to ⟨“ p ”⟩ \in Word P$
244	96	gsumws1	$⊢ p \in B \to \sum_{M} ⟨“ p ”⟩ = p$
245	215 244	syl	$⊢ ((φ \land d \in Word P) \land p \in P) \to \sum_{M} ⟨“ p ”⟩ = p$
246	245	eqcomd	$⊢ ((φ \land d \in Word P) \land p \in P) \to p = \sum_{M} ⟨“ p ”⟩$
247	241 243 246	rspcedvdw	$⊢ ((φ \land d \in Word P) \land p \in P) \to \exists f \in Word P p = \sum_{M} f$
248	239 215 247	elrabd	$⊢ ((φ \land d \in Word P) \land p \in P) \to p \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
249	248 8	eleqtrrdi	$⊢ ((φ \land d \in Word P) \land p \in P) \to p \in S$
250	249	ad7antr	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to p \in S$
251	1 2 3 4 5 183 185 8 12 237 250	1arithufdlem2	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to k \underset{˙}{\cdot} p \in S$
252	181 251	eqeltrrd	$⊢ (((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \land \neg k \in U) \to t \in S$
253	180 252	pm2.61dan	$⊢ ((((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land k \in B) \land k \underset{˙}{\cdot} p = t) \to t \in S$
254	253	r19.29an	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land \exists k \in B k \underset{˙}{\cdot} p = t) \to t \in S$
255	254	adantrl	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land (p \in B \land \exists k \in B k \underset{˙}{\cdot} p = t)) \to t \in S$
256	160 255	sylan2b	$⊢ (((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \land p ∥_{r} (R) t) \to t \in S$
257		simplr	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to w \in B$
258	1 76 12	dvdsrmul	$⊢ (p \in B \land \sum_{M} d \in B) \to p ∥_{r} (R) ((\sum_{M}, d) \underset{˙}{\cdot} p)$
259	89 112 258	syl2anc	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to p ∥_{r} (R) ((\sum_{M}, d) \underset{˙}{\cdot} p)$
260	259 131	breqtrrd	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to p ∥_{r} (R) (w \underset{˙}{\cdot} t)$
261	1 4 76 12 91 88 257 117 260	rprmdvds	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to (p ∥_{r} (R) w \lor p ∥_{r} (R) t)$
262	159 256 261	mpjaodan	$⊢ ((((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land w \in B) \land w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to t \in S$
263	262	r19.29an	$⊢ (((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land \exists w \in B w \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to t \in S$
264	75 263	sylan2b	$⊢ (((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \land \exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩)) \to t \in S$
265	264	ex	$⊢ ((((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \land t \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩) \to t \in S)$
266	265	ralrimiva	$⊢ (((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \to \forall t \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩) \to t \in S)$
267	147	eqeq1d	$⊢ z = t \to (y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \leftrightarrow y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩))$
268	267	rexbidv	$⊢ z = t \to (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \leftrightarrow \exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩))$
269	268 150	imbi12d	$⊢ z = t \to ((\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S) \leftrightarrow (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩) \to t \in S))$
270	269	cbvralvw	$⊢ \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S) \leftrightarrow \forall t \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} t = \sum_{M} (d ++ ⟨“ p ”⟩) \to t \in S)$
271	266 270	sylibr	$⊢ (((φ \land d \in Word P) \land p \in P) \land \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S)$
272	271	ex	$⊢ ((φ \land d \in Word P) \land p \in P) \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S))$
273	272	anasss	$⊢ (φ \land (d \in Word P \land p \in P)) \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S))$
274	273	expcom	$⊢ (d \in Word P \land p \in P) \to (φ \to (\forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S) \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S)))$
275	274	a2d	$⊢ (d \in Word P \land p \in P) \to ((φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} d \to z \in S)) \to (φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} (d ++ ⟨“ p ”⟩) \to z \in S)))$
276	30 36 42 48 72 275	wrdind	$⊢ f \in Word P \to (φ \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \to z \in S))$
277	276	impcom	$⊢ (φ \land f \in Word P) \to \forall z \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) (\exists y \in B y \underset{˙}{\cdot} z = \sum_{M} f \to z \in S)$
278	9 10	eldifd	$⊢ φ \to X \in (B ∖ U)$
279	278 11	eldifsnd	$⊢ φ \to X \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
280	279	adantr	$⊢ (φ \land f \in Word P) \to X \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
281	24 277 280	rspcdva	$⊢ (φ \land f \in Word P) \to (\exists y \in B y \underset{˙}{\cdot} X = \sum_{M} f \to X \in S)$
282	281	imp	$⊢ ((φ \land f \in Word P) \land \exists y \in B y \underset{˙}{\cdot} X = \sum_{M} f) \to X \in S$
283	19 282	syldan	$⊢ ((φ \land f \in Word P) \land Y \underset{˙}{\cdot} X = \sum_{M} f) \to X \in S$
284	14 8	eleqtrdi	$⊢ φ \to Y \underset{˙}{\cdot} X \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
285		eqeq1	$⊢ x = Y \underset{˙}{\cdot} X \to (x = \sum_{M} f \leftrightarrow Y \underset{˙}{\cdot} X = \sum_{M} f)$
286	285	rexbidv	$⊢ x = Y \underset{˙}{\cdot} X \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P Y \underset{˙}{\cdot} X = \sum_{M} f)$
287	286	elrab	$⊢ Y \underset{˙}{\cdot} X \in \{x \in B \| \exists f \in Word P x = \sum_{M} f\} \leftrightarrow (Y \underset{˙}{\cdot} X \in B \land \exists f \in Word P Y \underset{˙}{\cdot} X = \sum_{M} f)$
288	284 287	sylib	$⊢ φ \to (Y \underset{˙}{\cdot} X \in B \land \exists f \in Word P Y \underset{˙}{\cdot} X = \sum_{M} f)$
289	288	simprd	$⊢ φ \to \exists f \in Word P Y \underset{˙}{\cdot} X = \sum_{M} f$
290	283 289	r19.29a	$⊢ φ \to X \in S$

Metamath Proof Explorer

Theorem 1arithufdlem3

Proof