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

Theorem elrgspnlem2 33247
Description: Lemma for elrgspn 33250. (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
elrgspnlem2 (𝜑𝑆 ∈ (SubRing‘𝑅))
Distinct variable groups:   · ,𝑓,𝑔,𝑤   𝐴,𝑓,𝑔,𝑤   𝐵,𝑓,𝑔,𝑤   𝑓,𝐹,𝑔,𝑤   𝑓,𝑀,𝑔,𝑤   𝑅,𝑓,𝑔,𝑤   𝑆,𝑔,𝑤   𝜑,𝑓,𝑔,𝑤
Allowed substitution hints:   𝑆(𝑓)   𝑁(𝑤,𝑓,𝑔)

Proof of Theorem elrgspnlem2
Dummy variables 𝑎 𝑖 𝑗 𝑡 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elrgspn.r . 2 (𝜑𝑅 ∈ Ring)
2 elrgspn.b . . 3 𝐵 = (Base‘𝑅)
3 elrgspn.m . . 3 𝑀 = (mulGrp‘𝑅)
4 elrgspn.x . . 3 · = (.g𝑅)
5 elrgspn.n . . 3 𝑁 = (RingSpan‘𝑅)
6 elrgspn.f . . 3 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
7 elrgspn.a . . 3 (𝜑𝐴𝐵)
8 elrgspnlem1.1 . . 3 𝑆 = ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
92, 3, 4, 5, 6, 1, 7, 8elrgspnlem1 33246 . 2 (𝜑𝑆 ∈ (SubGrp‘𝑅))
10 eqeq2 2749 . . . . . . 7 ((1r𝑅) = if(𝑤 = ∅, (1r𝑅), (0g𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r𝑅), (0g𝑅))))
11 eqeq2 2749 . . . . . . 7 ((0g𝑅) = if(𝑤 = ∅, (1r𝑅), (0g𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r𝑅), (0g𝑅))))
12 simpr 484 . . . . . . . . . . 11 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → 𝑤 = ∅)
1312fveq2d 6910 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅))
14 eqid 2737 . . . . . . . . . . . 12 (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))
15 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑣 = ∅) → 𝑣 = ∅)
1615iftrued 4533 . . . . . . . . . . . 12 ((𝜑𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1)
17 wrd0 14577 . . . . . . . . . . . . 13 ∅ ∈ Word 𝐴
1817a1i 11 . . . . . . . . . . . 12 (𝜑 → ∅ ∈ Word 𝐴)
19 1zzd 12648 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
2014, 16, 18, 19fvmptd2 7024 . . . . . . . . . . 11 (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
2120ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
2213, 21eqtrd 2777 . . . . . . . . 9 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1)
2312oveq2d 7447 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg ∅))
24 eqid 2737 . . . . . . . . . . . 12 (1r𝑅) = (1r𝑅)
253, 24ringidval 20180 . . . . . . . . . . 11 (1r𝑅) = (0g𝑀)
2625gsum0 18697 . . . . . . . . . 10 (𝑀 Σg ∅) = (1r𝑅)
2723, 26eqtrdi 2793 . . . . . . . . 9 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r𝑅))
2822, 27oveq12d 7449 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · (1r𝑅)))
292, 24ringidcl 20262 . . . . . . . . . . 11 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
301, 29syl 17 . . . . . . . . . 10 (𝜑 → (1r𝑅) ∈ 𝐵)
312, 4mulg1 19099 . . . . . . . . . 10 ((1r𝑅) ∈ 𝐵 → (1 · (1r𝑅)) = (1r𝑅))
3230, 31syl 17 . . . . . . . . 9 (𝜑 → (1 · (1r𝑅)) = (1r𝑅))
3332ad2antrr 726 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (1 · (1r𝑅)) = (1r𝑅))
3428, 33eqtrd 2777 . . . . . . 7 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r𝑅))
35 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅))
3635notbid 318 . . . . . . . . . . . . 13 (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅))
3736biimparc 479 . . . . . . . . . . . 12 ((¬ 𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
3837adantll 714 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
3938iffalsed 4536 . . . . . . . . . 10 ((((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0)
40 simplr 769 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴)
41 0zd 12625 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈ ℤ)
4214, 39, 40, 41fvmptd2 7024 . . . . . . . . 9 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0)
4342oveq1d 7446 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
443ringmgp 20236 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
451, 44syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ Mnd)
46 sswrd 14560 . . . . . . . . . . . . 13 (𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵)
477, 46syl 17 . . . . . . . . . . . 12 (𝜑 → Word 𝐴 ⊆ Word 𝐵)
4847sselda 3983 . . . . . . . . . . 11 ((𝜑𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
493, 2mgpbas 20142 . . . . . . . . . . . 12 𝐵 = (Base‘𝑀)
5049gsumwcl 18852 . . . . . . . . . . 11 ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
5145, 48, 50syl2an2r 685 . . . . . . . . . 10 ((𝜑𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
52 eqid 2737 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
532, 52, 4mulg0 19092 . . . . . . . . . 10 ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
5451, 53syl 17 . . . . . . . . 9 ((𝜑𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
5554adantr 480 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
5643, 55eqtrd 2777 . . . . . . 7 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g𝑅))
5710, 11, 34, 56ifbothda 4564 . . . . . 6 ((𝜑𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r𝑅), (0g𝑅)))
5857mpteq2dva 5242 . . . . 5 (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅))))
5958oveq2d 7447 . . . 4 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅)))))
601ringcmnd 20281 . . . . . 6 (𝜑𝑅 ∈ CMnd)
6160cmnmndd 19822 . . . . 5 (𝜑𝑅 ∈ Mnd)
622fvexi 6920 . . . . . . . 8 𝐵 ∈ V
6362a1i 11 . . . . . . 7 (𝜑𝐵 ∈ V)
6463, 7ssexd 5324 . . . . . 6 (𝜑𝐴 ∈ V)
65 wrdexg 14562 . . . . . 6 (𝐴 ∈ V → Word 𝐴 ∈ V)
6664, 65syl 17 . . . . 5 (𝜑 → Word 𝐴 ∈ V)
67 eqid 2737 . . . . 5 (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅)))
6830, 2eleqtrdi 2851 . . . . 5 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
6952, 61, 66, 18, 67, 68gsummptif1n0 19984 . . . 4 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅)))) = (1r𝑅))
7059, 69eqtrd 2777 . . 3 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (1r𝑅))
71 eqid 2737 . . . . 5 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
72 fveq1 6905 . . . . . . . . . 10 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤))
7372oveq1d 7446 . . . . . . . . 9 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))
7473mpteq2dv 5244 . . . . . . . 8 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))
7574oveq2d 7447 . . . . . . 7 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
7675eqeq2d 2748 . . . . . 6 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))))
77 breq1 5146 . . . . . . . 8 (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0))
78 zex 12622 . . . . . . . . . 10 ℤ ∈ V
7978a1i 11 . . . . . . . . 9 (𝜑 → ℤ ∈ V)
80 1zzd 12648 . . . . . . . . . . 11 (((𝜑𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈ ℤ)
81 0zd 12625 . . . . . . . . . . 11 (((𝜑𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈ ℤ)
8280, 81ifclda 4561 . . . . . . . . . 10 ((𝜑𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈ ℤ)
8382fmpttd 7135 . . . . . . . . 9 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ)
8479, 66, 83elmapdd 8881 . . . . . . . 8 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ ↑m Word 𝐴))
8566mptexd 7244 . . . . . . . . 9 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V)
8683ffund 6740 . . . . . . . . 9 (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)))
87 0zd 12625 . . . . . . . . 9 (𝜑 → 0 ∈ ℤ)
88 snfi 9083 . . . . . . . . . 10 {∅} ∈ Fin
8988a1i 11 . . . . . . . . 9 (𝜑 → {∅} ∈ Fin)
90 eldifsni 4790 . . . . . . . . . . . . 13 (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅)
9190adantl 481 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅)
9291neneqd 2945 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅)
9392iffalsed 4536 . . . . . . . . . 10 ((𝜑𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) = 0)
9493, 66suppss2 8225 . . . . . . . . 9 (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})
95 suppssfifsupp 9420 . . . . . . . . 9 ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V ∧ Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∧ 0 ∈ ℤ) ∧ ({∅} ∈ Fin ∧ ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
9685, 86, 87, 89, 94, 95syl32anc 1380 . . . . . . . 8 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
9777, 84, 96elrabd 3694 . . . . . . 7 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
9897, 6eleqtrrdi 2852 . . . . . 6 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹)
99 eqidd 2738 . . . . . 6 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
10076, 98, 99rspcedvdw 3625 . . . . 5 (𝜑 → ∃𝑔𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
101 ovexd 7466 . . . . 5 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
10271, 100, 101elrnmptd 5974 . . . 4 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
103102, 8eleqtrrdi 2852 . . 3 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
10470, 103eqeltrrd 2842 . 2 (𝜑 → (1r𝑅) ∈ 𝑆)
105 simpllr 776 . . . . . . . 8 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
106 simpr 484 . . . . . . . 8 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
107105, 106oveq12d 7449 . . . . . . 7 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))))
108 eqid 2737 . . . . . . . . . . . . . 14 (.r𝑅) = (.r𝑅)
10966ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → Word 𝐴 ∈ V)
1101ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑅 ∈ Ring)
1111ringgrpd 20239 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 ∈ Grp)
112111ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
1136ssrab3 4082 . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 ⊆ (ℤ ↑m Word 𝐴)
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 ⊆ (ℤ ↑m Word 𝐴))
115114sselda 3983 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑔𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
11679, 66elmapd 8880 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
117116adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑔𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
118115, 117mpbid 232 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔𝐹) → 𝑔:Word 𝐴⟶ℤ)
119118ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔𝑤) ∈ ℤ)
12051adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
1212, 4, 112, 119, 120mulgcld 19114 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
122121adantlr 715 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
123122ralrimiva 3146 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
124 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑤 → (𝑔𝑢) = (𝑔𝑤))
125 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤))
126124, 125oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑤 → ((𝑔𝑢) · (𝑀 Σg 𝑢)) = ((𝑔𝑤) · (𝑀 Σg 𝑤)))
127126eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
128127cbvralvw 3237 . . . . . . . . . . . . . . . 16 (∀𝑢 ∈ Word 𝐴((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
129123, 128sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
130129r19.21bi 3251 . . . . . . . . . . . . . 14 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
131111ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
132 breq1 5146 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
133132, 6elrab2 3695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
134133simplbi 497 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖𝐹𝑖 ∈ (ℤ ↑m Word 𝐴))
135134adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
13679, 66elmapd 8880 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
137136adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
138135, 137mpbid 232 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐹) → 𝑖:Word 𝐴⟶ℤ)
139138ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖𝑤) ∈ ℤ)
14051adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
1412, 4, 131, 139, 140mulgcld 19114 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
142141adantllr 719 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
143142ralrimiva 3146 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
144 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑖𝑣) = (𝑖𝑤))
145 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤))
146144, 145oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑤 → ((𝑖𝑣) · (𝑀 Σg 𝑣)) = ((𝑖𝑤) · (𝑀 Σg 𝑤)))
147146eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑤 → (((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
148147cbvralvw 3237 . . . . . . . . . . . . . . . 16 (∀𝑣 ∈ Word 𝐴((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
149143, 148sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
150149r19.21bi 3251 . . . . . . . . . . . . . 14 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
151126cbvmptv 5255 . . . . . . . . . . . . . . 15 (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))
152 fvexd 6921 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → (0g𝑅) ∈ V)
153 0zd 12625 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → 0 ∈ ℤ)
15466adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → Word 𝐴 ∈ V)
155 ssidd 4007 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → Word 𝐴 ⊆ Word 𝐴)
156 breq1 5146 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
157156, 6elrab2 3695 . . . . . . . . . . . . . . . . . . 19 (𝑔𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
158157simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝑔𝐹𝑔 finSupp 0)
159158adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → 𝑔 finSupp 0)
1602, 52, 4mulg0 19092 . . . . . . . . . . . . . . . . . 18 (𝑦𝐵 → (0 · 𝑦) = (0g𝑅))
161160adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑦𝐵) → (0 · 𝑦) = (0g𝑅))
162152, 153, 154, 155, 120, 118, 159, 161fisuppov1 32692 . . . . . . . . . . . . . . . 16 ((𝜑𝑔𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
163162adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
164151, 163eqbrtrid 5178 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))) finSupp (0g𝑅))
165146cbvmptv 5255 . . . . . . . . . . . . . . 15 (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))
166162ralrimiva 3146 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑔𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
167 fveq1 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑖 → (𝑔𝑤) = (𝑖𝑤))
168167oveq1d 7446 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑖 → ((𝑔𝑤) · (𝑀 Σg 𝑤)) = ((𝑖𝑤) · (𝑀 Σg 𝑤)))
169168mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))
170169breq1d 5153 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅)))
171170cbvralvw 3237 . . . . . . . . . . . . . . . . . 18 (∀𝑔𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅) ↔ ∀𝑖𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
172166, 171sylib 218 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
173172r19.21bi 3251 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
174173adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
175165, 174eqbrtrid 5178 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))) finSupp (0g𝑅))
1762, 108, 52, 109, 109, 110, 130, 150, 164, 175gsumdixp 20316 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))))(.r𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))))
177151oveq2i 7442 . . . . . . . . . . . . . . 15 (𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))
178165oveq2i 7442 . . . . . . . . . . . . . . 15 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))
179177, 178oveq12i 7443 . . . . . . . . . . . . . 14 ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))))(.r𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
180179a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))))(.r𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))))
181110ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Ring)
182122adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183111ad4antr 732 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Grp)
184138adantlr 715 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑖:Word 𝐴⟶ℤ)
185184ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑓 ∈ Word 𝐴) → (𝑖𝑓) ∈ ℤ)
186185adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑖𝑓) ∈ ℤ)
18745ad4antr 732 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
18847adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑔𝐹) → Word 𝐴 ⊆ Word 𝐵)
189188ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
190189sselda 3983 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵)
19149gsumwcl 18852 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵)
192187, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵)
1932, 4, 183, 186, 192mulgcld 19114 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)
1942, 108, 181, 182, 193ringcld 20257 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
195194anasss 466 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ (𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴)) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
196195ralrimivva 3202 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴(((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
197 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
198197fmpo 8093 . . . . . . . . . . . . . . . 16 (∀𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴(((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵 ↔ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
199196, 198sylib 218 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
200 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
201 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑓 ∈ V
202200, 201op1std 8024 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ⟨𝑤, 𝑓⟩ → (1st𝑎) = 𝑤)
203202fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑔‘(1st𝑎)) = (𝑔𝑤))
204202oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (1st𝑎)) = (𝑀 Σg 𝑤))
205203, 204oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) = ((𝑔𝑤) · (𝑀 Σg 𝑤)))
206200, 201op2ndd 8025 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ⟨𝑤, 𝑓⟩ → (2nd𝑎) = 𝑓)
207206fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑖‘(2nd𝑎)) = (𝑖𝑓))
208206oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (2nd𝑎)) = (𝑀 Σg 𝑓))
209207, 208oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) = ((𝑖𝑓) · (𝑀 Σg 𝑓)))
210205, 209oveq12d 7449 . . . . . . . . . . . . . . . . 17 (𝑎 = ⟨𝑤, 𝑓⟩ → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
211210mpompt 7547 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
21266, 66xpexd 7771 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V)
213212ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (Word 𝐴 × Word 𝐴) ∈ V)
214213mptexd 7244 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) ∈ V)
215 fvexd 6921 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (0g𝑅) ∈ V)
216110adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Ring)
217111ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Grp)
218118ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
219 xp1st 8046 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st𝑎) ∈ Word 𝐴)
220219adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st𝑎) ∈ Word 𝐴)
221218, 220ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑔‘(1st𝑎)) ∈ ℤ)
222216, 44syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑀 ∈ Mnd)
223188ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
224223, 220sseldd 3984 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st𝑎) ∈ Word 𝐵)
22549gsumwcl 18852 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ Mnd ∧ (1st𝑎) ∈ Word 𝐵) → (𝑀 Σg (1st𝑎)) ∈ 𝐵)
226222, 224, 225syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st𝑎)) ∈ 𝐵)
2272, 4, 217, 221, 226mulgcld 19114 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) ∈ 𝐵)
228184adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
229 xp2nd 8047 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd𝑎) ∈ Word 𝐴)
230229adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐴)
231228, 230ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd𝑎)) ∈ ℤ)
232223, 230sseldd 3984 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐵)
23349gsumwcl 18852 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ Mnd ∧ (2nd𝑎) ∈ Word 𝐵) → (𝑀 Σg (2nd𝑎)) ∈ 𝐵)
234222, 232, 233syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd𝑎)) ∈ 𝐵)
2352, 4, 217, 231, 234mulgcld 19114 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) ∈ 𝐵)
2362, 108, 216, 227, 235ringcld 20257 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) ∈ 𝐵)
237236fmpttd 7135 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))):(Word 𝐴 × Word 𝐴)⟶𝐵)
238237ffund 6740 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → Fun (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))))
239159fsuppimpd 9409 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐹) → (𝑔 supp 0) ∈ Fin)
240133simprbi 496 . . . . . . . . . . . . . . . . . . . . 21 (𝑖𝐹𝑖 finSupp 0)
241240adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑖 finSupp 0)
242241fsuppimpd 9409 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑖 supp 0) ∈ Fin)
243 xpfi 9358 . . . . . . . . . . . . . . . . . . 19 (((𝑔 supp 0) ∈ Fin ∧ (𝑖 supp 0) ∈ Fin) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
244239, 242, 243syl2an2r 685 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
245118ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑔𝐹) → 𝑔 Fn Word 𝐴)
246245adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑔 Fn Word 𝐴)
247246ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑔 Fn Word 𝐴)
248109ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ∈ V)
249 0zd 12625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ)
250 xp1st 8046 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (1st𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
251250adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
252247, 248, 249, 251fvdifsupp 8196 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st𝑎)) = 0)
253252oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) = (0 · (𝑀 Σg (1st𝑎))))
25445ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑀 ∈ Mnd)
255188ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
256251eldifad 3963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st𝑎) ∈ Word 𝐴)
257255, 256sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st𝑎) ∈ Word 𝐵)
258254, 257, 225syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (1st𝑎)) ∈ 𝐵)
2592, 52, 4mulg0 19092 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 Σg (1st𝑎)) ∈ 𝐵 → (0 · (𝑀 Σg (1st𝑎))) = (0g𝑅))
260258, 259syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (0 · (𝑀 Σg (1st𝑎))) = (0g𝑅))
261253, 260eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) = (0g𝑅))
262261oveq1d 7446 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = ((0g𝑅)(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))))
263110ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Ring)
264111ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Grp)
265184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
266 xp2nd 8047 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (2nd𝑎) ∈ Word 𝐴)
267266adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐴)
268265, 267ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd𝑎)) ∈ ℤ)
269255, 267sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐵)
270254, 269, 233syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (2nd𝑎)) ∈ 𝐵)
2712, 4, 264, 268, 270mulgcld 19114 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) ∈ 𝐵)
2722, 108, 52, 263, 271ringlzd 20292 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g𝑅)(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (0g𝑅))
273262, 272eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (0g𝑅))
274138ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖𝐹) → 𝑖 Fn Word 𝐴)
275274adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑖 Fn Word 𝐴)
276275ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑖 Fn Word 𝐴)
277109ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ∈ V)
278 0zd 12625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈ ℤ)
279 xp2nd 8047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (2nd𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
280279adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
281276, 277, 278, 280fvdifsupp 8196 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd𝑎)) = 0)
282281oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) = (0 · (𝑀 Σg (2nd𝑎))))
28345ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑀 ∈ Mnd)
284188ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ⊆ Word 𝐵)
285280eldifad 3963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd𝑎) ∈ Word 𝐴)
286284, 285sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd𝑎) ∈ Word 𝐵)
287283, 286, 233syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (2nd𝑎)) ∈ 𝐵)
2882, 52, 4mulg0 19092 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 Σg (2nd𝑎)) ∈ 𝐵 → (0 · (𝑀 Σg (2nd𝑎))) = (0g𝑅))
289287, 288syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (0 · (𝑀 Σg (2nd𝑎))) = (0g𝑅))
290282, 289eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) = (0g𝑅))
291290oveq2d 7447 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)(0g𝑅)))
292110ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Ring)
293111ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Grp)
294118adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑔:Word 𝐴⟶ℤ)
295294ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑔:Word 𝐴⟶ℤ)
296 xp1st 8046 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (1st𝑎) ∈ Word 𝐴)
297296adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st𝑎) ∈ Word 𝐴)
298295, 297ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st𝑎)) ∈ ℤ)
299284, 297sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st𝑎) ∈ Word 𝐵)
300283, 299, 225syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (1st𝑎)) ∈ 𝐵)
3012, 4, 293, 298, 300mulgcld 19114 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) ∈ 𝐵)
3022, 108, 52, 292, 301ringrzd 20293 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)(0g𝑅)) = (0g𝑅))
303291, 302eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (0g𝑅))
304 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))))
305 difxp 6184 . . . . . . . . . . . . . . . . . . . . . 22 ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))
306304, 305eleqtrdi 2851 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
307 elun 4153 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) ↔ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
308306, 307sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
309273, 303, 308mpjaodan 961 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (0g𝑅))
310309, 213suppss2 8225 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) supp (0g𝑅)) ⊆ ((𝑔 supp 0) × (𝑖 supp 0)))
311244, 310ssfid 9301 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) supp (0g𝑅)) ∈ Fin)
312214, 215, 238, 311isfsuppd 9406 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) finSupp (0g𝑅))
313211, 312eqbrtrrid 5179 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) finSupp (0g𝑅))
31460ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑅 ∈ CMnd)
3157ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝐴𝐵)
3162, 52, 199, 313, 314, 315gsumwrd2dccat 33070 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
317126oveq1d 7446 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))) = (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))
318 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑓 → (𝑖𝑣) = (𝑖𝑓))
319 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓))
320318, 319oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑓 → ((𝑖𝑣) · (𝑀 Σg 𝑣)) = ((𝑖𝑓) · (𝑀 Σg 𝑓)))
321320oveq2d 7447 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑓 → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))) = (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
322317, 321cbvmpov 7528 . . . . . . . . . . . . . . . 16 (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
323322oveq2i 7442 . . . . . . . . . . . . . . 15 (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))))
324323a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))))
325 pfxcctswrd 14748 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ Word 𝐴𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
326325adantll 714 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
327326oveq2d 7447 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) = (𝑀 Σg 𝑣))
328327oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
329328mpteq2dva 5242 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣))))
330329oveq2d 7447 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
331 df-ov 7434 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)
332188sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
333332ad4ant13 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
334187, 333, 50syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
3352, 4, 108mulgass3 20353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ Ring ∧ ((𝑖𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
336181, 186, 334, 192, 335syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
337336oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔𝑤) · ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔𝑤) · ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))))
338119ad4ant13 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔𝑤) ∈ ℤ)
3392, 4, 108mulgass2 20306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ Ring ∧ ((𝑔𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))))
340181, 338, 334, 193, 339syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))))
3412, 108, 181, 334, 192ringcld 20257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)
3422, 4mulgass 19129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ Grp ∧ ((𝑔𝑤) ∈ ℤ ∧ (𝑖𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))))
343183, 338, 186, 341, 342syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))))
344337, 340, 3433eqtr4d 2787 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
3453, 108mgpplusg 20141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (.r𝑅) = (+g𝑀)
34649, 345gsumccat 18854 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))
347187, 333, 190, 346syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))
348347oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
349344, 348eqtr4d 2780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
350349adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
351350adantllr 719 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
3523513impa 1110 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
353352mpoeq3dva 7510 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))))
354 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑣 prefix 𝑗) → (𝑔𝑤) = (𝑔‘(𝑣 prefix 𝑗)))
355 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) → (𝑖𝑓) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
356354, 355oveqan12d 7450 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → ((𝑔𝑤) · (𝑖𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
357 oveq12 7440 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
358357oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
359356, 358oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
360359adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ (𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) → (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
361 pfxcl 14715 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴)
362361ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴)
363 swrdcl 14683 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ Word 𝐴 → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
364363ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
365 ovexd 7466 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) ∈ V)
366353, 360, 362, 364, 365ovmpod 7585 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
367331, 366eqtr3id 2791 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
368367mpteq2dva 5242 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))))
369368oveq2d 7447 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))))
370 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))
371 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣))
372371oveq2d 7447 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣)))
373 fvoveq1 7454 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗)))
374 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑣𝑡 = 𝑣)
375371opeq2d 4880 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑣 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑣)⟩)
376374, 375oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑣 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))
377376fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑣 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
378373, 377oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
379378adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = 𝑣𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
380372, 379sumeq12dv 15742 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
381 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴)
382 fzfid 14014 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin)
383294ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ)
384383, 362ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ)
385184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ)
386385, 364ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) ∈ ℤ)
387384, 386zmulcld 12728 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℤ)
388387zcnd 12723 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
389382, 388fsumcl 15769 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
390370, 380, 381, 389fvmptd3 7039 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
391390oveq1d 7446 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
392111ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑅 ∈ Grp)
39345ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
394315, 46syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → Word 𝐴 ⊆ Word 𝐵)
395394sselda 3983 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵)
39649gsumwcl 18852 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵)
397393, 395, 396syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵)
3982, 4, 392, 382, 397, 387gsummulgc2 33063 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
399391, 398eqtr4d 2780 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
400330, 369, 3993eqtr4rd 2788 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))
401400mpteq2dva 5242 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)))))
402401oveq2d 7447 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
403316, 324, 4023eqtr4d 2787 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
404176, 180, 4033eqtr3d 2785 . . . . . . . . . . . 12 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
405 fveq1 6905 . . . . . . . . . . . . . . . . . 18 (𝑔 = → (𝑔𝑤) = (𝑤))
406405oveq1d 7446 . . . . . . . . . . . . . . . . 17 (𝑔 = → ((𝑔𝑤) · (𝑀 Σg 𝑤)) = ((𝑤) · (𝑀 Σg 𝑤)))
407406mpteq2dv 5244 . . . . . . . . . . . . . . . 16 (𝑔 = → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤))))
408407oveq2d 7447 . . . . . . . . . . . . . . 15 (𝑔 = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))))
409408cbvmptv 5255 . . . . . . . . . . . . . 14 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))))
410 fveq1 6905 . . . . . . . . . . . . . . . . . . 19 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
411410oveq1d 7446 . . . . . . . . . . . . . . . . . 18 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
412411mpteq2dv 5244 . . . . . . . . . . . . . . . . 17 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
413412oveq2d 7447 . . . . . . . . . . . . . . . 16 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
414413eqeq2d 2748 . . . . . . . . . . . . . . 15 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))))
415 breq1 5146 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0))
41678a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ℤ ∈ V)
417 fzfid 14014 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin)
418294ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ)
419 pfxcl 14715 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴)
420419ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴)
421418, 420ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ)
422184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ)
423 swrdcl 14683 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ Word 𝐴 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
424423ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
425422, 424ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) ∈ ℤ)
426421, 425zmulcld 12728 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
427417, 426fsumzcl 15771 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
428427fmpttd 7135 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))):Word 𝐴⟶ℤ)
429416, 109, 428elmapdd 8881 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ (ℤ ↑m Word 𝐴))
430 0zd 12625 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 0 ∈ ℤ)
431428ffund 6740 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))))
432 ccatfn 14610 . . . . . . . . . . . . . . . . . . . . 21 ++ Fn (V × V)
433 fnfun 6668 . . . . . . . . . . . . . . . . . . . . 21 ( ++ Fn (V × V) → Fun ++ )
434432, 433ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Fun ++
435 imafi 9353 . . . . . . . . . . . . . . . . . . . 20 ((Fun ++ ∧ ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
436434, 244, 435sylancr 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
437 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → (♯‘𝑡) = (♯‘𝑤))
438437oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤)))
439 fvoveq1 7454 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗)))
440 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑤𝑡 = 𝑤)
441437opeq2d 4880 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑤 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑤)⟩)
442440, 441oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑤 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))
443442fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
444439, 443oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
445444adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = 𝑤𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
446438, 445sumeq12dv 15742 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
447 oveq1 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣))
448447eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣)))
449 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
450449eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → (𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
451246ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑔 Fn Word 𝐴)
452109ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → Word 𝐴 ∈ V)
453 0zd 12625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 0 ∈ ℤ)
454 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
455454eldifad 3963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴)
456455adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴)
457 pfxcl 14715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ Word 𝐴 → (𝑤 prefix 𝑗) ∈ Word 𝐴)
458456, 457syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
459458ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
460 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑔‘(𝑤 prefix 𝑗)) ≠ 0)
461451, 452, 453, 459, 460elsuppfnd 32691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ (𝑔 supp 0))
462275ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑖 Fn Word 𝐴)
463 swrdcl 14683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ Word 𝐴 → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
464456, 463syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
465464ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
466 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)
467462, 452, 453, 465, 466elsuppfnd 32691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ (𝑖 supp 0))
468456ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ Word 𝐴)
469 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑗 ∈ (0...(♯‘𝑤)))
470 pfxcctswrd 14748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤 ∈ Word 𝐴𝑗 ∈ (0...(♯‘𝑤))) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
471468, 469, 470syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
472471eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
473448, 450, 461, 467, 4722rspcedvdw 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
474 fnov 7564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( ++ Fn (V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)))
475432, 474mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))
476200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⊤ → 𝑤 ∈ V)
477 ssv 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 supp 0) ⊆ V
478477a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⊤ → (𝑔 supp 0) ⊆ V)
479 ssv 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 supp 0) ⊆ V
480479a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⊤ → (𝑖 supp 0) ⊆ V)
481475, 476, 478, 480elimampo 7570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⊤ → (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)))
482481mptru 1547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
483473, 482sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
484483anasss 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
485454ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
486485eldifbd 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
487486anasss 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
488484, 487pm2.65da 817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
489 df-ne 2941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0)
490 df-ne 2941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0 ↔ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)
491489, 490anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
492491notbii 320 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ ¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
493 pm4.57 993 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
494492, 493bitr2i 276 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
495488, 494sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
496294ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑔:Word 𝐴⟶ℤ)
497496, 458ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ)
498497zcnd 12723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ)
499184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ)
500499, 464ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℤ)
501500zcnd 12723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℂ)
502498, 501mul0ord 11913 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0 ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)))
503495, 502mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
504503sumeq2dv 15738 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))0)
505 fzssuz 13605 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(♯‘𝑤)) ⊆ (ℤ‘0)
506 sumz 15758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...(♯‘𝑤)) ⊆ (ℤ‘0) ∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
507506orcs 876 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0...(♯‘𝑤)) ⊆ (ℤ‘0) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
508505, 507mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
509504, 508eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
510446, 509sylan9eqr 2799 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = 0)
511 0zd 12625 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈ ℤ)
512370, 510, 455, 511fvmptd2 7024 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) = 0)
513428, 512suppss 8219 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ⊆ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
514436, 513ssfid 9301 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ∈ Fin)
515429, 430, 431, 514isfsuppd 9406 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0)
516415, 429, 515elrabd 3694 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
517516, 6eleqtrrdi 2852 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ 𝐹)
518 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
519518, 145oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
520519cbvmptv 5255 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
521520oveq2i 7442 . . . . . . . . . . . . . . . 16 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
522521a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
523414, 517, 522rspcedvdw 3625 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∃𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))))
524 ovexd 7466 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V)
525409, 523, 524elrnmptd 5974 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
526525, 8eleqtrrdi 2852 . . . . . . . . . . . 12 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆)
527404, 526eqeltrd 2841 . . . . . . . . . . 11 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
528527adantllr 719 . . . . . . . . . 10 ((((𝜑𝑥𝑆) ∧ 𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
529528adantllr 719 . . . . . . . . 9 (((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
530529adantlr 715 . . . . . . . 8 ((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
531530adantr 480 . . . . . . 7 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
532107, 531eqeltrd 2841 . . . . . 6 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
5338eleq2i 2833 . . . . . . . . 9 (𝑦𝑆𝑦 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
534169oveq2d 7447 . . . . . . . . . . . 12 (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
535534cbvmptv 5255 . . . . . . . . . . 11 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝑖𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
536535elrnmpt 5969 . . . . . . . . . 10 (𝑦 ∈ V → (𝑦 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))))
537536elv 3485 . . . . . . . . 9 (𝑦 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
538533, 537sylbb 219 . . . . . . . 8 (𝑦𝑆 → ∃𝑖𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
539538adantl 481 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑦𝑆) → ∃𝑖𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
540539ad2antrr 726 . . . . . 6 (((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
541532, 540r19.29a 3162 . . . . 5 (((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
5428eleq2i 2833 . . . . . . 7 (𝑥𝑆𝑥 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
54371elrnmpt 5969 . . . . . . . 8 (𝑥 ∈ V → (𝑥 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
544543elv 3485 . . . . . . 7 (𝑥 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
545542, 544sylbb 219 . . . . . 6 (𝑥𝑆 → ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
546545ad2antlr 727 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑦𝑆) → ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
547541, 546r19.29a 3162 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑦𝑆) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
548547anasss 466 . . 3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
549548ralrimivva 3202 . 2 (𝜑 → ∀𝑥𝑆𝑦𝑆 (𝑥(.r𝑅)𝑦) ∈ 𝑆)
5502, 24, 108issubrg2 20592 . . 3 (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r𝑅) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(.r𝑅)𝑦) ∈ 𝑆)))
551550biimpar 477 . 2 ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r𝑅) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(.r𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅))
5521, 9, 104, 549, 551syl13anc 1374 1 (𝜑𝑆 ∈ (SubRing‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wtru 1541  wcel 2108  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  wss 3951  c0 4333  ifcif 4525  {csn 4626  cop 4632   class class class wbr 5143  cmpt 5225   × cxp 5683  ran crn 5686  cima 5688  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  1st c1st 8012  2nd c2nd 8013   supp csupp 8185  m cmap 8866  Fincfn 8985   finSupp cfsupp 9401  cc 11153  0cc0 11155  1c1 11156   · cmul 11160  cz 12613  cuz 12878  ...cfz 13547  chash 14369  Word cword 14552   ++ cconcat 14608   substr csubstr 14678   prefix cpfx 14708  Σcsu 15722  Basecbs 17247  .rcmulr 17298  0gc0g 17484   Σg cgsu 17485  Mndcmnd 18747  Grpcgrp 18951  .gcmg 19085  SubGrpcsubg 19138  CMndccmn 19798  mulGrpcmgp 20137  1rcur 20178  Ringcrg 20230  SubRingcsubrg 20569  RingSpancrgspn 20610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-word 14553  df-concat 14609  df-substr 14679  df-pfx 14709  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-0g 17486  df-gsum 17487  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-mulg 19086  df-subg 19141  df-ghm 19231  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-oppr 20334  df-subrng 20546  df-subrg 20570  df-cnfld 21365  df-zring 21458
This theorem is referenced by:  elrgspnlem4  33249
  Copyright terms: Public domain W3C validator