Theorem elrgspnlem4 33873

Description: Lemma for elrgspn 33874. (Contributed by Thierry Arnoux, 5-Oct-2025.)

Hypotheses

Ref	Expression
elrgspn.b	⊢ 𝐵 = (Base‘𝑅)
elrgspn.m	⊢ 𝑀 = (mulGrp‘𝑅)
elrgspn.x	⊢ · = (.g‘𝑅)
elrgspn.n	⊢ 𝑁 = (RingSpan‘𝑅)
elrgspn.f	⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
elrgspn.r	⊢ (𝜑 → 𝑅 ∈ Ring)
elrgspn.a	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
elrgspnlem1.1	⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))

Assertion

Ref	Expression
elrgspnlem4	⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)

Distinct variable groups:   · ,𝑓,𝑔,𝑤   𝐴,𝑓,𝑔,𝑤   𝐵,𝑓,𝑔,𝑤   𝑓,𝐹,𝑔,𝑤   𝑓,𝑀,𝑔,𝑤   𝑅,𝑓,𝑔,𝑤   𝑆,𝑔,𝑤   𝜑,𝑓,𝑔,𝑤

Allowed substitution hints:   𝑆(𝑓)   𝑁(𝑤, 𝑓, 𝑔)

Proof of Theorem elrgspnlem4

