Theorem elrgspnlem4 33345

Description: Lemma for elrgspn 33346. (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 2738	. . 3 ⊢ (𝜑 → (𝑁‘𝐴) = (𝑁‘𝐴))
8	1, 3, 4, 6, 7	rgspnval 20562	. 2 ⊢ (𝜑 → (𝑁‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
9		sseq2 3962	. . . . 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 33343	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
15	2, 10, 11, 5, 12, 1, 4, 13	elrgspnlem3 33344	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
16	9, 14, 15	elrabd 3650	. . . 4 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
17		intss1 4920	. . . 4 ⊢ (𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
19		simpr 484	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
20		eqidd 2738	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) = (𝑔 supp 0))
21		oveq1 7377	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 supp 0) = (𝑔 supp 0))
22	21	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 supp 0) = (𝑔 supp 0) ↔ (𝑔 supp 0) = (𝑔 supp 0)))
23		fveq1 6843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤))
24	23	oveq1d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
25	24	mpteq2dv 5194	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
26	25	oveq2d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
27	26	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
28	22, 27	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
29		eqeq2 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ∅ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ∅))
30	29	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
31	30	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ∅ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
32		eqeq2 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ℎ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ℎ))
33	32	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ℎ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
34	33	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ℎ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
35		eqeq2 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
36	35	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
37	36	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
38		eqeq2 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑔 supp 0) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (𝑔 supp 0)))
39	38	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑔 supp 0) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
40	39	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑔 supp 0) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
41		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝑅) = (0g‘𝑅)
42	1	ringcmnd 20236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ CMnd)
43	42	ad5antr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → 𝑅 ∈ CMnd)
44	2	fvexi 6858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 ∈ V
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
46	45, 4	ssexd 5273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ V)
47		wrdexg 14461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
48	46, 47	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Word 𝐴 ∈ V)
49	48	ad5antr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → Word 𝐴 ∈ V)
50		simp-4l 783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝜑)
51	12	reqabi 3424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ 𝐹 ↔ (𝑓 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑓 finSupp 0))
52	51	simplbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ 𝐹 → 𝑓 ∈ (ℤ ↑m Word 𝐴))
53	52	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (ℤ ↑m Word 𝐴))
54		zex 12511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℤ ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℤ ∈ V)
56	55, 48	elmapd 8791	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑓 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑓:Word 𝐴⟶ℤ))
57	56	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ ↑m Word 𝐴)) → 𝑓:Word 𝐴⟶ℤ)
58	50, 53, 57	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓:Word 𝐴⟶ℤ)
59	58	ffnd 6673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 Fn Word 𝐴)
60	59	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑓 Fn Word 𝐴)
61	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ∈ V)
62		0zd 12514	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 0 ∈ ℤ)
63		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ ∅))
64	63	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐴)
65	63	eldifbd 3916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ ∅)
66		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓 supp 0) = ∅)
67	65, 66	neleqtrrd 2860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ (𝑓 supp 0))
68	64, 67	eldifd 3914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ (𝑓 supp 0)))
69	60, 61, 62, 68	fvdifsupp 8125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓‘𝑤) = 0)
70	69	oveq1d 7385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
71	10	ringmgp 20191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
72	1, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ Mnd)
73	72	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑀 ∈ Mnd)
74		sswrd 14459	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
75	4, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
76	75	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ⊆ Word 𝐵)
77	76, 64	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐵)
78	10, 2	mgpbas 20097	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 = (Base‘𝑀)
79	78	gsumwcl 18778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
80	73, 77, 79	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑀 Σg 𝑤) ∈ 𝐵)
81	2, 41, 11	mulg0 19021	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
83	70, 82	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
84		0fi 8993	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ Fin
85	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ∈ Fin)
86	1	ringgrpd 20194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 ∈ Grp)
87	86	ad6antr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
88	58	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑓:Word 𝐴⟶ℤ)
89		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
90	88, 89	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑓‘𝑤) ∈ ℤ)
91	72	ad6antr 737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
92	75	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
93	92, 89	sseldd 3936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
94	91, 93, 79	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
95	2, 11, 87, 90, 94	mulgcld 19043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
96		0ss 4354	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ⊆ Word 𝐴
97	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ⊆ Word 𝐴)
98	2, 41, 43, 49, 83, 85, 95, 97	gsummptres2 33153	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
99		mpt0 6644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅
100	99	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅)
101	100	oveq2d 7386	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg ∅))
102	41	gsum0 18623	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg ∅) = (0g‘𝑅))
104	98, 101, 103	3eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
105		subrgsubg 20527	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubGrp‘𝑅))
106	41	subg0cl 19081	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubGrp‘𝑅) → (0g‘𝑅) ∈ 𝑡)
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (SubRing‘𝑅) → (0g‘𝑅) ∈ 𝑡)
108	107	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (0g‘𝑅) ∈ 𝑡)
109	108	ad4antr 733	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (0g‘𝑅) ∈ 𝑡)
110	104, 109	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
111	110	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
112	111	ralrimiva 3130	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
113	42	ad7antr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ CMnd)
114	48	ad7antr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
115		simp-5l 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝜑)
116		breq1 5103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = 𝑒 → (𝑓 finSupp 0 ↔ 𝑒 finSupp 0))
117	116, 12	elrab2 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 ∈ 𝐹 ↔ (𝑒 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑒 finSupp 0))
118	117	simplbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 ∈ 𝐹 → 𝑒 ∈ (ℤ ↑m Word 𝐴))
119	55, 48	elmapd 8791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑒 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑒:Word 𝐴⟶ℤ))
120	119	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑒 ∈ (ℤ ↑m Word 𝐴)) → 𝑒:Word 𝐴⟶ℤ)
121	118, 120	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
122	115, 121	sylancom 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
123	122	adantl3r 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
124	123	ffnd 6673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒 Fn Word 𝐴)
125	124	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑒 Fn Word 𝐴)
126	114	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ∈ V)
127		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 0 ∈ ℤ)
128		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
129	125, 126, 127, 128	fvdifsupp 8125	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑒‘𝑤) = 0)
130	129	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
131	72	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑀 ∈ Mnd)
132	75	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ⊆ Word 𝐵)
133	128	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐴)
134	132, 133	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐵)
135	131, 134, 79	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑀 Σg 𝑤) ∈ 𝐵)
136	135, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
137	130, 136	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
138	117	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 ∈ 𝐹 → 𝑒 finSupp 0)
139	138	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 finSupp 0)
140	139	fsuppimpd 9286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ∈ Fin)
141	86	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
142	123	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑒:Word 𝐴⟶ℤ)
143		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
144	142, 143	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑒‘𝑤) ∈ ℤ)
145	72	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
146	75	ad7antr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝐵)
147	146	sselda 3935	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
148	145, 147, 79	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
149	2, 11, 141, 144, 148	mulgcld 19043	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
150		suppssdm 8131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 supp 0) ⊆ dom 𝑒
151	123	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
152	150, 151	fssdm 6691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ⊆ Word 𝐴)
153	2, 41, 113, 114, 137, 140, 149, 152	gsummptres2 33153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
154	153	adantllr 720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
155		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
156	155	mpteq1d 5190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
157	156	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
158		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (+g‘𝑅) = (+g‘𝑅)
159		breq1 5103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
160	159, 12	elrab2 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
161	160	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
162	161	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
163	162	fsuppimpd 9286	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
164	163	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ∈ Fin)
165		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ (𝑔 supp 0))
166	164, 165	ssfid 9183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
167	86	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑅 ∈ Grp)
168	151	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑒:Word 𝐴⟶ℤ)
169		suppssdm 8131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 supp 0) ⊆ dom 𝑔
170		simp-7l 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝜑)
171		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔 ∈ 𝐹)
172	160	simplbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝐹 → 𝑔 ∈ (ℤ ↑m Word 𝐴))
173	55, 48	elmapd 8791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
174	173	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 ∈ (ℤ ↑m Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
175	172, 174	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
176	170, 171, 175	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔:Word 𝐴⟶ℤ)
177	169, 176	fssdm 6691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ⊆ Word 𝐴)
178	165, 177	sstrd 3946	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ Word 𝐴)
179	178	sselda 3935	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑤 ∈ Word 𝐴)
180	168, 179	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑒‘𝑤) ∈ ℤ)
181	179, 148	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑀 Σg 𝑤) ∈ 𝐵)
182	2, 11, 167, 180, 181	mulgcld 19043	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))
184	183	eldifbd 3916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ¬ 𝑥 ∈ ℎ)
185	170, 86	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
186	183	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ (𝑔 supp 0))
187	177, 186	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
188	151, 187	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
189	170, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑀 ∈ Mnd)
190	146, 187	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐵)
191	78	gsumwcl 18778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵) → (𝑀 Σg 𝑥) ∈ 𝐵)
192	189, 190, 191	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝐵)
193	2, 11, 185, 188, 192	mulgcld 19043	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝐵)
194		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑒‘𝑤) = (𝑒‘𝑥))
195		oveq2 7378	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑥))
196	194, 195	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑥) · (𝑀 Σg 𝑥)))
197	2, 158, 113, 166, 182, 183, 184, 193, 196	gsumunsn 19906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
198	197	adantllr 720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
199	154, 157, 198	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
200	105	ad8antlr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubGrp‘𝑅))
201	124	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 Fn Word 𝐴)
202		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
203	201, 187, 202	fmptunsnop 32796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
204	203	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
205	204	fveq1d 6846	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
206		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))
207		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ 𝑦 = 𝑥) → 0 = 0)
208	201	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑒 Fn Word 𝐴)
209	114	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → Word 𝐴 ∈ V)
210		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 0 ∈ ℤ)
211		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 = 𝑤)
212		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
213	212	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ Word 𝐴)
214	211, 213	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
215		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
216	212	eldifbd 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑤 ∈ ℎ)
217	211, 216	eqneltrd 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ ℎ)
218		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑥)
219	218	neqned 2940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ≠ 𝑥)
220		nelsn 4625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≠ 𝑥 → ¬ 𝑦 ∈ {𝑥})
221	219, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ {𝑥})
222		nelun 32606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (¬ 𝑦 ∈ (𝑒 supp 0) ↔ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})))
223	222	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑒 supp 0) = (ℎ ∪ {𝑥}) ∧ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})) → ¬ 𝑦 ∈ (𝑒 supp 0))
224	215, 217, 221, 223	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ (𝑒 supp 0))
225	214, 224	eldifd 3914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
226	208, 209, 210, 225	fvdifsupp 8125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) = 0)
227	207, 226	ifeqda 4518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = 0)
228		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
229	228	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ Word 𝐴)
230		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 0 ∈ ℤ)
231	206, 227, 229, 230	fvmptd2 6960	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = 0)
232	205, 231	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = 0)
233	232	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
234	229, 148	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑀 Σg 𝑤) ∈ 𝐵)
235	234, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
236	233, 235	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
237	203	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
238	237	fveq1d 6846	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
239		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
240	151	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
241		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
242	240, 241	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ)
243	239, 242	ifclda 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ)
244	243	fmpttd 7071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
245	244	ffvelcdmda 7040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) ∈ ℤ)
246	238, 245	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) ∈ ℤ)
247	2, 11, 141, 246, 148	mulgcld 19043	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
248	2, 41, 113, 114, 236, 166, 247, 178	gsummptres2 33153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
249	248	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
251	250	fveq1d 6846	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
252		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
253		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑤 ∈ ℎ)
254	252, 253	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 ∈ ℎ)
255	184	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑥 ∈ ℎ)
256		nelneq 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℎ ∧ ¬ 𝑥 ∈ ℎ) → ¬ 𝑦 = 𝑥)
257	254, 255, 256	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑦 = 𝑥)
258	257	iffalsed 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑦))
259	252	fveq2d 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → (𝑒‘𝑦) = (𝑒‘𝑤))
260	258, 259	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑤))
261	206, 260, 179, 180	fvmptd2 6960	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (𝑒‘𝑤))
262	251, 261	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = (𝑒‘𝑤))
263	262	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))
264	263	mpteq2dva 5193	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
265	264	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
266	265	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
267	249, 266	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
268		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 ∈ 𝐹)
269	268	resexd 5997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∈ V)
270		snex 5387	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {⟨𝑥, 0⟩} ∈ V
271	270	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → {⟨𝑥, 0⟩} ∈ V)
272	269, 271, 202	suppun2 32780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)))
273	114, 202, 201	fdifsupp 32781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ((𝑒 supp 0) ∖ {𝑥}))
274		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
275	274	difeq1d 4079	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 supp 0) ∖ {𝑥}) = ((ℎ ∪ {𝑥}) ∖ {𝑥}))
276		disjsn 4670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ℎ)
277		undif5 4439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
278	276, 277	sylbir 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ ℎ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
279	184, 278	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
280	273, 275, 279	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ℎ)
281		vex 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑥 ∈ V
282		c0ex 11140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 ∈ V
283	281, 282	xpsn 7098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ({𝑥} × {0}) = {⟨𝑥, 0⟩}
284	283	oveq1i 7380	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ({⟨𝑥, 0⟩} supp 0)
285		fczsupp0 8147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ∅
286	284, 285	eqtr3i 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨𝑥, 0⟩} supp 0) = ∅
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ({⟨𝑥, 0⟩} supp 0) = ∅)
288	280, 287	uneq12d 4123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)) = (ℎ ∪ ∅))
289		un0 4348	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∪ ∅) = ℎ
290	289	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (ℎ ∪ ∅) = ℎ)
291	272, 288, 290	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
292	291	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
293		oveq1 7377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0))
294	293	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓 supp 0) = ℎ ↔ (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ))
295		fveq1 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
296	295	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))
297	296	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))))
298	297	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
299	298	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
300	294, 299	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
301		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
302		breq1 5103	. . . . . . . . . . . . . . . . . . . . . . . . . 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 720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
305	203	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
306		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
307		simp-10l 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝜑)
308		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒 ∈ 𝐹)
309	307, 308, 121	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
310		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
311	309, 310	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ)
312	306, 311	ifclda 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ)
313	312	fmpttd 7071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
314	305, 313	feq1dd 6655	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}):Word 𝐴⟶ℤ)
315	303, 304, 314	elmapdd 8792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ (ℤ ↑m Word 𝐴))
316		0zd 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
317	314	ffund 6676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Fun ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
318	166	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
319	292, 318	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) ∈ Fin)
320	315, 316, 317, 319	isfsuppd 9283	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ 𝐹)
323	300, 301, 322	rspcdva 3579	. . . . . . . . . . . . . . . . . . . . . . 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 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
325	267, 324	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
326	86	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
327	10	subrgsubm 20535	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubMnd‘𝑀))
328	327	ad8antlr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubMnd‘𝑀))
329		sswrd 14459	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝑡 → Word 𝐴 ⊆ Word 𝑡)
330	329	ad7antlr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝑡)
331	187	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
332	330, 331	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝑡)
333		gsumwsubmcl 18776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ (SubMnd‘𝑀) ∧ 𝑥 ∈ Word 𝑡) → (𝑀 Σg 𝑥) ∈ 𝑡)
334	328, 332, 333	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝑡)
335	123	ad4ant13 752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
336	335, 331	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
337	2, 11, 326, 334, 200, 336	subgmulgcld 33143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝑡)
338	158, 200, 325, 337	subgcld 33141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))) ∈ 𝑡)
339	199, 338	eqeltrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
340	339	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
341	340	ralrimiva 3130	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
342	341	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
343	342	anasss 466	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
344		oveq1 7377	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑒 supp 0) = (𝑓 supp 0))
345	344	eqeq1d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
346		fveq1 6843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑓 → (𝑒‘𝑤) = (𝑓‘𝑤))
347	346	oveq1d 7385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑓 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))
348	347	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑓 → (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))))
349	348	oveq2d 7386	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
350	349	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
351	345, 350	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑓 → (((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
352	351	cbvralvw 3216	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
353	343, 352	imbitrdi 251	. . . . . . . . . . . . . 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 9105	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
355		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ 𝐹)
356	28, 354, 355	rspcdva 3579	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
357	20, 356	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
358	357	ad4ant13 752	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
359	19, 358	eqeltrd 2837	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 ∈ 𝑡)
360		eqid 2737	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
361	13	eleq2i 2829	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝑆 ↔ 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
362	361	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝑆 → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
363	362	adantl 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
364	360, 363	elrnmpt2d 5925	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
365	359, 364	r19.29a 3146	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑡)
366	365	ex 412	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → (𝑠 ∈ 𝑆 → 𝑠 ∈ 𝑡))
367	366	ssrdv 3941	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → 𝑆 ⊆ 𝑡)
368	367	ex 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
369	368	ralrimiva 3130	. . . 4 ⊢ (𝜑 → ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
370		ssintrab 4928	. . . 4 ⊢ (𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ↔ ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
371	369, 370	sylibr 234	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
372	18, 371	eqssd 3953	. 2 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} = 𝑆)
373	8, 372	eqtrd 2772	1 ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  {crab 3401  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  ifcif 4481  {csn 4582  ⟨cop 4588  ∩ cint 4904   class class class wbr 5100   ↦ cmpt 5181   × cxp 5632  ran crn 5635   ↾ cres 5636   Fn wfn 6497  ⟶wf 6498  ‘cfv 6502  (class class class)co 7370   supp csupp 8114   ↑_m cmap 8777  Fincfn 8897   finSupp cfsupp 9278  0cc0 11040  ℤcz 12502  Word cword 14450  Basecbs 17150  +_gcplusg 17191  0_gc0g 17373   Σ_g cgsu 17374  Mndcmnd 18673  SubMndcsubmnd 18721  Grpcgrp 18880  ._gcmg 19014  SubGrpcsubg 19067  CMndccmn 19726  mulGrpcmgp 20092  Ringcrg 20185  SubRingcsubrg 20519  RingSpancrgspn 20560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-inf2 9564  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118  ax-addf 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-se 5588  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-isom 6511  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-of 7634  df-om 7821  df-1st 7945  df-2nd 7946  df-supp 8115  df-tpos 8180  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-2o 8410  df-er 8647  df-map 8779  df-en 8898  df-dom 8899  df-sdom 8900  df-fin 8901  df-fsupp 9279  df-sup 9359  df-oi 9429  df-card 9865  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809  df-nn 12160  df-2 12222  df-3 12223  df-4 12224  df-5 12225  df-6 12226  df-7 12227  df-8 12228  df-9 12229  df-n0 12416  df-z 12503  df-dec 12622  df-uz 12766  df-rp 12920  df-fz 13438  df-fzo 13585  df-seq 13939  df-exp 13999  df-hash 14268  df-word 14451  df-concat 14508  df-s1 14534  df-substr 14579  df-pfx 14609  df-cj 15036  df-re 15037  df-im 15038  df-sqrt 15172  df-abs 15173  df-clim 15425  df-sum 15624  df-struct 17088  df-sets 17105  df-slot 17123  df-ndx 17135  df-base 17151  df-ress 17172  df-plusg 17204  df-mulr 17205  df-starv 17206  df-tset 17210  df-ple 17211  df-ds 17213  df-unif 17214  df-0g 17375  df-gsum 17376  df-mre 17519  df-mrc 17520  df-acs 17522  df-mgm 18579  df-sgrp 18658  df-mnd 18674  df-mhm 18722  df-submnd 18723  df-grp 18883  df-minusg 18884  df-mulg 19015  df-subg 19070  df-ghm 19159  df-cntz 19263  df-cmn 19728  df-abl 19729  df-mgp 20093  df-rng 20105  df-ur 20134  df-ring 20187  df-cring 20188  df-oppr 20290  df-subrng 20496  df-subrg 20520  df-rgspn 20561  df-cnfld 21327  df-zring 21419

This theorem is referenced by:  elrgspn  33346