Theorem elrgspnlem4 33717

Description: Lemma for elrgspn 33718. (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 2761	. . 3 ⊢ (𝜑 → (𝑁‘𝐴) = (𝑁‘𝐴))
8	1, 3, 4, 6, 7	rgspnval 20803	. 2 ⊢ (𝜑 → (𝑁‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
9		sseq2 3957	. . . . 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 33715	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
15	2, 10, 11, 5, 12, 1, 4, 13	elrgspnlem3 33716	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
16	9, 14, 15	elrabd 3647	. . . 4 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
17		intss1 4923	. . . 4 ⊢ (𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
18	16, 17	syl 18	. . 3 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆)
19		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
20		eqidd 2761	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) = (𝑔 supp 0))
21		oveq1 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 supp 0) = (𝑔 supp 0))
22	21	eqeq1d 2762	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 supp 0) = (𝑔 supp 0) ↔ (𝑔 supp 0) = (𝑔 supp 0)))
23		fveq1 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤))
24	23	oveq1d 7431	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
25	24	mpteq2dv 5199	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
26	25	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
27	26	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
28	22, 27	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
29		eqeq2 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ∅ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ∅))
30	29	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
31	30	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ∅ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
32		eqeq2 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = ℎ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ℎ))
33	32	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ℎ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
34	33	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑖 = ℎ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
35		eqeq2 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
36	35	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
37	36	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (ℎ ∪ {𝑥}) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
38		eqeq2 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑔 supp 0) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (𝑔 supp 0)))
39	38	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑔 supp 0) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
40	39	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑔 supp 0) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
41		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝑅) = (0g‘𝑅)
42	1	ringcmnd 20452	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ CMnd)
43	42	ad5antr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → 𝑅 ∈ CMnd)
44	2	fvexi 6895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 ∈ V
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
46	45, 4	ssexd 5289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ V)
47		wrdexg 14614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
48	46, 47	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Word 𝐴 ∈ V)
49	48	ad5antr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → Word 𝐴 ∈ V)
50		simp-4l 795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝜑)
51	12	reqabi 3434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ 𝐹 ↔ (𝑓 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑓 finSupp 0))
52	51	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ 𝐹 → 𝑓 ∈ (ℤ ↑m Word 𝐴))
53	52	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (ℤ ↑m Word 𝐴))
54		zex 12649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℤ ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℤ ∈ V)
56	55, 48	elmapd 8846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑓 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑓:Word 𝐴⟶ℤ))
57	56	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ ↑m Word 𝐴)) → 𝑓:Word 𝐴⟶ℤ)
58	50, 53, 57	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓:Word 𝐴⟶ℤ)
59	58	ffnd 6706	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 Fn Word 𝐴)
60	59	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑓 Fn Word 𝐴)
61	49	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ∈ V)
62		0zd 12652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 0 ∈ ℤ)
63		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ ∅))
64	63	eldifad 3911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐴)
65	63	eldifbd 3912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ ∅)
66		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓 supp 0) = ∅)
67	65, 66	neleqtrrd 2883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ (𝑓 supp 0))
68	64, 67	eldifd 3910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ (𝑓 supp 0)))
69	60, 61, 62, 68	fvdifsupp 8174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓‘𝑤) = 0)
70	69	oveq1d 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
71	10	ringmgp 20404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
72	1, 71	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ Mnd)
73	72	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑀 ∈ Mnd)
74		sswrd 14612	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
75	4, 74	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
76	75	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ⊆ Word 𝐵)
77	76, 64	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐵)
78	10, 2	mgpbas 20304	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 = (Base‘𝑀)
79	78	gsumwcl 18974	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
80	73, 77, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑀 Σg 𝑤) ∈ 𝐵)
81	2, 41, 11	mulg0 19223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
82	80, 81	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
83	70, 82	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
84		0fi 9056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ Fin
85	84	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ∈ Fin)
86	1	ringgrpd 20408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 ∈ Grp)
87	86	ad6antr 749	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
88	58	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑓:Word 𝐴⟶ℤ)
89		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
90	88, 89	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑓‘𝑤) ∈ ℤ)
91	72	ad6antr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
92	75	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
93	92, 89	sseldd 3932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
94	91, 93, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
95	2, 11, 87, 90, 94	mulgcld 19245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
96		0ss 4350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ⊆ Word 𝐴
97	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ⊆ Word 𝐴)
98	2, 41, 43, 49, 83, 85, 95, 97	gsummptres2 33525	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
99		mpt0 6677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅
100	99	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅)
101	100	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg ∅))
102	41	gsum0 18812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg ∅) = (0g‘𝑅))
104	98, 101, 103	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
105		subrgsubg 20768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubGrp‘𝑅))
106	41	subg0cl 19283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (SubGrp‘𝑅) → (0g‘𝑅) ∈ 𝑡)
107	105, 106	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (SubRing‘𝑅) → (0g‘𝑅) ∈ 𝑡)
108	107	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (0g‘𝑅) ∈ 𝑡)
109	108	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (0g‘𝑅) ∈ 𝑡)
110	104, 109	eqeltrd 2860	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
111	110	ex 418	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
112	111	ralrimiva 3154	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
113	42	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ CMnd)
114	48	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
115		simp-5l 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝜑)
116		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = 𝑒 → (𝑓 finSupp 0 ↔ 𝑒 finSupp 0))
117	116, 12	elrab2 3649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑒 ∈ 𝐹 ↔ (𝑒 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑒 finSupp 0))
118	117	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑒 ∈ 𝐹 → 𝑒 ∈ (ℤ ↑m Word 𝐴))
119	55, 48	elmapd 8846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑒 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑒:Word 𝐴⟶ℤ))
120	119	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑒 ∈ (ℤ ↑m Word 𝐴)) → 𝑒:Word 𝐴⟶ℤ)
121	118, 120	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
122	115, 121	sylancom 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
123	122	adantl3r 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ)
124	123	ffnd 6706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒 Fn Word 𝐴)
125	124	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑒 Fn Word 𝐴)
126	114	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ∈ V)
127		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 0 ∈ ℤ)
128		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
129	125, 126, 127, 128	fvdifsupp 8174	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑒‘𝑤) = 0)
130	129	oveq1d 7431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
131	72	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑀 ∈ Mnd)
132	75	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ⊆ Word 𝐵)
133	128	eldifad 3911	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐴)
134	132, 133	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐵)
135	131, 134, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑀 Σg 𝑤) ∈ 𝐵)
136	135, 81	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
137	130, 136	eqtrd 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
138	117	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 ∈ 𝐹 → 𝑒 finSupp 0)
139	138	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 finSupp 0)
140	139	fsuppimpd 9346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ∈ Fin)
141	86	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
142	123	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑒:Word 𝐴⟶ℤ)
143		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
144	142, 143	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑒‘𝑤) ∈ ℤ)
145	72	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
146	75	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝐵)
147	146	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
148	145, 147, 79	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
149	2, 11, 141, 144, 148	mulgcld 19245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
150		suppssdm 8180	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 supp 0) ⊆ dom 𝑒
151	123	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
152	150, 151	fssdm 6725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ⊆ Word 𝐴)
153	2, 41, 113, 114, 137, 140, 149, 152	gsummptres2 33525	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
154	153	adantllr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
155		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
156	155	mpteq1d 5195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
157	156	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
158		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (+g‘𝑅) = (+g‘𝑅)
159		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
160	159, 12	elrab2 3649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
161	160	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
162	161	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
163	162	fsuppimpd 9346	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
164	163	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ∈ Fin)
165		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ (𝑔 supp 0))
166	164, 165	ssfid 9246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
167	86	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑅 ∈ Grp)
168	151	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑒:Word 𝐴⟶ℤ)
169		suppssdm 8180	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 supp 0) ⊆ dom 𝑔
170		simp-7l 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝜑)
171		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔 ∈ 𝐹)
172	160	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝐹 → 𝑔 ∈ (ℤ ↑m Word 𝐴))
173	55, 48	elmapd 8846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
174	173	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑔 ∈ (ℤ ↑m Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
175	172, 174	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
176	170, 171, 175	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔:Word 𝐴⟶ℤ)
177	169, 176	fssdm 6725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ⊆ Word 𝐴)
178	165, 177	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ Word 𝐴)
179	178	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑤 ∈ Word 𝐴)
180	168, 179	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑒‘𝑤) ∈ ℤ)
181	179, 148	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑀 Σg 𝑤) ∈ 𝐵)
182	2, 11, 167, 180, 181	mulgcld 19245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))
184	183	eldifbd 3912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ¬ 𝑥 ∈ ℎ)
185	170, 86	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
186	183	eldifad 3911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ (𝑔 supp 0))
187	177, 186	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
188	151, 187	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
189	170, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑀 ∈ Mnd)
190	146, 187	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐵)
191	78	gsumwcl 18974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵) → (𝑀 Σg 𝑥) ∈ 𝐵)
192	189, 190, 191	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝐵)
193	2, 11, 185, 188, 192	mulgcld 19245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝐵)
194		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑒‘𝑤) = (𝑒‘𝑥))
195		oveq2 7424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑥))
196	194, 195	oveq12d 7434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑥) · (𝑀 Σg 𝑥)))
197	2, 158, 113, 166, 182, 183, 184, 193, 196	gsumunsn 20113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
198	197	adantllr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
199	154, 157, 198	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))))
200	105	ad8antlr 754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubGrp‘𝑅))
201	124	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 Fn Word 𝐴)
202		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
203	201, 187, 202	fmptunsnop 33204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
204	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
205	204	fveq1d 6883	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
206		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))
207		eqidd 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ 𝑦 = 𝑥) → 0 = 0)
208	201	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑒 Fn Word 𝐴)
209	114	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → Word 𝐴 ∈ V)
210		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 0 ∈ ℤ)
211		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 = 𝑤)
212		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
213	212	eldifad 3911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ Word 𝐴)
214	211, 213	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
215		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
216	212	eldifbd 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑤 ∈ ℎ)
217	211, 216	eqneltrd 2880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ ℎ)
218		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑥)
219	218	neqned 2962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ≠ 𝑥)
220		nelsn 4627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ≠ 𝑥 → ¬ 𝑦 ∈ {𝑥})
221	219, 220	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ {𝑥})
222		nelun 33020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (¬ 𝑦 ∈ (𝑒 supp 0) ↔ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})))
223	222	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑒 supp 0) = (ℎ ∪ {𝑥}) ∧ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})) → ¬ 𝑦 ∈ (𝑒 supp 0))
224	215, 217, 221, 223	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ (𝑒 supp 0))
225	214, 224	eldifd 3910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
226	208, 209, 210, 225	fvdifsupp 8174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ (Word 𝐴 ∖ ℎ))
229	228	eldifad 3911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ Word 𝐴)
230		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 0 ∈ ℤ)
231	206, 227, 229, 230	fvmptd2 6998	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = 0)
232	205, 231	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = 0)
233	232	oveq1d 7431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
234	229, 148	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑀 Σg 𝑤) ∈ 𝐵)
235	234, 81	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
236	233, 235	eqtrd 2795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
237	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
238	237	fveq1d 6883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
239		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
240	151	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
241		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
242	240, 241	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
245	244	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) ∈ ℤ)
246	238, 245	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) ∈ ℤ)
247	2, 11, 141, 246, 148	mulgcld 19245	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
248	2, 41, 113, 114, 236, 166, 247, 178	gsummptres2 33525	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
249	248	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
250	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
251	250	fveq1d 6883	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
252		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
253		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑤 ∈ ℎ)
254	252, 253	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 ∈ ℎ)
255	184	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑥 ∈ ℎ)
256		nelneq 2884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℎ ∧ ¬ 𝑥 ∈ ℎ) → ¬ 𝑦 = 𝑥)
257	254, 255, 256	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → (𝑒‘𝑦) = (𝑒‘𝑤))
260	258, 259	eqtrd 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑤))
261	206, 260, 179, 180	fvmptd2 6998	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (𝑒‘𝑤))
262	251, 261	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = (𝑒‘𝑤))
263	262	oveq1d 7431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))
264	263	mpteq2dva 5198	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
265	264	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))
266	265	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
267	249, 266	eqtrd 2795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))))
268		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 ∈ 𝐹)
269	268	resexd 6023	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∈ V)
270		snex 5404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {⟨𝑥, 0⟩} ∈ V
271	270	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → {⟨𝑥, 0⟩} ∈ V)
272	269, 271, 202	suppun2 33188	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)))
273	114, 202, 201	fdifsupp 33189	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ((𝑒 supp 0) ∖ {𝑥}))
274		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥}))
275	274	difeq1d 4073	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 supp 0) ∖ {𝑥}) = ((ℎ ∪ {𝑥}) ∖ {𝑥}))
276		disjsn 4672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ℎ)
277		undif5 4440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ℎ ∩ {𝑥}) = ∅ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
278	276, 277	sylbir 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ ℎ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
279	184, 278	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ)
280	273, 275, 279	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ℎ)
281		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑥 ∈ V
282		c0ex 11249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 ∈ V
283	281, 282	xpsn 7137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ({𝑥} × {0}) = {⟨𝑥, 0⟩}
284	283	oveq1i 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ({⟨𝑥, 0⟩} supp 0)
285		fczsupp0 8196	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑥} × {0}) supp 0) = ∅
286	284, 285	eqtr3i 2785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({⟨𝑥, 0⟩} supp 0) = ∅
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ({⟨𝑥, 0⟩} supp 0) = ∅)
288	280, 287	uneq12d 4116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)) = (ℎ ∪ ∅))
289		un0 4344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∪ ∅) = ℎ
290	289	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (ℎ ∪ ∅) = ℎ)
291	272, 288, 290	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
292	291	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ)
293		oveq1 7423	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0))
294	293	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓 supp 0) = ℎ ↔ (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ))
295		fveq1 6880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
296	295	oveq1d 7431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))
297	296	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))))
298	297	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
299	298	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
300	294, 299	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
301		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
302		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 finSupp 0 ↔ ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0))
303	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℤ ∈ V)
304	114	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V)
305	203	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
306		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
307		simp-10l 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝜑)
308		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒 ∈ 𝐹)
309	307, 308, 121	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
310		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
311	309, 310	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ)
314	305, 313	feq1dd 6688	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}):Word 𝐴⟶ℤ)
315	303, 304, 314	elmapdd 8847	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ (ℤ ↑m Word 𝐴))
316		0zd 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ)
317	314	ffund 6710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Fun ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
318	166	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin)
319	292, 318	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) ∈ Fin)
320	315, 316, 317, 319	isfsuppd 9343	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0)
321	302, 315, 320	elrabd 3647	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
322	321, 12	eleqtrrdi 2871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ 𝐹)
323	300, 301, 322	rspcdva 3577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
324	292, 323	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
325	267, 324	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
326	86	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp)
327	10	subrgsubm 20776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubMnd‘𝑀))
328	327	ad8antlr 754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubMnd‘𝑀))
329		sswrd 14612	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ⊆ 𝑡 → Word 𝐴 ⊆ Word 𝑡)
330	329	ad7antlr 752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝑡)
331	187	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
332	330, 331	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝑡)
333		gsumwsubmcl 18972	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ (SubMnd‘𝑀) ∧ 𝑥 ∈ Word 𝑡) → (𝑀 Σg 𝑥) ∈ 𝑡)
334	328, 332, 333	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝑡)
335	123	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
336	335, 331	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ)
337	2, 11, 326, 334, 200, 336	subgmulgcld 33515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝑡)
338	158, 200, 325, 337	subgcld 19286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))) ∈ 𝑡)
339	199, 338	eqeltrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
340	339	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
341	340	ralrimiva 3154	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
342	341	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
343	342	anasss 472	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
344		oveq1 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑒 supp 0) = (𝑓 supp 0))
345	344	eqeq1d 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥})))
346		fveq1 6880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑓 → (𝑒‘𝑤) = (𝑓‘𝑤))
347	346	oveq1d 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑓 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))
348	347	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑓 → (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))))
349	348	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑓 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))))
350	349	eleq1d 2845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑓 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
351	345, 350	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑓 → (((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
352	351	cbvralvw 3240	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
353	343, 352	imbitrdi 254	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
354	31, 34, 37, 40, 112, 353, 163	findcard2d 9168	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
355		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ 𝐹)
356	28, 354, 355	rspcdva 3577	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
357	20, 356	mpd 16	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
358	357	ad4ant13 764	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
359	19, 358	eqeltrd 2860	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 ∈ 𝑡)
360		eqid 2760	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
361	13	eleq2i 2852	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝑆 ↔ 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
362	361	bilani 510	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
363	360, 362	elrnmpt2d 5952	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
364	359, 363	r19.29a 3170	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑡)
365	364	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → (𝑠 ∈ 𝑆 → 𝑠 ∈ 𝑡))
366	365	ssrdv 3937	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → 𝑆 ⊆ 𝑡)
367	366	ex 418	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
368	367	ralrimiva 3154	. . . 4 ⊢ (𝜑 → ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
369		ssintrab 4931	. . . 4 ⊢ (𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ↔ ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡))
370	368, 369	sylibr 237	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
371	18, 370	eqssd 3948	. 2 ⊢ (𝜑 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} = 𝑆)
372	8, 371	eqtrd 2795	1 ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  {crab 3412  Vcvv 3450   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  ifcif 4482  {csn 4584  ⟨cop 4590  ∩ cint 4907   class class class wbr 5103   ↦ cmpt 5186   × cxp 5653  ran crn 5656   ↾ cres 5657   Fn wfn 6530  ⟶wf 6531  ‘cfv 6535  (class class class)co 7416   supp csupp 8163   ↑_m cmap 8833  Fincfn 8959   finSupp cfsupp 9338  0cc0 11149  ℤcz 12640  Word cword 14603  Basecbs 17326  +_gcplusg 17367  0_gc0g 17549   Σ_g cgsu 17550  Mndcmnd 18862  SubMndcsubmnd 18916  Grpcgrp 19083  ._gcmg 19216  SubGrpcsubg 19269  CMndccmn 19933  mulGrpcmgp 20299  Ringcrg 20398  SubRingcsubrg 20760  RingSpancrgspn 20801

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742  ax-inf2 9627  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  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 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6301  df-ord 6362  df-on 6363  df-lim 6364  df-suc 6365  df-iota 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7684  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8164  df-tpos 8229  df-frecs 8285  df-wrecs 8316  df-recs 8365  df-rdg 8404  df-1o 8462  df-2o 8463  df-er 8703  df-map 8835  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fsupp 9339  df-sup 9419  df-oi 9489  df-card 9969  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11492  df-neg 11493  df-div 11921  df-nn 12283  df-2 12352  df-3 12353  df-4 12354  df-5 12355  df-6 12356  df-7 12357  df-8 12358  df-9 12359  df-n0 12554  df-z 12641  df-dec 12762  df-uz 12913  df-rp 13068  df-fz 13587  df-fzo 13735  df-seq 14091  df-exp 14151  df-hash 14420  df-word 14604  df-concat 14661  df-s1 14688  df-substr 14734  df-pfx 14766  df-cj 15211  df-re 15212  df-im 15213  df-sqrt 15347  df-abs 15348  df-clim 15600  df-sum 15799  df-struct 17264  df-sets 17281  df-slot 17299  df-ndx 17311  df-base 17327  df-ress 17348  df-plusg 17380  df-mulr 17381  df-starv 17382  df-tset 17386  df-ple 17387  df-ds 17389  df-unif 17390  df-0g 17551  df-gsum 17552  df-mre 17695  df-mrc 17696  df-acs 17698  df-mgm 18755  df-sgrp 18847  df-mnd 18863  df-mhm 18917  df-submnd 18918  df-grp 19086  df-minusg 19087  df-mulg 19217  df-subg 19272  df-ghm 19367  df-cntz 19470  df-cmn 19935  df-abl 19936  df-mgp 20300  df-rng 20314  df-ur 20347  df-ring 20400  df-cring 20401  df-oppr 20506  df-subrng 20737  df-subrg 20761  df-rgspn 20802  df-cnfld 21618  df-zring 21692

This theorem is used by:  elrgspn  33718