Theorem elrgspnlem4 33428

Description: Lemma for elrgspn 33429. (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 2765	. . 3 ⊢ (𝜑 → (𝑁‘𝐴) = (𝑁‘𝐴))
8	1, 3, 4, 6, 7	rgspnval 20664	. 2 ⊢ (𝜑 → (𝑁‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
9		sseq2 3964	. . . . 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 33426	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
15	2, 10, 11, 5, 12, 1, 4, 13	elrgspnlem3 33427	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
16	9, 14, 15	elrabd 3654	. . . 4 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
17		intss1 4923	. . . 4 ⊢ (𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
19		simpr 488	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
20		eqidd 2765	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) = (𝑔 supp 0))
21		oveq1 7405	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 supp 0) = (𝑔 supp 0))
22	21	eqeq1d 2766	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 supp 0) = (𝑔 supp 0) ↔ (𝑔 supp 0) = (𝑔 supp 0)))
23		fveq1 6868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤))
24	23	oveq1d 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
25	24	mpteq2dv 5196	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
26	25	oveq2d 7414	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
27	26	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
28	22, 27	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
29		eqeq2 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ∅ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ∅))
30	29	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
31	30	ralbidv 3187	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ∅ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
32		eqeq2 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ℎ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ℎ))
33	32	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ℎ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
34	33	ralbidv 3187	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ℎ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
35		eqeq2 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
36	35	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
37	36	ralbidv 3187	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
38		eqeq2 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑔 supp 0) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (𝑔 supp 0)))
39	38	imbi1d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑔 supp 0) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
40	39	ralbidv 3187	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑔 supp 0) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
41		eqid 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝑅) = (0g‘𝑅)
42	1	ringcmnd 20336	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ CMnd)
43	42	ad5antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → 𝑅 ∈ CMnd)
44	2	fvexi 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 ∈ V
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
46	45, 4	ssexd 5282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ V)
47		wrdexg 14539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
48	46, 47	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Word 𝐴 ∈ V)
49	48	ad5antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → Word 𝐴 ∈ V)
50		simp-4l 792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝜑)
51	12	reqabi 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ 𝐹 ↔ (𝑓 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑓 finSupp 0))
52	51	simplbi 500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ 𝐹 → 𝑓 ∈ (ℤ ↑m Word 𝐴))
53	52	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (ℤ ↑m Word 𝐴))
54		zex 12579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℤ ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℤ ∈ V)
56	55, 48	elmapd 8823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑓 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑓:Word 𝐴⟶ℤ))
57	56	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ ↑m Word 𝐴)) → 𝑓:Word 𝐴⟶ℤ)
58	50, 53, 57	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓:Word 𝐴⟶ℤ)
59	58	ffnd 6694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 Fn Word 𝐴)
60	59	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑓 Fn Word 𝐴)
61	49	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ∈ V)
62		0zd 12582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 0 ∈ ℤ)
63		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ ∅))
64	63	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐴)
65	63	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ ∅)
66		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓 supp 0) = ∅)
67	65, 66	neleqtrrd 2887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ (𝑓 supp 0))
68	64, 67	eldifd 3917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ (𝑓 supp 0)))
69	60, 61, 62, 68	fvdifsupp 8153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓‘𝑤) = 0)
70	69	oveq1d 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
71	10	ringmgp 20291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
72	1, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ Mnd)
73	72	ad6antr 746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑀 ∈ Mnd)
74		sswrd 14537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
75	4, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
76	75	ad6antr 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ⊆ Word 𝐵)
77	76, 64	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐵)
78	10, 2	mgpbas 20193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 = (Base‘𝑀)
79	78	gsumwcl 18875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
80	73, 77, 79	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑀 Σg 𝑤) ∈ 𝐵)
81	2, 41, 11	mulg0 19118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
83	70, 82	eqtrd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
84		0fi 9025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ Fin
85	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ∈ Fin)
86	1	ringgrpd 20294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 ∈ Grp)
87	86	ad6antr 746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
88	58	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑓:Word 𝐴⟶ℤ)
89		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
90	88, 89	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑓‘𝑤) ∈ ℤ)
91	72	ad6antr 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
92	75	ad6antr 746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
93	92, 89	sseldd 3939	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
94	91, 93, 79	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
95	2, 11, 87, 90, 94	mulgcld 19140	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
96		0ss 4356	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ⊆ Word 𝐴
97	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ⊆ Word 𝐴)
98	2, 41, 43, 49, 83, 85, 95, 97	gsummptres2 33235	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
99		mpt0 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅
100	99	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅)
101	100	oveq2d 7414	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg ∅))
102	41	gsum0 18720	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg ∅) = (0g‘𝑅))
104	98, 101, 103	3eqtrd 2803	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
105		subrgsubg 20629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubGrp‘𝑅))
106	41	subg0cl 19178	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubGrp‘𝑅) → (0g‘𝑅) ∈ 𝑡)
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (SubRing‘𝑅) → (0g‘𝑅) ∈ 𝑡)
108	107	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (0g‘𝑅) ∈ 𝑡)
109	108	ad4antr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (0g‘𝑅) ∈ 𝑡)
110	104, 109	eqeltrd 2864	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
111	110	ex 416	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
112	111	ralrimiva 3156	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
113	42	ad7antr 748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ CMnd)
114	48	ad7antr 748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
115		simp-5l 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝜑)
116		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = 𝑒 → (𝑓 finSupp 0 ↔ 𝑒 finSupp 0))
117	116, 12	elrab2 3656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 ∈ 𝐹 ↔ (𝑒 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑒 finSupp 0))
118	117	simplbi 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 ∈ 𝐹 → 𝑒 ∈ (ℤ ↑m Word 𝐴))
119	55, 48	elmapd 8823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑒 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑒:Word 𝐴⟶ℤ))
120	119	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑒 ∈ (ℤ ↑m Word 𝐴)) → 𝑒:Word 𝐴⟶ℤ)
121	118, 120	sylan2 602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
122	115, 121	sylancom 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
123	122	adantl3r 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
124	123	ffnd 6694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒 Fn Word 𝐴)
125	124	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑒 Fn Word 𝐴)
126	114	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ∈ V)
127		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 0 ∈ ℤ)
128		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
129	125, 126, 127, 128	fvdifsupp 8153	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑒‘𝑤) = 0)
130	129	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
131	72	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑀 ∈ Mnd)
132	75	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ⊆ Word 𝐵)
133	128	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐴)
134	132, 133	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐵)
135	131, 134, 79	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
138	117	simprbi 501	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 ∈ 𝐹 → 𝑒 finSupp 0)
139	138	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 finSupp 0)
140	139	fsuppimpd 9317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ∈ Fin)
141	86	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
142	123	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑒:Word 𝐴⟶ℤ)
143		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
144	142, 143	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑒‘𝑤) ∈ ℤ)
145	72	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
146	75	ad7antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝐵)
147	146	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
148	145, 147, 79	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
149	2, 11, 141, 144, 148	mulgcld 19140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
150		suppssdm 8159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 supp 0) ⊆ dom 𝑒
151	123	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
152	150, 151	fssdm 6713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ⊆ Word 𝐴)
153	2, 41, 113, 114, 137, 140, 149, 152	gsummptres2 33235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
154	153	adantllr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
155		simpr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
156	155	mpteq1d 5192	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
157	156	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
158		eqid 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (+g‘𝑅) = (+g‘𝑅)
159		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
160	159, 12	elrab2 3656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
161	160	simprbi 501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
162	161	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
163	162	fsuppimpd 9317	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
164	163	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ∈ Fin)
165		simp-4r 793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ (𝑔 supp 0))
166	164, 165	ssfid 9215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
167	86	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑅 ∈ Grp)
168	151	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑒:Word 𝐴⟶ℤ)
169		suppssdm 8159	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 supp 0) ⊆ dom 𝑔
170		simp-7l 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝜑)
171		simp-5r 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔 ∈ 𝐹)
172	160	simplbi 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝐹 → 𝑔 ∈ (ℤ ↑m Word 𝐴))
173	55, 48	elmapd 8823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
174	173	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 ∈ (ℤ ↑m Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
175	172, 174	sylan2 602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
176	170, 171, 175	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔:Word 𝐴⟶ℤ)
177	169, 176	fssdm 6713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ⊆ Word 𝐴)
178	165, 177	sstrd 3948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ Word 𝐴)
179	178	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑤 ∈ Word 𝐴)
180	168, 179	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑒‘𝑤) ∈ ℤ)
181	179, 148	syldan 600	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑀 Σg 𝑤) ∈ 𝐵)
182	2, 11, 167, 180, 181	mulgcld 19140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183		simpllr 785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))
184	183	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ (𝑔 supp 0))
187	177, 186	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
188	151, 187	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . 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 3939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐵)
191	78	gsumwcl 18875	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵) → (𝑀 Σg 𝑥) ∈ 𝐵)
192	189, 190, 191	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝐵)
193	2, 11, 185, 188, 192	mulgcld 19140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝐵)
194		fveq2 6869	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑒‘𝑤) = (𝑒‘𝑥))
195		oveq2 7406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑥))
196	194, 195	oveq12d 7416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑥) · (𝑀 Σg 𝑥)))
197	2, 158, 113, 166, 182, 183, 184, 193, 196	gsumunsn 20002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
198	197	adantllr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
199	154, 157, 198	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
200	105	ad8antlr 751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubGrp‘𝑅))
201	124	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 Fn Word 𝐴)
202		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
203	201, 187, 202	fmptunsnop 32904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
204	203	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
205	204	fveq1d 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
206		eqid 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))
207		eqidd 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ 𝑦 = 𝑥) → 0 = 0)
208	201	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑒 Fn Word 𝐴)
209	114	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → Word 𝐴 ∈ V)
210		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 0 ∈ ℤ)
211		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 = 𝑤)
212		simpllr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
213	212	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
216	212	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ {𝑥})
222		nelun 32714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (¬ 𝑦 ∈ (𝑒 supp 0) ↔ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})))
223	222	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑒 supp 0) = (ℎ ∪ {𝑥}) ∧ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})) → ¬ 𝑦 ∈ (𝑒 supp 0))
224	215, 217, 221, 223	syl12anc 847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ (𝑒 supp 0))
225	214, 224	eldifd 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
226	208, 209, 210, 225	fvdifsupp 8153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) = 0)
227	207, 226	ifeqda 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = 0)
228		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
229	228	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ Word 𝐴)
230		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 0 ∈ ℤ)
231	206, 227, 229, 230	fvmptd2 6986	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = 0)
232	205, 231	eqtr3d 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = 0)
233	232	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
234	229, 148	syldan 600	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
237	203	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
238	237	fveq1d 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
239		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
240	151	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
241		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
242	240, 241	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ)
243	239, 242	ifclda 4518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ)
244	243	fmpttd 7098	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
245	244	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 19140	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
248	2, 41, 113, 114, 236, 166, 247, 178	gsummptres2 33235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
249	248	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
251	250	fveq1d 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
252		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
253		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑤 ∈ ℎ)
254	252, 253	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 ∈ ℎ)
255	184	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑥 ∈ ℎ)
256		nelneq 2888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℎ ∧ ¬ 𝑥 ∈ ℎ) → ¬ 𝑦 = 𝑥)
257	254, 255, 256	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑦 = 𝑥)
258	257	iffalsed 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑦))
259	252	fveq2d 6873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → (𝑒‘𝑦) = (𝑒‘𝑤))
260	258, 259	eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑤))
261	206, 260, 179, 180	fvmptd2 6986	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (𝑒‘𝑤))
262	251, 261	eqtr3d 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = (𝑒‘𝑤))
263	262	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))
264	263	mpteq2dva 5195	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
265	264	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
266	265	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
267	249, 266	eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
268		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 ∈ 𝐹)
269	268	resexd 6016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∈ V)
270		snex 5398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {⟨𝑥, 0⟩} ∈ V
271	270	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → {⟨𝑥, 0⟩} ∈ V)
272	269, 271, 202	suppun2 32888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)))
273	114, 202, 201	fdifsupp 32889	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ((𝑒 supp 0) ∖ {𝑥}))
274		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
275	274	difeq1d 4081	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 supp 0) ∖ {𝑥}) = ((ℎ ∪ {𝑥}) ∖ {𝑥}))
276		disjsn 4672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ℎ)
277		undif5 4440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
278	276, 277	sylbir 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ ℎ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
279	184, 278	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
280	273, 275, 279	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ℎ)
281		vex 3460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑥 ∈ V
282		c0ex 11175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 ∈ V
283	281, 282	xpsn 7125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ({𝑥} × {0}) = {⟨𝑥, 0⟩}
284	283	oveq1i 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ({⟨𝑥, 0⟩} supp 0)
285		fczsupp0 8175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ∅
286	284, 285	eqtr3i 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨𝑥, 0⟩} supp 0) = ∅
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ({⟨𝑥, 0⟩} supp 0) = ∅)
288	280, 287	uneq12d 4124	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)) = (ℎ ∪ ∅))
289		un0 4350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∪ ∅) = ℎ
290	289	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (ℎ ∪ ∅) = ℎ)
291	272, 288, 290	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
292	291	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
293		oveq1 7405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0))
294	293	eqeq1d 2766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓 supp 0) = ℎ ↔ (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ))
295		fveq1 6868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
296	295	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))
297	296	mpteq2dv 5196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))))
298	297	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . . . . 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 346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
301		simpllr 785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
302		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
305	203	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
306		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
307		simp-10l 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝜑)
308		simp-4r 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒 ∈ 𝐹)
309	307, 308, 121	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
310		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
311	309, 310	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ)
312	306, 311	ifclda 4518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ)
313	312	fmpttd 7098	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
314	305, 313	feq1dd 6676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}):Word 𝐴⟶ℤ)
315	303, 304, 314	elmapdd 8824	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ (ℤ ↑m Word 𝐴))
316		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
317	314	ffund 6698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Fun ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
318	166	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9314	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0)
321	302, 315, 320	elrabd 3654	. . . . . . . . . . . . . . . . . . . . . . . . 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 3584	. . . . . . . . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
326	86	ad8antr 750	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
327	10	subrgsubm 20637	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubMnd‘𝑀))
328	327	ad8antlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubMnd‘𝑀))
329		sswrd 14537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝑡 → Word 𝐴 ⊆ Word 𝑡)
330	329	ad7antlr 749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝑡)
331	187	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
332	330, 331	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝑡)
333		gsumwsubmcl 18873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ (SubMnd‘𝑀) ∧ 𝑥 ∈ Word 𝑡) → (𝑀 Σg 𝑥) ∈ 𝑡)
334	328, 332, 333	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝑡)
335	123	ad4ant13 761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
336	335, 331	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
337	2, 11, 326, 334, 200, 336	subgmulgcld 33225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝑡)
338	158, 200, 325, 337	subgcld 33223	. . . . . . . . . . . . . . . . . . . 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 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
341	340	ralrimiva 3156	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
342	341	ex 416	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
343	342	anasss 470	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
344		oveq1 7405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑒 supp 0) = (𝑓 supp 0))
345	344	eqeq1d 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
346		fveq1 6868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑓 → (𝑒‘𝑤) = (𝑓‘𝑤))
347	346	oveq1d 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑓 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))
348	347	mpteq2dv 5196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑓 → (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))))
349	348	oveq2d 7414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
350	349	eleq1d 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
351	345, 350	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑓 → (((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
352	351	cbvralvw 3242	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
353	343, 352	imbitrdi 253	. . . . . . . . . . . . . 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 9137	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
355		simpr 488	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ 𝐹)
356	28, 354, 355	rspcdva 3584	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
357	20, 356	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
358	357	ad4ant13 761	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
359	19, 358	eqeltrd 2864	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 ∈ 𝑡)
360		eqid 2764	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
361	13	eleq2i 2856	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝑆 ↔ 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
362	361	bilani 508	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
363	360, 362	elrnmpt2d 5944	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
364	359, 363	r19.29a 3172	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑡)
365	364	ex 416	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → (𝑠 ∈ 𝑆 → 𝑠 ∈ 𝑡))
366	365	ssrdv 3944	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → 𝑆 ⊆ 𝑡)
367	366	ex 416	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
368	367	ralrimiva 3156	. . . 4 ⊢ (𝜑 → ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
369		ssintrab 4931	. . . 4 ⊢ (𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ↔ ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
370	368, 369	sylibr 236	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
371	18, 370	eqssd 3955	. 2 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} = 𝑆)
372	8, 371	eqtrd 2799	1 ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144   ≠ wne 2959  ∀wral 3078  {crab 3416  Vcvv 3456   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287  ifcif 4482  {csn 4584  ⟨cop 4590  ∩ cint 4907   class class class wbr 5102   ↦ cmpt 5183   × cxp 5647  ran crn 5650   ↾ cres 5651   Fn wfn 6518  ⟶wf 6519  ‘cfv 6523  (class class class)co 7398   supp csupp 8142   ↑_m cmap 8810  Fincfn 8929   finSupp cfsupp 9309  0cc0 11075  ℤcz 12570  Word cword 14528  Basecbs 17247  +_gcplusg 17288  0_gc0g 17470   Σ_g cgsu 17471  Mndcmnd 18770  SubMndcsubmnd 18818  Grpcgrp 18977  ._gcmg 19111  SubGrpcsubg 19164  CMndccmn 19822  mulGrpcmgp 20188  Ringcrg 20285  SubRingcsubrg 20621  RingSpancrgspn 20662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-inf2 9598  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-se 5603  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-of 7662  df-om 7849  df-1st 7972  df-2nd 7973  df-supp 8143  df-tpos 8208  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-2o 8440  df-er 8680  df-map 8812  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-fsupp 9310  df-sup 9390  df-oi 9460  df-card 9899  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12484  df-z 12571  df-dec 12691  df-uz 12842  df-rp 12996  df-fz 13515  df-fzo 13662  df-seq 14017  df-exp 14077  df-hash 14346  df-word 14529  df-concat 14586  df-s1 14612  df-substr 14657  df-pfx 14687  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265  df-clim 15517  df-sum 15716  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17248  df-ress 17269  df-plusg 17301  df-mulr 17302  df-starv 17303  df-tset 17307  df-ple 17308  df-ds 17310  df-unif 17311  df-0g 17472  df-gsum 17473  df-mre 17616  df-mrc 17617  df-acs 17619  df-mgm 18676  df-sgrp 18755  df-mnd 18771  df-mhm 18819  df-submnd 18820  df-grp 18980  df-minusg 18981  df-mulg 19112  df-subg 19167  df-ghm 19256  df-cntz 19359  df-cmn 19824  df-abl 19825  df-mgp 20189  df-rng 20201  df-ur 20234  df-ring 20287  df-cring 20288  df-oppr 20388  df-subrng 20598  df-subrg 20622  df-rgspn 20663  df-cnfld 21427  df-zring 21501

This theorem is referenced by:  elrgspn  33429