Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elrgspnlem4 Structured version   Visualization version   GIF version

Theorem elrgspnlem4 33234
Description: Lemma for elrgspn 33235. (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.
StepHypRef Expression
1 elrgspn.r . . 3 (𝜑𝑅 ∈ Ring)
2 elrgspn.b . . . 4 𝐵 = (Base‘𝑅)
32a1i 11 . . 3 (𝜑𝐵 = (Base‘𝑅))
4 elrgspn.a . . 3 (𝜑𝐴𝐵)
5 elrgspn.n . . . 4 𝑁 = (RingSpan‘𝑅)
65a1i 11 . . 3 (𝜑𝑁 = (RingSpan‘𝑅))
7 eqidd 2735 . . 3 (𝜑 → (𝑁𝐴) = (𝑁𝐴))
81, 3, 4, 6, 7rgspnval 20628 . 2 (𝜑 → (𝑁𝐴) = {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡})
9 sseq2 4021 . . . . 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 𝑤)))))
142, 10, 11, 5, 12, 1, 4, 13elrgspnlem2 33232 . . . . 5 (𝜑𝑆 ∈ (SubRing‘𝑅))
152, 10, 11, 5, 12, 1, 4, 13elrgspnlem3 33233 . . . . 5 (𝜑𝐴𝑆)
169, 14, 15elrabd 3696 . . . 4 (𝜑𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡})
17 intss1 4967 . . . 4 (𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡} → {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡} ⊆ 𝑆)
1816, 17syl 17 . . 3 (𝜑 {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡} ⊆ 𝑆)
19 simpr 484 . . . . . . . . . 10 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑠𝑆) ∧ 𝑔𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
20 eqidd 2735 . . . . . . . . . . . 12 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → (𝑔 supp 0) = (𝑔 supp 0))
21 oveq1 7437 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓 supp 0) = (𝑔 supp 0))
2221eqeq1d 2736 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑓 supp 0) = (𝑔 supp 0) ↔ (𝑔 supp 0) = (𝑔 supp 0)))
23 fveq1 6905 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑔 → (𝑓𝑤) = (𝑔𝑤))
2423oveq1d 7445 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → ((𝑓𝑤) · (𝑀 Σg 𝑤)) = ((𝑔𝑤) · (𝑀 Σg 𝑤)))
2524mpteq2dv 5249 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))
2625oveq2d 7446 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
2726eleq1d 2823 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
2822, 27imbi12d 344 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
29 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑖 = ∅ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ∅))
3029imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = ∅ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
3130ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = ∅ → (∀𝑓𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
32 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑖 = → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ))
3332imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
3433ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = → (∀𝑓𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
35 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑖 = ( ∪ {𝑥}) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ( ∪ {𝑥})))
3635imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = ( ∪ {𝑥}) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
3736ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = ( ∪ {𝑥}) → (∀𝑓𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓𝐹 ((𝑓 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
38 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑔 supp 0) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (𝑔 supp 0)))
3938imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = (𝑔 supp 0) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
4039ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = (𝑔 supp 0) → (∀𝑓𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
41 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (0g𝑅) = (0g𝑅)
421ringcmnd 20297 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 ∈ CMnd)
4342ad5antr 734 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → 𝑅 ∈ CMnd)
442fvexi 6920 . . . . . . . . . . . . . . . . . . . . . . 23 𝐵 ∈ V
4544a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ V)
4645, 4ssexd 5329 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ V)
47 wrdexg 14558 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ V → Word 𝐴 ∈ V)
4846, 47syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → Word 𝐴 ∈ V)
4948ad5antr 734 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → Word 𝐴 ∈ V)
50 simp-4l 783 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) → 𝜑)
5112reqabi 3456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝐹 ↔ (𝑓 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑓 finSupp 0))
5251simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝐹𝑓 ∈ (ℤ ↑m Word 𝐴))
5352adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) → 𝑓 ∈ (ℤ ↑m Word 𝐴))
54 zex 12619 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℤ ∈ V
5554a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ℤ ∈ V)
5655, 48elmapd 8878 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑓 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑓:Word 𝐴⟶ℤ))
5756biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (ℤ ↑m Word 𝐴)) → 𝑓:Word 𝐴⟶ℤ)
5850, 53, 57syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) → 𝑓:Word 𝐴⟶ℤ)
5958ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) → 𝑓 Fn Word 𝐴)
6059ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑓 Fn Word 𝐴)
6149adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ∈ V)
62 0zd 12622 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 0 ∈ ℤ)
63 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ ∅))
6463eldifad 3974 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐴)
6563eldifbd 3975 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ ∅)
66 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓 supp 0) = ∅)
6765, 66neleqtrrd 2861 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ (𝑓 supp 0))
6864, 67eldifd 3973 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ (𝑓 supp 0)))
6960, 61, 62, 68fvdifsupp 8194 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓𝑤) = 0)
7069oveq1d 7445 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
7110ringmgp 20256 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
721, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ Mnd)
7372ad6antr 736 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑀 ∈ Mnd)
74 sswrd 14556 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵)
754, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → Word 𝐴 ⊆ Word 𝐵)
7675ad6antr 736 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ⊆ Word 𝐵)
7776, 64sseldd 3995 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐵)
7810, 2mgpbas 20157 . . . . . . . . . . . . . . . . . . . . . . 23 𝐵 = (Base‘𝑀)
7978gsumwcl 18864 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
8073, 77, 79syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑀 Σg 𝑤) ∈ 𝐵)
812, 41, 11mulg0 19104 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
8280, 81syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
8370, 82eqtrd 2774 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓𝑤) · (𝑀 Σg 𝑤)) = (0g𝑅))
84 0fi 9080 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ Fin
8584a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ∈ Fin)
861ringgrpd 20259 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑅 ∈ Grp)
8786ad6antr 736 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
8858ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑓:Word 𝐴⟶ℤ)
89 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
9088, 89ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑓𝑤) ∈ ℤ)
9172ad6antr 736 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
9275ad6antr 736 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
9392, 89sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
9491, 93, 79syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
952, 11, 87, 90, 94mulgcld 19126 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → ((𝑓𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
96 0ss 4405 . . . . . . . . . . . . . . . . . . . 20 ∅ ⊆ Word 𝐴
9796a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ⊆ Word 𝐴)
982, 41, 43, 49, 83, 85, 95, 97gsummptres2 33038 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))))
99 mpt0 6710 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ∅ ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤))) = ∅
10099a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑤 ∈ ∅ ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤))) = ∅)
101100oveq2d 7446 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg ∅))
10241gsum0 18709 . . . . . . . . . . . . . . . . . . 19 (𝑅 Σg ∅) = (0g𝑅)
103102a1i 11 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg ∅) = (0g𝑅))
10498, 101, 1033eqtrd 2778 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) = (0g𝑅))
105 subrgsubg 20593 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubGrp‘𝑅))
10641subg0cl 19164 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (SubGrp‘𝑅) → (0g𝑅) ∈ 𝑡)
107105, 106syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (SubRing‘𝑅) → (0g𝑅) ∈ 𝑡)
108107adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (SubRing‘𝑅)) → (0g𝑅) ∈ 𝑡)
109108ad4antr 732 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (0g𝑅) ∈ 𝑡)
110104, 109eqeltrd 2838 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
111110ex 412 . . . . . . . . . . . . . . 15 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ 𝑓𝐹) → ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
112111ralrimiva 3143 . . . . . . . . . . . . . 14 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → ∀𝑓𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
11342ad7antr 738 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑅 ∈ CMnd)
11448ad7antr 738 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → Word 𝐴 ∈ V)
115 simp-5l 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) → 𝜑)
116 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = 𝑒 → (𝑓 finSupp 0 ↔ 𝑒 finSupp 0))
117116, 12elrab2 3697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑒𝐹 ↔ (𝑒 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑒 finSupp 0))
118117simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑒𝐹𝑒 ∈ (ℤ ↑m Word 𝐴))
11955, 48elmapd 8878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑒 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑒:Word 𝐴⟶ℤ))
120119biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑒 ∈ (ℤ ↑m Word 𝐴)) → 𝑒:Word 𝐴⟶ℤ)
121118, 120sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑒𝐹) → 𝑒:Word 𝐴⟶ℤ)
122115, 121sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) → 𝑒:Word 𝐴⟶ℤ)
123122adantl3r 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) → 𝑒:Word 𝐴⟶ℤ)
124123ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) → 𝑒 Fn Word 𝐴)
125124ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑒 Fn Word 𝐴)
126114adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ∈ V)
127 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 0 ∈ ℤ)
128 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
129125, 126, 127, 128fvdifsupp 8194 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑒𝑤) = 0)
130129oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
13172ad8antr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑀 ∈ Mnd)
13275ad8antr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ⊆ Word 𝐵)
133128eldifad 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐴)
134132, 133sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐵)
135131, 134, 79syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑀 Σg 𝑤) ∈ 𝐵)
136135, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
137130, 136eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒𝑤) · (𝑀 Σg 𝑤)) = (0g𝑅))
138117simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑒𝐹𝑒 finSupp 0)
139138ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑒 finSupp 0)
140139fsuppimpd 9406 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒 supp 0) ∈ Fin)
14186ad8antr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
142123ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑒:Word 𝐴⟶ℤ)
143 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
144142, 143ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑒𝑤) ∈ ℤ)
14572ad8antr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
14675ad7antr 738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝐵)
147146sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
148145, 147, 79syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
1492, 11, 141, 144, 148mulgcld 19126 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑒𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
150 suppssdm 8200 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 supp 0) ⊆ dom 𝑒
151123adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
152150, 151fssdm 6755 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒 supp 0) ⊆ Word 𝐴)
1532, 41, 113, 114, 137, 140, 149, 152gsummptres2 33038 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))))
154153adantllr 719 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))))
155 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒 supp 0) = ( ∪ {𝑥}))
156155mpteq1d 5242 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ( ∪ {𝑥}) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))
157156oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ( ∪ {𝑥}) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))))
158 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . 23 (+g𝑅) = (+g𝑅)
159 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
160159, 12elrab2 3697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
161160simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔𝐹𝑔 finSupp 0)
162161adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → 𝑔 finSupp 0)
163162fsuppimpd 9406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → (𝑔 supp 0) ∈ Fin)
164163ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑔 supp 0) ∈ Fin)
165 simp-4r 784 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ⊆ (𝑔 supp 0))
166164, 165ssfid 9298 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ∈ Fin)
16786ad8antr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → 𝑅 ∈ Grp)
168151adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → 𝑒:Word 𝐴⟶ℤ)
169 suppssdm 8200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔 supp 0) ⊆ dom 𝑔
170 simp-7l 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝜑)
171 simp-5r 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑔𝐹)
172160simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔𝐹𝑔 ∈ (ℤ ↑m Word 𝐴))
17355, 48elmapd 8878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
174173biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑔 ∈ (ℤ ↑m Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
175172, 174sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑔𝐹) → 𝑔:Word 𝐴⟶ℤ)
176170, 171, 175syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑔:Word 𝐴⟶ℤ)
177169, 176fssdm 6755 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑔 supp 0) ⊆ Word 𝐴)
178165, 177sstrd 4005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ⊆ Word 𝐴)
179178sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → 𝑤 ∈ Word 𝐴)
180168, 179ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → (𝑒𝑤) ∈ ℤ)
181179, 148syldan 591 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → (𝑀 Σg 𝑤) ∈ 𝐵)
1822, 11, 167, 180, 181mulgcld 19126 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → ((𝑒𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑥 ∈ ((𝑔 supp 0) ∖ ))
184183eldifbd 3975 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ¬ 𝑥)
185170, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑅 ∈ Grp)
186183eldifad 3974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑥 ∈ (𝑔 supp 0))
187177, 186sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
188151, 187ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒𝑥) ∈ ℤ)
189170, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑀 ∈ Mnd)
190146, 187sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑥 ∈ Word 𝐵)
19178gsumwcl 18864 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵) → (𝑀 Σg 𝑥) ∈ 𝐵)
192189, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝐵)
1932, 11, 185, 188, 192mulgcld 19126 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒𝑥) · (𝑀 Σg 𝑥)) ∈ 𝐵)
194 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑒𝑤) = (𝑒𝑥))
195 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑥))
196194, 195oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑥 → ((𝑒𝑤) · (𝑀 Σg 𝑤)) = ((𝑒𝑥) · (𝑀 Σg 𝑥)))
1972, 158, 113, 166, 182, 183, 184, 193, 196gsumunsn 19992 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ( ∪ {𝑥}) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))(+g𝑅)((𝑒𝑥) · (𝑀 Σg 𝑥))))
198197adantllr 719 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ( ∪ {𝑥}) ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))(+g𝑅)((𝑒𝑥) · (𝑀 Σg 𝑥))))
199154, 157, 1983eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))(+g𝑅)((𝑒𝑥) · (𝑀 Σg 𝑥))))
200105ad8antlr 741 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑡 ∈ (SubGrp‘𝑅))
201124adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑒 Fn Word 𝐴)
202 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 0 ∈ ℤ)
203201, 187, 202fmptunsnop 32714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
204203adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
205204fveq1d 6908 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
206 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))) = (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))
207 eqidd 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ 𝑦 = 𝑥) → 0 = 0)
208201ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑒 Fn Word 𝐴)
209114ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → Word 𝐴 ∈ V)
210 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 0 ∈ ℤ)
211 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 = 𝑤)
212 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ (Word 𝐴))
213212eldifad 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ Word 𝐴)
214211, 213eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
215 simp-4r 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒 supp 0) = ( ∪ {𝑥}))
216212eldifbd 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑤)
217211, 216eqneltrd 2858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦)
218 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑥)
219218neqned 2944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦𝑥)
220 nelsn 4670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦𝑥 → ¬ 𝑦 ∈ {𝑥})
221219, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ {𝑥})
222 nelun 32540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑒 supp 0) = ( ∪ {𝑥}) → (¬ 𝑦 ∈ (𝑒 supp 0) ↔ (¬ 𝑦 ∧ ¬ 𝑦 ∈ {𝑥})))
223222biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑒 supp 0) = ( ∪ {𝑥}) ∧ (¬ 𝑦 ∧ ¬ 𝑦 ∈ {𝑥})) → ¬ 𝑦 ∈ (𝑒 supp 0))
224215, 217, 221, 223syl12anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ (𝑒 supp 0))
225214, 224eldifd 3973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (Word 𝐴 ∖ (𝑒 supp 0)))
226208, 209, 210, 225fvdifsupp 8194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒𝑦) = 0)
227207, 226ifeqda 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒𝑦)) = 0)
228 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → 𝑤 ∈ (Word 𝐴))
229228eldifad 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → 𝑤 ∈ Word 𝐴)
230 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → 0 ∈ ℤ)
231206, 227, 229, 230fvmptd2 7023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))‘𝑤) = 0)
232205, 231eqtr3d 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = 0)
233232oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
234229, 148syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → (𝑀 Σg 𝑤) ∈ 𝐵)
235234, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
236233, 235eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = (0g𝑅))
237203adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
238237fveq1d 6908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
239 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
240151ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
241 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
242240, 241ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒𝑦) ∈ ℤ)
243239, 242ifclda 4565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒𝑦)) ∈ ℤ)
244243fmpttd 7134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))):Word 𝐴⟶ℤ)
245244ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))‘𝑤) ∈ ℤ)
246238, 245eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) ∈ ℤ)
2472, 11, 141, 246, 148mulgcld 19126 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
2482, 41, 113, 114, 236, 166, 247, 178gsummptres2 33038 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
249248adantllr 719 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
250203adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
251250fveq1d 6908 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
252 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
253 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → 𝑤)
254252, 253eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → 𝑦)
255184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → ¬ 𝑥)
256 nelneq 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦 ∧ ¬ 𝑥) → ¬ 𝑦 = 𝑥)
257254, 255, 256syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → ¬ 𝑦 = 𝑥)
258257iffalsed 4541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒𝑦)) = (𝑒𝑦))
259252fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → (𝑒𝑦) = (𝑒𝑤))
260258, 259eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒𝑦)) = (𝑒𝑤))
261206, 260, 179, 180fvmptd2 7023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦)))‘𝑤) = (𝑒𝑤))
262251, 261eqtr3d 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) = (𝑒𝑤))
263262oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑤) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒𝑤) · (𝑀 Σg 𝑤)))
264263mpteq2dva 5247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑤 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))
265264adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑤 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))
266265oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))))
267249, 266eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))))
268 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑒𝐹)
269268resexd 6047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∈ V)
270 snex 5441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {⟨𝑥, 0⟩} ∈ V
271270a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → {⟨𝑥, 0⟩} ∈ V)
272269, 271, 202suppun2 32698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)))
273114, 202, 201fdifsupp 32699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ((𝑒 supp 0) ∖ {𝑥}))
274 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒 supp 0) = ( ∪ {𝑥}))
275274difeq1d 4134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 supp 0) ∖ {𝑥}) = (( ∪ {𝑥}) ∖ {𝑥}))
276 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (( ∩ {𝑥}) = ∅ ↔ ¬ 𝑥)
277 undif5 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (( ∩ {𝑥}) = ∅ → (( ∪ {𝑥}) ∖ {𝑥}) = )
278276, 277sylbir 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 → (( ∪ {𝑥}) ∖ {𝑥}) = )
279184, 278syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (( ∪ {𝑥}) ∖ {𝑥}) = )
280273, 275, 2793eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = )
281 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑥 ∈ V
282 c0ex 11252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 ∈ V
283281, 282xpsn 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({𝑥} × {0}) = {⟨𝑥, 0⟩}
284283oveq1i 7440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({𝑥} × {0}) supp 0) = ({⟨𝑥, 0⟩} supp 0)
285 fczsupp0 8216 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({𝑥} × {0}) supp 0) = ∅
286284, 285eqtr3i 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({⟨𝑥, 0⟩} supp 0) = ∅
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ({⟨𝑥, 0⟩} supp 0) = ∅)
288280, 287uneq12d 4178 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({⟨𝑥, 0⟩} supp 0)) = ( ∪ ∅))
289 un0 4399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( ∪ ∅) =
290289a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ( ∪ ∅) = )
291272, 288, 2903eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = )
292291adantllr 719 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = )
293 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0))
294293eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓 supp 0) = ↔ (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = ))
295 fveq1 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤))
296295oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑓𝑤) · (𝑀 Σg 𝑤)) = ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))
297296mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤))))
298297oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))))
299298eleq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
300294, 299imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
301 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
302 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) → (𝑓 finSupp 0 ↔ ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0))
30354a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ℤ ∈ V)
304114adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → Word 𝐴 ∈ V)
305203adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
306 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ)
307 simp-10l 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝜑)
308 simp-4r 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒𝐹)
309307, 308, 121syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ)
310 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴)
311309, 310ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒𝑦) ∈ ℤ)
312306, 311ifclda 4565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒𝑦)) ∈ ℤ)
313312fmpttd 7134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒𝑦))):Word 𝐴⟶ℤ)
314305, 313feq1dd 6721 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}):Word 𝐴⟶ℤ)
315303, 304, 314elmapdd 8879 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ (ℤ ↑m Word 𝐴))
316 0zd 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 0 ∈ ℤ)
317314ffund 6740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → Fun ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}))
318166adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ∈ Fin)
319292, 318eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) ∈ Fin)
320315, 316, 317, 319isfsuppd 9403 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) finSupp 0)
321302, 315, 320elrabd 3696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
322321, 12eleqtrrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) ∈ 𝐹)
323300, 301, 322rspcdva 3622 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩}) supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
324292, 323mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {⟨𝑥, 0⟩})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
325267, 324eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
32686ad8antr 740 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑅 ∈ Grp)
32710subrgsubm 20601 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubMnd‘𝑀))
328327ad8antlr 741 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑡 ∈ (SubMnd‘𝑀))
329 sswrd 14556 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑡 → Word 𝐴 ⊆ Word 𝑡)
330329ad7antlr 739 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝑡)
331187adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑥 ∈ Word 𝐴)
332330, 331sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑥 ∈ Word 𝑡)
333 gsumwsubmcl 18862 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (SubMnd‘𝑀) ∧ 𝑥 ∈ Word 𝑡) → (𝑀 Σg 𝑥) ∈ 𝑡)
334328, 332, 333syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝑡)
335123ad4ant13 751 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ)
336335, 331ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑒𝑥) ∈ ℤ)
3372, 11, 326, 334, 200, 336subgmulgcld 33030 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑒𝑥) · (𝑀 Σg 𝑥)) ∈ 𝑡)
338158, 200, 325, 337subgcld 33028 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → ((𝑅 Σg (𝑤 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))))(+g𝑅)((𝑒𝑥) · (𝑀 Σg 𝑥))) ∈ 𝑡)
339199, 338eqeltrd 2838 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) ∧ (𝑒 supp 0) = ( ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
340339ex 412 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒𝐹) → ((𝑒 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
341340ralrimiva 3143 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) ∧ ∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) → ∀𝑒𝐹 ((𝑒 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
342341ex 412 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ )) → (∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒𝐹 ((𝑒 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
343342anasss 466 . . . . . . . . . . . . . . 15 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ( ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ))) → (∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒𝐹 ((𝑒 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
344 oveq1 7437 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑓 → (𝑒 supp 0) = (𝑓 supp 0))
345344eqeq1d 2736 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑓 → ((𝑒 supp 0) = ( ∪ {𝑥}) ↔ (𝑓 supp 0) = ( ∪ {𝑥})))
346 fveq1 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑓 → (𝑒𝑤) = (𝑓𝑤))
347346oveq1d 7445 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑓 → ((𝑒𝑤) · (𝑀 Σg 𝑤)) = ((𝑓𝑤) · (𝑀 Σg 𝑤)))
348347mpteq2dv 5249 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑓 → (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤))))
349348oveq2d 7446 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑓 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))))
350349eleq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑓 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
351345, 350imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑓 → (((𝑒 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
352351cbvralvw 3234 . . . . . . . . . . . . . . 15 (∀𝑒𝐹 ((𝑒 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓𝐹 ((𝑓 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
353343, 352imbitrdi 251 . . . . . . . . . . . . . 14 (((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) ∧ ( ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ))) → (∀𝑓𝐹 ((𝑓 supp 0) = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑓𝐹 ((𝑓 supp 0) = ( ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)))
35431, 34, 37, 40, 112, 353, 163findcard2d 9204 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → ∀𝑓𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
355 simpr 484 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → 𝑔𝐹)
35628, 354, 355rspcdva 3622 . . . . . . . . . . . 12 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))
35720, 356mpd 15 . . . . . . . . . . 11 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑔𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
358357ad4ant13 751 . . . . . . . . . 10 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑠𝑆) ∧ 𝑔𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)
35919, 358eqeltrd 2838 . . . . . . . . 9 ((((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑠𝑆) ∧ 𝑔𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) → 𝑠𝑡)
360 eqid 2734 . . . . . . . . . 10 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
36113eleq2i 2830 . . . . . . . . . . . 12 (𝑠𝑆𝑠 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
362361biimpi 216 . . . . . . . . . . 11 (𝑠𝑆𝑠 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
363362adantl 481 . . . . . . . . . 10 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑠𝑆) → 𝑠 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
364360, 363elrnmpt2d 5979 . . . . . . . . 9 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑠𝑆) → ∃𝑔𝐹 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
365359, 364r19.29a 3159 . . . . . . . 8 ((((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) ∧ 𝑠𝑆) → 𝑠𝑡)
366365ex 412 . . . . . . 7 (((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) → (𝑠𝑆𝑠𝑡))
367366ssrdv 4000 . . . . . 6 (((𝜑𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴𝑡) → 𝑆𝑡)
368367ex 412 . . . . 5 ((𝜑𝑡 ∈ (SubRing‘𝑅)) → (𝐴𝑡𝑆𝑡))
369368ralrimiva 3143 . . . 4 (𝜑 → ∀𝑡 ∈ (SubRing‘𝑅)(𝐴𝑡𝑆𝑡))
370 ssintrab 4975 . . . 4 (𝑆 {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡} ↔ ∀𝑡 ∈ (SubRing‘𝑅)(𝐴𝑡𝑆𝑡))
371369, 370sylibr 234 . . 3 (𝜑𝑆 {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡})
37218, 371eqssd 4012 . 2 (𝜑 {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴𝑡} = 𝑆)
3738, 372eqtrd 2774 1 (𝜑 → (𝑁𝐴) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1536  wcel 2105  wne 2937  wral 3058  {crab 3432  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  ifcif 4530  {csn 4630  cop 4636   cint 4950   class class class wbr 5147  cmpt 5230   × cxp 5686  ran crn 5689  cres 5690   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430   supp csupp 8183  m cmap 8864  Fincfn 8983   finSupp cfsupp 9398  0cc0 11152  cz 12610  Word cword 14548  Basecbs 17244  +gcplusg 17297  0gc0g 17485   Σg cgsu 17486  Mndcmnd 18759  SubMndcsubmnd 18807  Grpcgrp 18963  .gcmg 19097  SubGrpcsubg 19150  CMndccmn 19812  mulGrpcmgp 20151  Ringcrg 20250  SubRingcsubrg 20585  RingSpancrgspn 20626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-tpos 8249  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-word 14549  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-0g 17487  df-gsum 17488  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18966  df-minusg 18967  df-mulg 19098  df-subg 19153  df-ghm 19243  df-cntz 19347  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-cring 20253  df-oppr 20350  df-subrng 20562  df-subrg 20586  df-rgspn 20627  df-cnfld 21382  df-zring 21475
This theorem is referenced by:  elrgspn  33235
  Copyright terms: Public domain W3C validator