dfufd2lem

	Ref	Expression
Hypotheses	dfufd2.b	$⊢ B = {Base}_{R}$
	dfufd2.0	$⊢ \underset{˙}{0} = 0_{R}$
	dfufd2.u	$⊢ U = Unit (R)$
	dfufd2.p	$⊢ P = RPrime (R)$
	dfufd2.m	$⊢ M = {mulGrp}_{R}$
	dfufd2lem.1	$⊢ φ \to R \in IDomn$
	dfufd2lem.2	$⊢ φ \to I \in PrmIdeal (R)$
	dfufd2lem.3	$⊢ φ \to F \in Word P$
	dfufd2lem.4	$⊢ φ \to \sum_{M} F \in I$
	dfufd2lem.5	$⊢ φ \to \sum_{M} F \neq \underset{˙}{0}$
Assertion	dfufd2lem	$⊢ φ \to I \cap P \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		dfufd2.b	$⊢ B = {Base}_{R}$
2		dfufd2.0	$⊢ \underset{˙}{0} = 0_{R}$
3		dfufd2.u	$⊢ U = Unit (R)$
4		dfufd2.p	$⊢ P = RPrime (R)$
5		dfufd2.m	$⊢ M = {mulGrp}_{R}$
6		dfufd2lem.1	$⊢ φ \to R \in IDomn$
7		dfufd2lem.2	$⊢ φ \to I \in PrmIdeal (R)$
8		dfufd2lem.3	$⊢ φ \to F \in Word P$
9		dfufd2lem.4	$⊢ φ \to \sum_{M} F \in I$
10		dfufd2lem.5	$⊢ φ \to \sum_{M} F \neq \underset{˙}{0}$
11		simpr	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to F (i) \in I$
12		eqidd	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to \|F\| = \|F\|$
13	8	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to F \in Word P$
14	12 13	wrdfd	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to F : (0 ..^\|F\|) ⟶ P$
15		simplr	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to i \in (0 ..^\|F\|)$
16	14 15	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to F (i) \in P$
17		inelcm	$⊢ (F (i) \in I \land F (i) \in P) \to I \cap P \neq \emptyset$
18	11 16 17	syl2anc	$⊢ ((φ \land i \in (0 ..^\|F\|)) \land F (i) \in I) \to I \cap P \neq \emptyset$
19		id	$⊢ φ \to φ$
20		oveq2	$⊢ g = \emptyset \to \sum_{M} g = \sum_{M} \emptyset$
21	20	eleq1d	$⊢ g = \emptyset \to (\sum_{M} g \in I \leftrightarrow \sum_{M} \emptyset \in I)$
22	20	neeq1d	$⊢ g = \emptyset \to (\sum_{M} g \neq \underset{˙}{0} \leftrightarrow \sum_{M} \emptyset \neq \underset{˙}{0})$
23	21 22	3anbi23d	$⊢ g = \emptyset \to ((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \leftrightarrow (φ \land \sum_{M} \emptyset \in I \land \sum_{M} \emptyset \neq \underset{˙}{0}))$
24		fveq2	$⊢ g = \emptyset \to \|g\| = \|\emptyset\|$
25	24	oveq2d	$⊢ g = \emptyset \to (0 ..^\|g\|) = (0 ..^\|\emptyset\|)$
26		fveq1	$⊢ g = \emptyset \to g (i) = \emptyset (i)$
27	26	eleq1d	$⊢ g = \emptyset \to (g (i) \in I \leftrightarrow \emptyset (i) \in I)$
28	25 27	rexeqbidv	$⊢ g = \emptyset \to (\exists i \in (0 ..^\|g\|) g (i) \in I \leftrightarrow \exists i \in (0 ..^\|\emptyset\|) \emptyset (i) \in I)$
29	23 28	imbi12d	$⊢ g = \emptyset \to (((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|g\|) g (i) \in I) \leftrightarrow ((φ \land \sum_{M} \emptyset \in I \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|\emptyset\|) \emptyset (i) \in I))$
30		oveq2	$⊢ g = f \to \sum_{M} g = \sum_{M} f$
31	30	eleq1d	$⊢ g = f \to (\sum_{M} g \in I \leftrightarrow \sum_{M} f \in I)$
32	30	neeq1d	$⊢ g = f \to (\sum_{M} g \neq \underset{˙}{0} \leftrightarrow \sum_{M} f \neq \underset{˙}{0})$
33	31 32	3anbi23d	$⊢ g = f \to ((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \leftrightarrow (φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}))$
34		fveq2	$⊢ g = f \to \|g\| = \|f\|$
35	34	oveq2d	$⊢ g = f \to (0 ..^\|g\|) = (0 ..^\|f\|)$
36		fveq1	$⊢ g = f \to g (i) = f (i)$
37	36	eleq1d	$⊢ g = f \to (g (i) \in I \leftrightarrow f (i) \in I)$
38	35 37	rexeqbidv	$⊢ g = f \to (\exists i \in (0 ..^\|g\|) g (i) \in I \leftrightarrow \exists i \in (0 ..^\|f\|) f (i) \in I)$
39	33 38	imbi12d	$⊢ g = f \to (((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|g\|) g (i) \in I) \leftrightarrow ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I))$
40		oveq2	$⊢ g = f ++ ⟨“ p ”⟩ \to \sum_{M} g = \sum_{M} (f ++ ⟨“ p ”⟩)$
41	40	eleq1d	$⊢ g = f ++ ⟨“ p ”⟩ \to (\sum_{M} g \in I \leftrightarrow \sum_{M} (f ++ ⟨“ p ”⟩) \in I)$
42	40	neeq1d	$⊢ g = f ++ ⟨“ p ”⟩ \to (\sum_{M} g \neq \underset{˙}{0} \leftrightarrow \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0})$
43	41 42	3anbi23d	$⊢ g = f ++ ⟨“ p ”⟩ \to ((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \leftrightarrow (φ \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}))$
44		fveq2	$⊢ g = f ++ ⟨“ p ”⟩ \to \|g\| = \|f ++ ⟨“ p ”⟩\|$
45	44	oveq2d	$⊢ g = f ++ ⟨“ p ”⟩ \to (0 ..^\|g\|) = (0 ..^\|f ++ ⟨“ p ”⟩\|)$
46		fveq1	$⊢ g = f ++ ⟨“ p ”⟩ \to g (i) = (f ++ ⟨“ p ”⟩) (i)$
47	46	eleq1d	$⊢ g = f ++ ⟨“ p ”⟩ \to (g (i) \in I \leftrightarrow (f ++ ⟨“ p ”⟩) (i) \in I)$
48	45 47	rexeqbidv	$⊢ g = f ++ ⟨“ p ”⟩ \to (\exists i \in (0 ..^\|g\|) g (i) \in I \leftrightarrow \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I)$
49	43 48	imbi12d	$⊢ g = f ++ ⟨“ p ”⟩ \to (((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|g\|) g (i) \in I) \leftrightarrow ((φ \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I))$
50		oveq2	$⊢ g = F \to \sum_{M} g = \sum_{M} F$
51	50	eleq1d	$⊢ g = F \to (\sum_{M} g \in I \leftrightarrow \sum_{M} F \in I)$
52	50	neeq1d	$⊢ g = F \to (\sum_{M} g \neq \underset{˙}{0} \leftrightarrow \sum_{M} F \neq \underset{˙}{0})$
53	51 52	3anbi23d	$⊢ g = F \to ((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \leftrightarrow (φ \land \sum_{M} F \in I \land \sum_{M} F \neq \underset{˙}{0}))$
54		fveq2	$⊢ g = F \to \|g\| = \|F\|$
55	54	oveq2d	$⊢ g = F \to (0 ..^\|g\|) = (0 ..^\|F\|)$
56		fveq1	$⊢ g = F \to g (i) = F (i)$
57	56	eleq1d	$⊢ g = F \to (g (i) \in I \leftrightarrow F (i) \in I)$
58	55 57	rexeqbidv	$⊢ g = F \to (\exists i \in (0 ..^\|g\|) g (i) \in I \leftrightarrow \exists i \in (0 ..^\|F\|) F (i) \in I)$
59	53 58	imbi12d	$⊢ g = F \to (((φ \land \sum_{M} g \in I \land \sum_{M} g \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|g\|) g (i) \in I) \leftrightarrow ((φ \land \sum_{M} F \in I \land \sum_{M} F \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|F\|) F (i) \in I))$
60	6	idomringd	$⊢ φ \to R \in Ring$
61		eqid	$⊢ 1_{R} = 1_{R}$
62	3 61	1unit	$⊢ R \in Ring \to 1_{R} \in U$
63	60 62	syl	$⊢ φ \to 1_{R} \in U$
64	63	ad2antrr	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to 1_{R} \in U$
65	5 61	ringidval	$⊢ 1_{R} = 0_{M}$
66	65	gsum0	$⊢ \sum_{M} \emptyset = 1_{R}$
67		simplr	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to \sum_{M} \emptyset \in I$
68	66 67	eqeltrrid	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to 1_{R} \in I$
69	60	ad2antrr	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to R \in Ring$
70	7	ad2antrr	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to I \in PrmIdeal (R)$
71		prmidlidl	$⊢ (R \in Ring \land I \in PrmIdeal (R)) \to I \in LIdeal (R)$
72	69 70 71	syl2anc	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to I \in LIdeal (R)$
73	1 3 64 68 69 72	lidlunitel	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to I = B$
74		eqid	$⊢ \cdot_{R} = \cdot_{R}$
75	1 74	prmidlnr	$⊢ (R \in Ring \land I \in PrmIdeal (R)) \to I \neq B$
76	69 70 75	syl2anc	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to I \neq B$
77	73 76	pm2.21ddne	$⊢ ((φ \land \sum_{M} \emptyset \in I) \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|\emptyset\|) \emptyset (i) \in I$
78	77	3impa	$⊢ (φ \land \sum_{M} \emptyset \in I \land \sum_{M} \emptyset \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|\emptyset\|) \emptyset (i) \in I$
79		simpllr	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to φ$
80		simp-4r	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \sum_{M} f \in I$
81	6	idomdomd	$⊢ φ \to R \in Domn$
82	81	ad3antlr	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to R \in Domn$
83	6	adantr	$⊢ (φ \land p \in P) \to R \in IDomn$
84		simpr	$⊢ (φ \land p \in P) \to p \in P$
85	1 4 83 84	rprmcl	$⊢ (φ \land p \in P) \to p \in B$
86	4 2 83 84	rprmnz	$⊢ (φ \land p \in P) \to p \neq \underset{˙}{0}$
87	85 86	eldifsnd	$⊢ (φ \land p \in P) \to p \in (B ∖ \{\underset{˙}{0}\})$
88	87	ex	$⊢ φ \to (p \in P \to p \in (B ∖ \{\underset{˙}{0}\}))$
89	88	ssrdv	$⊢ φ \to P \subseteq B ∖ \{\underset{˙}{0}\}$
90		sswrd	$⊢ P \subseteq B ∖ \{\underset{˙}{0}\} \to Word P \subseteq Word (B ∖ \{\underset{˙}{0}\})$
91	89 90	syl	$⊢ φ \to Word P \subseteq Word (B ∖ \{\underset{˙}{0}\})$
92	91	ad3antlr	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to Word P \subseteq Word (B ∖ \{\underset{˙}{0}\})$
93		simpll	$⊢ ((f \in Word P \land p \in P) \land φ) \to f \in Word P$
94	93	ad5ant13	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to f \in Word P$
95	92 94	sseldd	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to f \in Word (B ∖ \{\underset{˙}{0}\})$
96	1 5 2 82 95	domnprodn0	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \sum_{M} f \neq \underset{˙}{0}$
97	79 80 96	3jca	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0})$
98		lencl	$⊢ f \in Word P \to \|f\| \in ℕ_{0}$
99		fzossfzop1	$⊢ \|f\| \in ℕ_{0} \to (0 ..^\|f\|) \subseteq (0 ..^\|f\| + 1)$
100	94 98 99	3syl	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (0 ..^\|f\|) \subseteq (0 ..^\|f\| + 1)$
101		ccatws1len	$⊢ f \in Word P \to \|f ++ ⟨“ p ”⟩\| = \|f\| + 1$
102	94 101	syl	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \|f ++ ⟨“ p ”⟩\| = \|f\| + 1$
103	102	oveq2d	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (0 ..^\|f ++ ⟨“ p ”⟩\|) = (0 ..^\|f\| + 1)$
104	100 103	sseqtrrd	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (0 ..^\|f\|) \subseteq (0 ..^\|f ++ ⟨“ p ”⟩\|)$
105	94	ad2antrr	$⊢ (((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land i \in (0 ..^\|f\|)) \land f (i) \in I) \to f \in Word P$
106		simplr	$⊢ (((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land i \in (0 ..^\|f\|)) \land f (i) \in I) \to i \in (0 ..^\|f\|)$
107		ccats1val1	$⊢ (f \in Word P \land i \in (0 ..^\|f\|)) \to (f ++ ⟨“ p ”⟩) (i) = f (i)$
108	105 106 107	syl2anc	$⊢ (((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land i \in (0 ..^\|f\|)) \land f (i) \in I) \to (f ++ ⟨“ p ”⟩) (i) = f (i)$
109		simpr	$⊢ (((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land i \in (0 ..^\|f\|)) \land f (i) \in I) \to f (i) \in I$
110	108 109	eqeltrd	$⊢ (((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land i \in (0 ..^\|f\|)) \land f (i) \in I) \to (f ++ ⟨“ p ”⟩) (i) \in I$
111	110	ex	$⊢ ((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land i \in (0 ..^\|f\|)) \to (f (i) \in I \to (f ++ ⟨“ p ”⟩) (i) \in I)$
112	111	reximdva	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (\exists i \in (0 ..^\|f\|) f (i) \in I \to \exists i \in (0 ..^\|f\|) (f ++ ⟨“ p ”⟩) (i) \in I)$
113		ssrexv	$⊢ (0 ..^\|f\|) \subseteq (0 ..^\|f ++ ⟨“ p ”⟩\|) \to (\exists i \in (0 ..^\|f\|) (f ++ ⟨“ p ”⟩) (i) \in I \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I)$
114	104 112 113	sylsyld	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (\exists i \in (0 ..^\|f\|) f (i) \in I \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I)$
115	97 114	embantd	$⊢ (((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I)$
116	115	imp	$⊢ ((((((f \in Word P \land p \in P) \land \sum_{M} f \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I$
117	116	an62ds	$⊢ ((((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land \sum_{M} f \in I) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I$
118		fveq2	$⊢ i = \|f\| \to (f ++ ⟨“ p ”⟩) (i) = (f ++ ⟨“ p ”⟩) (\|f\|)$
119	118	eleq1d	$⊢ i = \|f\| \to ((f ++ ⟨“ p ”⟩) (i) \in I \leftrightarrow (f ++ ⟨“ p ”⟩) (\|f\|) \in I)$
120	98	ad5antr	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \|f\| \in ℕ_{0}$
121		fzonn0p1	$⊢ \|f\| \in ℕ_{0} \to \|f\| \in (0 ..^\|f\| + 1)$
122	120 121	syl	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \|f\| \in (0 ..^\|f\| + 1)$
123	101	ad5antr	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \|f ++ ⟨“ p ”⟩\| = \|f\| + 1$
124	123	oveq2d	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (0 ..^\|f ++ ⟨“ p ”⟩\|) = (0 ..^\|f\| + 1)$
125	122 124	eleqtrrd	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \|f\| \in (0 ..^\|f ++ ⟨“ p ”⟩\|)$
126		ccatws1ls	$⊢ (f \in Word P \land p \in P) \to (f ++ ⟨“ p ”⟩) (\|f\|) = p$
127	126	ad4antr	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (f ++ ⟨“ p ”⟩) (\|f\|) = p$
128		simp-4r	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to p \in I$
129	127 128	eqeltrd	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (f ++ ⟨“ p ”⟩) (\|f\|) \in I$
130	119 125 129	rspcedvdw	$⊢ (((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I$
131	130	adantr	$⊢ ((((((f \in Word P \land p \in P) \land p \in I) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I$
132	131	an62ds	$⊢ ((((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \land p \in I) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I$
133	6	idomcringd	$⊢ φ \to R \in CRing$
134	133	ad3antlr	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to R \in CRing$
135	7	ad3antlr	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to I \in PrmIdeal (R)$
136	5 1	mgpbas	$⊢ B = {Base}_{M}$
137	5	crngmgp	$⊢ R \in CRing \to M \in CMnd$
138	133 137	syl	$⊢ φ \to M \in CMnd$
139	138	adantl	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to M \in CMnd$
140		ovexd	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to (0 ..^\|f\|) \in V$
141		eqidd	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to \|f\| = \|f\|$
142		simplll	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to f \in Word P$
143	141 142	wrdfd	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to f : (0 ..^\|f\|) ⟶ P$
144	85	ex	$⊢ φ \to (p \in P \to p \in B)$
145	144	ssrdv	$⊢ φ \to P \subseteq B$
146	145	adantl	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to P \subseteq B$
147	143 146	fssd	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to f : (0 ..^\|f\|) ⟶ B$
148		fvexd	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to 1_{R} \in V$
149	148 142	wrdfsupp	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to {finSupp}_{1_{R}} (f)$
150	136 65 139 140 147 149	gsumcl	$⊢ (((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \to \sum_{M} f \in B$
151	150	ad2antrr	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \sum_{M} f \in B$
152	145	adantl	$⊢ ((f \in Word P \land p \in P) \land φ) \to P \subseteq B$
153		simplr	$⊢ ((f \in Word P \land p \in P) \land φ) \to p \in P$
154	152 153	sseldd	$⊢ ((f \in Word P \land p \in P) \land φ) \to p \in B$
155	154	ad5ant13	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to p \in B$
156	138	cmnmndd	$⊢ φ \to M \in Mnd$
157	156	adantl	$⊢ ((f \in Word P \land p \in P) \land φ) \to M \in Mnd$
158		sswrd	$⊢ P \subseteq B \to Word P \subseteq Word B$
159	145 158	syl	$⊢ φ \to Word P \subseteq Word B$
160	159	adantl	$⊢ ((f \in Word P \land p \in P) \land φ) \to Word P \subseteq Word B$
161	160 93	sseldd	$⊢ ((f \in Word P \land p \in P) \land φ) \to f \in Word B$
162	5 74	mgpplusg	$⊢ \cdot_{R} = +_{M}$
163	136 162	gsumccatsn	$⊢ (M \in Mnd \land f \in Word B \land p \in B) \to \sum_{M} (f ++ ⟨“ p ”⟩) = (\sum_{M}, f) \cdot_{R} p$
164	157 161 154 163	syl3anc	$⊢ ((f \in Word P \land p \in P) \land φ) \to \sum_{M} (f ++ ⟨“ p ”⟩) = (\sum_{M}, f) \cdot_{R} p$
165	164	ad5ant13	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \sum_{M} (f ++ ⟨“ p ”⟩) = (\sum_{M}, f) \cdot_{R} p$
166		simplr	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \sum_{M} (f ++ ⟨“ p ”⟩) \in I$
167	165 166	eqeltrrd	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (\sum_{M}, f) \cdot_{R} p \in I$
168	1 74	prmidlc	$⊢ ((R \in CRing \land I \in PrmIdeal (R)) \land (\sum_{M} f \in B \land p \in B \land (\sum_{M}, f) \cdot_{R} p \in I)) \to (\sum_{M} f \in I \lor p \in I)$
169	134 135 151 155 167 168	syl23anc	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to (\sum_{M} f \in I \lor p \in I)$
170	117 132 169	mpjaodan	$⊢ (((((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \land φ) \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I) \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I$
171	170	exp41	$⊢ ((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \to (φ \to (\sum_{M} (f ++ ⟨“ p ”⟩) \in I \to (\sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0} \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I)))$
172	171	3impd	$⊢ ((f \in Word P \land p \in P) \land ((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I)) \to ((φ \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I)$
173	172	ex	$⊢ (f \in Word P \land p \in P) \to (((φ \land \sum_{M} f \in I \land \sum_{M} f \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f\|) f (i) \in I) \to ((φ \land \sum_{M} (f ++ ⟨“ p ”⟩) \in I \land \sum_{M} (f ++ ⟨“ p ”⟩) \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|f ++ ⟨“ p ”⟩\|) (f ++ ⟨“ p ”⟩) (i) \in I))$
174	29 39 49 59 78 173	wrdind	$⊢ F \in Word P \to ((φ \land \sum_{M} F \in I \land \sum_{M} F \neq \underset{˙}{0}) \to \exists i \in (0 ..^\|F\|) F (i) \in I)$
175	174	imp	$⊢ (F \in Word P \land (φ \land \sum_{M} F \in I \land \sum_{M} F \neq \underset{˙}{0})) \to \exists i \in (0 ..^\|F\|) F (i) \in I$
176	8 19 9 10 175	syl13anc	$⊢ φ \to \exists i \in (0 ..^\|F\|) F (i) \in I$
177	18 176	r19.29a	$⊢ φ \to I \cap P \neq \emptyset$

Metamath Proof Explorer

Theorem dfufd2lem

Proof