Dummy variables 𝑒 ℎ 𝑖 𝑠 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrgspn.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
2		elrgspn.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
3	2	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 = (Base‘𝑅))
4		elrgspn.a	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
5		elrgspn.n	. . . 4 ⊢ 𝑁 = (RingSpan‘𝑅)
6	5	a1i 11	. . 3 ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))
7		eqidd 2764	. . 3 ⊢ (𝜑 → (𝑁‘𝐴) = (𝑁‘𝐴))
8	1, 3, 4, 6, 7	rgspnval 20891	. 2 ⊢ (𝜑 → (𝑁‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
9		sseq2 3939	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝑆))
10		elrgspn.m	. . . . . 6 ⊢ 𝑀 = (mulGrp‘𝑅)
11		elrgspn.x	. . . . . 6 ⊢ · = (.g‘𝑅)
12		elrgspn.f	. . . . . 6 ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
13		elrgspnlem1.1	. . . . . 6 ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
14	2, 10, 11, 5, 12, 1, 4, 13	elrgspnlem2 33871	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
15	2, 10, 11, 5, 12, 1, 4, 13	elrgspnlem3 33872	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
16	9, 14, 15	elrabd 3650	. . . 4 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
17		intss1 4926	. . . 4 ⊢ (𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
18	16, 17	syl 18	. . 3 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
19		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
20		eqidd 2764	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) = (𝑔 supp 0))
21		oveq1 7447	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 supp 0) = (𝑔 supp 0))
22	21	eqeq1d 2765	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 supp 0) = (𝑔 supp 0) ↔ (𝑔 supp 0) = (𝑔 supp 0)))
23		fveq1 6904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤))
24	23	oveq1d 7455	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
25	24	mpteq2dv 5202	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
26	25	oveq2d 7456	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
27	26	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
28	22, 27	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
29		eqeq2 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ∅ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ∅))
30	29	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
31	30	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ∅ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
32		eqeq2 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ℎ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ℎ))
33	32	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ℎ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
34	33	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ℎ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
35		eqeq2 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
36	35	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
37	36	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
38		eqeq2 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑔 supp 0) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (𝑔 supp 0)))
39	38	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑔 supp 0) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
40	39	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑔 supp 0) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
41		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝑅) = (0g‘𝑅)
42	1	ringcmnd 20540	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ CMnd)
43	42	ad5antr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → 𝑅 ∈ CMnd)
44	2	fvexi 6919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 ∈ V
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
46	45, 4	ssexd 5290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ V)
47		wrdexg 14693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
48	46, 47	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Word 𝐴 ∈ V)
49	48	ad5antr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → Word 𝐴 ∈ V)
50		simp-4l 795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝜑)
51	12	reqabi 3438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ 𝐹 ↔ (𝑓 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑓 finSupp 0))
52	51	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ 𝐹 → 𝑓 ∈ (ℤ ↑m Word 𝐴))
53	52	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (ℤ ↑m Word 𝐴))
54		zex 12726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℤ ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℤ ∈ V)
56	55, 48	elmapd 8885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑓 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑓:Word 𝐴⟶ℤ))
57	56	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ ↑m Word 𝐴)) → 𝑓:Word 𝐴⟶ℤ)
58	50, 53, 57	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓:Word 𝐴⟶ℤ)
59	58	ffnd 6729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 Fn Word 𝐴)
60	59	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑓 Fn Word 𝐴)
61	49	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ∈ V)
62		0zd 12729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 0 ∈ ℤ)
63		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ ∅))
64	63	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐴)
65	63	eldifbd 4055	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ ∅)
66		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓 supp 0) = ∅)
67	65, 66	neleqtrrd 2887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ (𝑓 supp 0))
68	64, 67	eldifd 4053	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ (𝑓 supp 0)))
69	60, 61, 62, 68	fvdifsupp 8213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓‘𝑤) = 0)
70	69	oveq1d 7455	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
71	10	ringmgp 20492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
72	1, 71	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ Mnd)
73	72	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑀 ∈ Mnd)
74		sswrd 14691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
75	4, 74	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
76	75	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ⊆ Word 𝐵)
77	76, 64	sseldd 3914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐵)
78	10, 2	mgpbas 20392	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 = (Base‘𝑀)
79	78	gsumwcl 19061	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
80	73, 77, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑀 Σg 𝑤) ∈ 𝐵)
81	2, 41, 11	mulg0 19310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
82	80, 81	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
83	70, 82	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
84		0fi 9095	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ Fin
85	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ∈ Fin)
86	1	ringgrpd 20496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 ∈ Grp)
87	86	ad6antr 749	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
88	58	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑓:Word 𝐴⟶ℤ)
89		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
90	88, 89	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑓‘𝑤) ∈ ℤ)
91	72	ad6antr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
92	75	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
93	92, 89	sseldd 3914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
94	91, 93, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
95	2, 11, 87, 90, 94	mulgcld 19332	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
96		0ss 4353	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ⊆ Word 𝐴
97	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ⊆ Word 𝐴)
98	2, 41, 43, 49, 83, 85, 95, 97	gsummptres2 33681	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
99		mpt0 6700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅
100	99	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅)
101	100	oveq2d 7456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg ∅))
102	41	gsum0 18899	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg ∅) = (0g‘𝑅))
104	98, 101, 103	3eqtrd 2802	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
105		subrgsubg 20856	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubGrp‘𝑅))
106	41	subg0cl 19370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubGrp‘𝑅) → (0g‘𝑅) ∈ 𝑡)
107	105, 106	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (SubRing‘𝑅) → (0g‘𝑅) ∈ 𝑡)
108	107	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (0g‘𝑅) ∈ 𝑡)
109	108	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (0g‘𝑅) ∈ 𝑡)
110	104, 109	eqeltrd 2864	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
111	110	ex 418	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
112	111	ralrimiva 3158	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
113	42	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ CMnd)
114	48	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
115		simp-5l 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝜑)
116		breq1 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = 𝑒 → (𝑓 finSupp 0 ↔ 𝑒 finSupp 0))
117	116, 12	elrab2 3652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 ∈ 𝐹 ↔ (𝑒 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑒 finSupp 0))
118	117	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 ∈ 𝐹 → 𝑒 ∈ (ℤ ↑m Word 𝐴))
119	55, 48	elmapd 8885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑒 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑒:Word 𝐴⟶ℤ))
120	119	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑒 ∈ (ℤ ↑m Word 𝐴)) → 𝑒:Word 𝐴⟶ℤ)
121	118, 120	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
122	115, 121	sylancom 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
123	122	adantl3r 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
124	123	ffnd 6729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒 Fn Word 𝐴)
125	124	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑒 Fn Word 𝐴)
126	114	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ∈ V)
127		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 0 ∈ ℤ)
128		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
129	125, 126, 127, 128	fvdifsupp 8213	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑒‘𝑤) = 0)
130	129	oveq1d 7455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
131	72	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑀 ∈ Mnd)
132	75	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ⊆ Word 𝐵)
133	128	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐴)
134	132, 133	sseldd 3914	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐵)
135	131, 134, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑀 Σg 𝑤) ∈ 𝐵)
136	135, 81	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
137	130, 136	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
138	117	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 ∈ 𝐹 → 𝑒 finSupp 0)
139	138	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 finSupp 0)
140	139	fsuppimpd 9386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ∈ Fin)
141	86	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
142	123	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑒:Word 𝐴⟶ℤ)
143		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
144	142, 143	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑒‘𝑤) ∈ ℤ)
145	72	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
146	75	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝐵)
147	146	sselda 3913	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
148	145, 147, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
149	2, 11, 141, 144, 148	mulgcld 19332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
150		suppssdm 8219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 supp 0) ⊆ dom 𝑒
151	123	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
152	150, 151	fssdm 6748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ⊆ Word 𝐴)
153	2, 41, 113, 114, 137, 140, 149, 152	gsummptres2 33681	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
154	153	adantllr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
155		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
156	155	mpteq1d 5198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
157	156	oveq2d 7456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
158		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (+g‘𝑅) = (+g‘𝑅)
159		breq1 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
160	159, 12	elrab2 3652	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
161	160	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
162	161	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
163	162	fsuppimpd 9386	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
164	163	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ∈ Fin)
165		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ (𝑔 supp 0))
166	164, 165	ssfid 9285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
167	86	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑅 ∈ Grp)
168	151	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑒:Word 𝐴⟶ℤ)
169		suppssdm 8219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 supp 0) ⊆ dom 𝑔
170		simp-7l 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝜑)
171		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔 ∈ 𝐹)
172	160	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝐹 → 𝑔 ∈ (ℤ ↑m Word 𝐴))
173	55, 48	elmapd 8885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
174	173	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 ∈ (ℤ ↑m Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
175	172, 174	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
176	170, 171, 175	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔:Word 𝐴⟶ℤ)
177	169, 176	fssdm 6748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ⊆ Word 𝐴)
178	165, 177	sstrd 3923	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ Word 𝐴)
179	178	sselda 3913	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑤 ∈ Word 𝐴)
180	168, 179	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑒‘𝑤) ∈ ℤ)
181	179, 148	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑀 Σg 𝑤) ∈ 𝐵)
182	2, 11, 167, 180, 181	mulgcld 19332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))
184	183	eldifbd 4055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ¬ 𝑥 ∈ ℎ)
185	170, 86	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
186	183	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ (𝑔 supp 0))
187	177, 186	sseldd 3914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
188	151, 187	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
189	170, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑀 ∈ Mnd)
190	146, 187	sseldd 3914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐵)
191	78	gsumwcl 19061	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵) → (𝑀 Σg 𝑥) ∈ 𝐵)
192	189, 190, 191	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝐵)
193	2, 11, 185, 188, 192	mulgcld 19332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝐵)
194		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑒‘𝑤) = (𝑒‘𝑥))
195		oveq2 7448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑥))
196	194, 195	oveq12d 7458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑥) · (𝑀 Σg 𝑥)))
197	2, 158, 113, 166, 182, 183, 184, 193, 196	gsumunsn 20201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
198	197	adantllr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
199	154, 157, 198	3eqtrd 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
200	105	ad8antlr 754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubGrp‘𝑅))
201	124	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 Fn Word 𝐴)
202		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
203	201, 187, 202	fmptunsnop 33361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
204	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
205	204	fveq1d 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
206		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))
207		eqidd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ 𝑦 = 𝑥) → 0 = 0)
208	201	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑒 Fn Word 𝐴)
209	114	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → Word 𝐴 ∈ V)
210		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 0 ∈ ℤ)
211		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 = 𝑤)
212		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
213	212	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ Word 𝐴)
214	211, 213	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
215		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
216	212	eldifbd 4055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑤 ∈ ℎ)
217	211, 216	eqneltrd 2884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ ℎ)
218		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑥)
219	218	neqned 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ≠ 𝑥)
220		nelsn 4627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≠ 𝑥 → ¬ 𝑦 ∈ {𝑥})
221	219, 220	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ {𝑥})
222		nelun 33178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (¬ 𝑦 ∈ (𝑒 supp 0) ↔ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})))
223	222	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑒 supp 0) = (ℎ ∪ {𝑥}) ∧ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})) → ¬ 𝑦 ∈ (𝑒 supp 0))
224	215, 217, 221, 223	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ (𝑒 supp 0))
225	214, 224	eldifd 4053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
226	208, 209, 210, 225	fvdifsupp 8213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) = 0)
227	207, 226	ifeqda 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = 0)
228		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
229	228	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ Word 𝐴)
230		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 0 ∈ ℤ)
231	206, 227, 229, 230	fvmptd2 7022	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = 0)
232	205, 231	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = 0)
233	232	oveq1d 7455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
234	229, 148	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑀 Σg 𝑤) ∈ 𝐵)
235	234, 81	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
236	233, 235	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
237	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
238	237	fveq1d 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
239		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
240	151	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
241		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
242	240, 241	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ)
243	239, 242	ifclda 4521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ)
244	243	fmpttd 7136	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
245	244	ffvelcdmda 7105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) ∈ ℤ)
246	238, 245	eqeltrrd 2865	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) ∈ ℤ)
247	2, 11, 141, 246, 148	mulgcld 19332	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
248	2, 41, 113, 114, 236, 166, 247, 178	gsummptres2 33681	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
249	248	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
250	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
251	250	fveq1d 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
252		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
253		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑤 ∈ ℎ)
254	252, 253	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 ∈ ℎ)
255	184	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑥 ∈ ℎ)
256		nelneq 2888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℎ ∧ ¬ 𝑥 ∈ ℎ) → ¬ 𝑦 = 𝑥)
257	254, 255, 256	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑦 = 𝑥)
258	257	iffalsed 4496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑦))
259	252	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → (𝑒‘𝑦) = (𝑒‘𝑤))
260	258, 259	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑤))
261	206, 260, 179, 180	fvmptd2 7022	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (𝑒‘𝑤))
262	251, 261	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = (𝑒‘𝑤))
263	262	oveq1d 7455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))
264	263	mpteq2dva 5201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
265	264	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
266	265	oveq2d 7456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
267	249, 266	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
268		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 ∈ 𝐹)
269	268	resexd 6028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∈ V)
270		snex 5401	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {⟨𝑥, 0⟩} ∈ V
271	270	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → {⟨𝑥, 0⟩} ∈ V)
272	269, 271, 202	suppun2 33345	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)))
273	114, 202, 201	fdifsupp 33346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ((𝑒 supp 0) ∖ {𝑥}))
274		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
275	274	difeq1d 4065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 supp 0) ∖ {𝑥}) = ((ℎ ∪ {𝑥}) ∖ {𝑥}))
276		disjsn 4672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ℎ)
277		undif5 4443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
278	276, 277	sylbir 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ ℎ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
279	184, 278	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
280	273, 275, 279	3eqtrd 2802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ℎ)
281		vex 3458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑥 ∈ V
282		c0ex 11324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 ∈ V
283	281, 282	xpsn 7162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ({𝑥} × {0}) = {⟨𝑥, 0⟩}
284	283	oveq1i 7450	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ({⟨𝑥, 0⟩} supp 0)
285		fczsupp0 8235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ∅
286	284, 285	eqtr3i 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨𝑥, 0⟩} supp 0) = ∅
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ({⟨𝑥, 0⟩} supp 0) = ∅)
288	280, 287	uneq12d 4171	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)) = (ℎ ∪ ∅))
289		un0 4347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∪ ∅) = ℎ
290	289	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (ℎ ∪ ∅) = ℎ)
291	272, 288, 290	3eqtrd 2802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
292	291	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
293		oveq1 7447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0))
294	293	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓 supp 0) = ℎ ↔ (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ))
295		fveq1 6904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
296	295	oveq1d 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))
297	296	mpteq2dv 5202	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))))
298	297	oveq2d 7456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
299	298	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
300	294, 299	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
301		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
302		breq1 5109	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 finSupp 0 ↔ ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0))
303	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℤ ∈ V)
304	114	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
305	203	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
306		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
307		simp-10l 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝜑)
308		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒 ∈ 𝐹)
309	307, 308, 121	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
310		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
311	309, 310	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ)
312	306, 311	ifclda 4521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ)
313	312	fmpttd 7136	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
314	305, 313	feq1dd 6711	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}):Word 𝐴⟶ℤ)
315	303, 304, 314	elmapdd 8886	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ (ℤ ↑m Word 𝐴))
316		0zd 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
317	314	ffund 6733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Fun ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
318	166	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
319	292, 318	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) ∈ Fin)
320	315, 316, 317, 319	isfsuppd 9383	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0)
321	302, 315, 320	elrabd 3650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
322	321, 12	eleqtrrdi 2875	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ 𝐹)
323	300, 301, 322	rspcdva 3581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
324	292, 323	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
325	267, 324	eqeltrrd 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
326	86	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
327	10	subrgsubm 20864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubMnd‘𝑀))
328	327	ad8antlr 754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubMnd‘𝑀))
329		sswrd 14691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝑡 → Word 𝐴 ⊆ Word 𝑡)
330	329	ad7antlr 752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝑡)
331	187	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
332	330, 331	sseldd 3914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝑡)
333		gsumwsubmcl 19059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ (SubMnd‘𝑀) ∧ 𝑥 ∈ Word 𝑡) → (𝑀 Σg 𝑥) ∈ 𝑡)
334	328, 332, 333	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝑡)
335	123	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
336	335, 331	ffvelcdmd 7106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
337	2, 11, 326, 334, 200, 336	subgmulgcld 33671	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝑡)
338	158, 200, 325, 337	subgcld 19373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))) ∈ 𝑡)
339	199, 338	eqeltrd 2864	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
340	339	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
341	340	ralrimiva 3158	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
342	341	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
343	342	anasss 472	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
344		oveq1 7447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑒 supp 0) = (𝑓 supp 0))
345	344	eqeq1d 2765	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
346		fveq1 6904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑓 → (𝑒‘𝑤) = (𝑓‘𝑤))
347	346	oveq1d 7455	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑓 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))
348	347	mpteq2dv 5202	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑓 → (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))))
349	348	oveq2d 7456	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
350	349	eleq1d 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
351	345, 350	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑓 → (((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
352	351	cbvralvw 3244	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
353	343, 352	imbitrdi 254	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
354	31, 34, 37, 40, 112, 353, 163	findcard2d 9207	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
355		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ 𝐹)
356	28, 354, 355	rspcdva 3581	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
357	20, 356	mpd 16	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
358	357	ad4ant13 764	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
359	19, 358	eqeltrd 2864	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 ∈ 𝑡)
360		eqid 2763	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
361	13	eleq2i 2856	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝑆 ↔ 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
362	361	bilani 510	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
363	360, 362	elrnmpt2d 5954	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
364	359, 363	r19.29a 3174	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑡)
365	364	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → (𝑠 ∈ 𝑆 → 𝑠 ∈ 𝑡))
366	365	ssrdv 3919	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → 𝑆 ⊆ 𝑡)
367	366	ex 418	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
368	367	ralrimiva 3158	. . . 4 ⊢ (𝜑 → ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
369		ssintrab 4934	. . . 4 ⊢ (𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ↔ ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
370	368, 369	sylibr 237	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
371	18, 370	eqssd 3930	. 2 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} = 𝑆)
372	8, 371	eqtrd 2798	1 ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  ifcif 4485  {csn 4588  ⟨cop 4838  ∩ cint 4910   class class class wbr 5106   ↦ cmpt 5189   × cxp 5653  ran crn 5656   ↾ cres 5657   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440   supp csupp 8201   ↑_m cmap 8872  Fincfn 8998   finSupp cfsupp 9378  0cc0 11224  ℤcz 12717  Word cword 14682  Basecbs 17413  +_gcplusg 17454  0_gc0g 17636   Σ_g cgsu 17637  Mndcmnd 18949  SubMndcsubmnd 19003  Grpcgrp 19170  ._gcmg 19303  SubGrpcsubg 19356  CMndccmn 20021  mulGrpcmgp 20387  Ringcrg 20486  SubRingcsubrg 20848  RingSpancrgspn 20889

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-inf2 9666  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301  ax-pre-sup 11302  ax-addf 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-isom 6564  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-of 7714  df-om 7899  df-1st 8022  df-2nd 8023  df-supp 8202  df-tpos 8268  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-er 8742  df-map 8874  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-fsupp 9379  df-sup 9458  df-oi 9528  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-div 11998  df-nn 12360  df-2 12429  df-3 12430  df-4 12431  df-5 12432  df-6 12433  df-7 12434  df-8 12435  df-9 12436  df-n0 12631  df-z 12718  df-dec 12839  df-uz 12990  df-rp 13145  df-fz 13664  df-fzo 13813  df-seq 14169  df-exp 14229  df-hash 14499  df-word 14683  df-concat 14740  df-s1 14767  df-substr 14814  df-pfx 14846  df-cj 15292  df-re 15293  df-im 15294  df-sqrt 15428  df-abs 15429  df-clim 15681  df-sum 15880  df-struct 17351  df-sets 17368  df-slot 17386  df-ndx 17398  df-base 17414  df-ress 17435  df-plusg 17467  df-mulr 17468  df-starv 17469  df-tset 17473  df-ple 17474  df-ds 17476  df-unif 17477  df-0g 17638  df-gsum 17639  df-mre 17782  df-mrc 17783  df-acs 17785  df-mgm 18842  df-sgrp 18934  df-mnd 18950  df-mhm 19004  df-submnd 19005  df-grp 19173  df-minusg 19174  df-mulg 19304  df-subg 19359  df-ghm 19454  df-cntz 19558  df-cmn 20023  df-abl 20024  df-mgp 20388  df-rng 20402  df-ur 20435  df-ring 20488  df-cring 20489  df-oppr 20594  df-subrng 20825  df-subrg 20849  df-rgspn 20890  df-cnfld 21706  df-zring 21780

This theorem is used by:  elrgspn  33874