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 33232
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
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 33231 . 2 (𝜑𝑆 ∈ (SubGrp‘𝑅))
10 eqeq2 2746 . . . . . . 7 ((1r𝑅) = if(𝑤 = ∅, (1r𝑅), (0g𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r𝑅), (0g𝑅))))
11 eqeq2 2746 . . . . . . 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 2734 . . . . . . . . . . . 12 (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))
15 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑣 = ∅) → 𝑣 = ∅)
1615iftrued 4538 . . . . . . . . . . . 12 ((𝜑𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1)
17 wrd0 14573 . . . . . . . . . . . . 13 ∅ ∈ Word 𝐴
1817a1i 11 . . . . . . . . . . . 12 (𝜑 → ∅ ∈ Word 𝐴)
19 1zzd 12645 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
2014, 16, 18, 19fvmptd2 7023 . . . . . . . . . . 11 (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
2120ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
2213, 21eqtrd 2774 . . . . . . . . 9 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1)
2312oveq2d 7446 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg ∅))
24 eqid 2734 . . . . . . . . . . . 12 (1r𝑅) = (1r𝑅)
253, 24ringidval 20200 . . . . . . . . . . 11 (1r𝑅) = (0g𝑀)
2625gsum0 18709 . . . . . . . . . 10 (𝑀 Σg ∅) = (1r𝑅)
2723, 26eqtrdi 2790 . . . . . . . . 9 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r𝑅))
2822, 27oveq12d 7448 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · (1r𝑅)))
292, 24ringidcl 20279 . . . . . . . . . . 11 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
301, 29syl 17 . . . . . . . . . 10 (𝜑 → (1r𝑅) ∈ 𝐵)
312, 4mulg1 19111 . . . . . . . . . 10 ((1r𝑅) ∈ 𝐵 → (1 · (1r𝑅)) = (1r𝑅))
3230, 31syl 17 . . . . . . . . 9 (𝜑 → (1 · (1r𝑅)) = (1r𝑅))
3332ad2antrr 726 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (1 · (1r𝑅)) = (1r𝑅))
3428, 33eqtrd 2774 . . . . . . 7 (((𝜑𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r𝑅))
35 eqeq1 2738 . . . . . . . . . . . . . 14 (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅))
3635notbid 318 . . . . . . . . . . . . 13 (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅))
3736biimparc 479 . . . . . . . . . . . 12 ((¬ 𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
3837adantll 714 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
3938iffalsed 4541 . . . . . . . . . 10 ((((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0)
40 simplr 769 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴)
41 0zd 12622 . . . . . . . . . 10 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈ ℤ)
4214, 39, 40, 41fvmptd2 7023 . . . . . . . . 9 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0)
4342oveq1d 7445 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
443ringmgp 20256 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
451, 44syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ Mnd)
46 sswrd 14556 . . . . . . . . . . . . 13 (𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵)
477, 46syl 17 . . . . . . . . . . . 12 (𝜑 → Word 𝐴 ⊆ Word 𝐵)
4847sselda 3994 . . . . . . . . . . 11 ((𝜑𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
493, 2mgpbas 20157 . . . . . . . . . . . 12 𝐵 = (Base‘𝑀)
5049gsumwcl 18864 . . . . . . . . . . 11 ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
5145, 48, 50syl2an2r 685 . . . . . . . . . 10 ((𝜑𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
52 eqid 2734 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
532, 52, 4mulg0 19104 . . . . . . . . . 10 ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
5451, 53syl 17 . . . . . . . . 9 ((𝜑𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
5554adantr 480 . . . . . . . 8 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (0 · (𝑀 Σg 𝑤)) = (0g𝑅))
5643, 55eqtrd 2774 . . . . . . 7 (((𝜑𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g𝑅))
5710, 11, 34, 56ifbothda 4568 . . . . . 6 ((𝜑𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r𝑅), (0g𝑅)))
5857mpteq2dva 5247 . . . . 5 (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅))))
5958oveq2d 7446 . . . 4 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅)))))
601ringcmnd 20297 . . . . . 6 (𝜑𝑅 ∈ CMnd)
6160cmnmndd 19836 . . . . 5 (𝜑𝑅 ∈ Mnd)
622fvexi 6920 . . . . . . . 8 𝐵 ∈ V
6362a1i 11 . . . . . . 7 (𝜑𝐵 ∈ V)
6463, 7ssexd 5329 . . . . . 6 (𝜑𝐴 ∈ V)
65 wrdexg 14558 . . . . . 6 (𝐴 ∈ V → Word 𝐴 ∈ V)
6664, 65syl 17 . . . . 5 (𝜑 → Word 𝐴 ∈ V)
67 eqid 2734 . . . . 5 (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅)))
6830, 2eleqtrdi 2848 . . . . 5 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
6952, 61, 66, 18, 67, 68gsummptif1n0 19998 . . . 4 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r𝑅), (0g𝑅)))) = (1r𝑅))
7059, 69eqtrd 2774 . . 3 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (1r𝑅))
71 eqid 2734 . . . . 5 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
72 fveq1 6905 . . . . . . . . . 10 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤))
7372oveq1d 7445 . . . . . . . . 9 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))
7473mpteq2dv 5249 . . . . . . . 8 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))
7574oveq2d 7446 . . . . . . 7 (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
7675eqeq2d 2745 . . . . . 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 5150 . . . . . . . 8 (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0))
78 zex 12619 . . . . . . . . . 10 ℤ ∈ V
7978a1i 11 . . . . . . . . 9 (𝜑 → ℤ ∈ V)
80 1zzd 12645 . . . . . . . . . . 11 (((𝜑𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈ ℤ)
81 0zd 12622 . . . . . . . . . . 11 (((𝜑𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈ ℤ)
8280, 81ifclda 4565 . . . . . . . . . 10 ((𝜑𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈ ℤ)
8382fmpttd 7134 . . . . . . . . 9 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ)
8479, 66, 83elmapdd 8879 . . . . . . . 8 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ ↑m Word 𝐴))
8566mptexd 7243 . . . . . . . . 9 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V)
8683ffund 6740 . . . . . . . . 9 (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)))
87 0zd 12622 . . . . . . . . 9 (𝜑 → 0 ∈ ℤ)
88 snfi 9081 . . . . . . . . . 10 {∅} ∈ Fin
8988a1i 11 . . . . . . . . 9 (𝜑 → {∅} ∈ Fin)
90 eldifsni 4794 . . . . . . . . . . . . 13 (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅)
9190adantl 481 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅)
9291neneqd 2942 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅)
9392iffalsed 4541 . . . . . . . . . 10 ((𝜑𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) = 0)
9493, 66suppss2 8223 . . . . . . . . 9 (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})
95 suppssfifsupp 9417 . . . . . . . . 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 1377 . . . . . . . 8 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
9777, 84, 96elrabd 3696 . . . . . . 7 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
9897, 6eleqtrrdi 2849 . . . . . 6 (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹)
99 eqidd 2735 . . . . . 6 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
10076, 98, 99rspcedvdw 3624 . . . . 5 (𝜑 → ∃𝑔𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
101 ovexd 7465 . . . . 5 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
10271, 100, 101elrnmptd 5976 . . . 4 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
103102, 8eleqtrrdi 2849 . . 3 (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
10470, 103eqeltrrd 2839 . 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 7448 . . . . . . 7 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))))
108 eqid 2734 . . . . . . . . . . . . . 14 (.r𝑅) = (.r𝑅)
10966ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → Word 𝐴 ∈ V)
1101ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑅 ∈ Ring)
1111ringgrpd 20259 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 ∈ Grp)
112111ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
1136ssrab3 4091 . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 ⊆ (ℤ ↑m Word 𝐴)
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 ⊆ (ℤ ↑m Word 𝐴))
115114sselda 3994 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑔𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
11679, 66elmapd 8878 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
117116adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑔𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
118115, 117mpbid 232 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔𝐹) → 𝑔:Word 𝐴⟶ℤ)
119118ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔𝑤) ∈ ℤ)
12051adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
1212, 4, 112, 119, 120mulgcld 19126 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
122121adantlr 715 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
123122ralrimiva 3143 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
124 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑤 → (𝑔𝑢) = (𝑔𝑤))
125 oveq2 7438 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤))
126124, 125oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑤 → ((𝑔𝑢) · (𝑀 Σg 𝑢)) = ((𝑔𝑤) · (𝑀 Σg 𝑤)))
127126eleq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
128127cbvralvw 3234 . . . . . . . . . . . . . . . 16 (∀𝑢 ∈ Word 𝐴((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
129123, 128sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
130129r19.21bi 3248 . . . . . . . . . . . . . 14 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
131111ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
132 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
133132, 6elrab2 3697 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
134133simplbi 497 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖𝐹𝑖 ∈ (ℤ ↑m Word 𝐴))
135134adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
13679, 66elmapd 8878 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
137136adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
138135, 137mpbid 232 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐹) → 𝑖:Word 𝐴⟶ℤ)
139138ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖𝑤) ∈ ℤ)
14051adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
1412, 4, 131, 139, 140mulgcld 19126 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
142141adantllr 719 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
143142ralrimiva 3143 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
144 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑖𝑣) = (𝑖𝑤))
145 oveq2 7438 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤))
146144, 145oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑤 → ((𝑖𝑣) · (𝑀 Σg 𝑣)) = ((𝑖𝑤) · (𝑀 Σg 𝑤)))
147146eleq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑤 → (((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
148147cbvralvw 3234 . . . . . . . . . . . . . . . 16 (∀𝑣 ∈ Word 𝐴((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
149143, 148sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
150149r19.21bi 3248 . . . . . . . . . . . . . 14 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
151126cbvmptv 5260 . . . . . . . . . . . . . . 15 (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))
152 fvexd 6921 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → (0g𝑅) ∈ V)
153 0zd 12622 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → 0 ∈ ℤ)
15466adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → Word 𝐴 ∈ V)
155 ssidd 4018 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → Word 𝐴 ⊆ Word 𝐴)
156 breq1 5150 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
157156, 6elrab2 3697 . . . . . . . . . . . . . . . . . . 19 (𝑔𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
158157simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝑔𝐹𝑔 finSupp 0)
159158adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐹) → 𝑔 finSupp 0)
1602, 52, 4mulg0 19104 . . . . . . . . . . . . . . . . . 18 (𝑦𝐵 → (0 · 𝑦) = (0g𝑅))
161160adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑦𝐵) → (0 · 𝑦) = (0g𝑅))
162152, 153, 154, 155, 120, 118, 159, 161fisuppov1 32697 . . . . . . . . . . . . . . . 16 ((𝜑𝑔𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
163162adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
164151, 163eqbrtrid 5182 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))) finSupp (0g𝑅))
165146cbvmptv 5260 . . . . . . . . . . . . . . 15 (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))
166162ralrimiva 3143 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑔𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
167 fveq1 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑖 → (𝑔𝑤) = (𝑖𝑤))
168167oveq1d 7445 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑖 → ((𝑔𝑤) · (𝑀 Σg 𝑤)) = ((𝑖𝑤) · (𝑀 Σg 𝑤)))
169168mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))
170169breq1d 5157 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅)))
171170cbvralvw 3234 . . . . . . . . . . . . . . . . . 18 (∀𝑔𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅) ↔ ∀𝑖𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
172166, 171sylib 218 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
173172r19.21bi 3248 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
174173adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))) finSupp (0g𝑅))
175165, 174eqbrtrid 5182 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))) finSupp (0g𝑅))
1762, 108, 52, 109, 109, 110, 130, 150, 164, 175gsumdixp 20332 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢))))(.r𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))))
177151oveq2i 7441 . . . . . . . . . . . . . . 15 (𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))
178165oveq2i 7441 . . . . . . . . . . . . . . 15 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))
179177, 178oveq12i 7442 . . . . . . . . . . . . . 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 7103 . . . . . . . . . . . . . . . . . . . . 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 3994 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵)
19149gsumwcl 18864 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵)
192187, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵)
1932, 4, 183, 186, 192mulgcld 19126 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)
1942, 108, 181, 182, 193ringcld 20276 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
195194anasss 466 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ (𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴)) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
196195ralrimivva 3199 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∀𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴(((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
197 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
198197fmpo 8091 . . . . . . . . . . . . . . . 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 3481 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
201 vex 3481 . . . . . . . . . . . . . . . . . . . . 21 𝑓 ∈ V
202200, 201op1std 8022 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ⟨𝑤, 𝑓⟩ → (1st𝑎) = 𝑤)
203202fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑔‘(1st𝑎)) = (𝑔𝑤))
204202oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (1st𝑎)) = (𝑀 Σg 𝑤))
205203, 204oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) = ((𝑔𝑤) · (𝑀 Σg 𝑤)))
206200, 201op2ndd 8023 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ⟨𝑤, 𝑓⟩ → (2nd𝑎) = 𝑓)
207206fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑖‘(2nd𝑎)) = (𝑖𝑓))
208206oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (2nd𝑎)) = (𝑀 Σg 𝑓))
209207, 208oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) = ((𝑖𝑓) · (𝑀 Σg 𝑓)))
210205, 209oveq12d 7448 . . . . . . . . . . . . . . . . 17 (𝑎 = ⟨𝑤, 𝑓⟩ → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
211210mpompt 7546 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
21266, 66xpexd 7769 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V)
213212ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (Word 𝐴 × Word 𝐴) ∈ V)
214213mptexd 7243 . . . . . . . . . . . . . . . . 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 8044 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st𝑎) ∈ Word 𝐴)
220219adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st𝑎) ∈ Word 𝐴)
221218, 220ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑔‘(1st𝑎)) ∈ ℤ)
222216, 44syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑀 ∈ Mnd)
223188ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
224223, 220sseldd 3995 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st𝑎) ∈ Word 𝐵)
22549gsumwcl 18864 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ Mnd ∧ (1st𝑎) ∈ Word 𝐵) → (𝑀 Σg (1st𝑎)) ∈ 𝐵)
226222, 224, 225syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st𝑎)) ∈ 𝐵)
2272, 4, 217, 221, 226mulgcld 19126 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) ∈ 𝐵)
228184adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
229 xp2nd 8045 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd𝑎) ∈ Word 𝐴)
230229adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐴)
231228, 230ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd𝑎)) ∈ ℤ)
232223, 230sseldd 3995 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐵)
23349gsumwcl 18864 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ Mnd ∧ (2nd𝑎) ∈ Word 𝐵) → (𝑀 Σg (2nd𝑎)) ∈ 𝐵)
234222, 232, 233syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd𝑎)) ∈ 𝐵)
2352, 4, 217, 231, 234mulgcld 19126 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) ∈ 𝐵)
2362, 108, 216, 227, 235ringcld 20276 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) ∈ 𝐵)
237236fmpttd 7134 . . . . . . . . . . . . . . . . . 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 9406 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐹) → (𝑔 supp 0) ∈ Fin)
240133simprbi 496 . . . . . . . . . . . . . . . . . . . . 21 (𝑖𝐹𝑖 finSupp 0)
241240adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑖 finSupp 0)
242241fsuppimpd 9406 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑖 supp 0) ∈ Fin)
243 xpfi 9355 . . . . . . . . . . . . . . . . . . 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 12622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ)
250 xp1st 8044 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8194 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st𝑎)) = 0)
253252oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . 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 3974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st𝑎) ∈ Word 𝐴)
257255, 256sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . 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 19104 . . . . . . . . . . . . . . . . . . . . . . . 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 2774 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) = (0g𝑅))
262261oveq1d 7445 . . . . . . . . . . . . . . . . . . . . 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 8045 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (2nd𝑎) ∈ Word 𝐴)
267266adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd𝑎) ∈ Word 𝐴)
268265, 267ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd𝑎)) ∈ ℤ)
269255, 267sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . 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 19126 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) ∈ 𝐵)
2722, 108, 52, 263, 271ringlzd 20308 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g𝑅)(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (0g𝑅))
273262, 272eqtrd 2774 . . . . . . . . . . . . . . . . . . . 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 12622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈ ℤ)
279 xp2nd 8045 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8194 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd𝑎)) = 0)
282281oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . 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 3974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd𝑎) ∈ Word 𝐴)
286284, 285sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . 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 19104 . . . . . . . . . . . . . . . . . . . . . . . 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 2774 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))) = (0g𝑅))
291290oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 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 8044 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (1st𝑎) ∈ Word 𝐴)
297296adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st𝑎) ∈ Word 𝐴)
298295, 297ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st𝑎)) ∈ ℤ)
299284, 297sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . 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 19126 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎))) ∈ 𝐵)
3022, 108, 52, 292, 301ringrzd 20309 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)(0g𝑅)) = (0g𝑅))
303291, 302eqtrd 2774 . . . . . . . . . . . . . . . . . . . 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 6185 . . . . . . . . . . . . . . . . . . . . . 22 ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))
306304, 305eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
307 elun 4162 . . . . . . . . . . . . . . . . . . . . 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 960 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎)))) = (0g𝑅))
310309, 213suppss2 8223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) supp (0g𝑅)) ⊆ ((𝑔 supp 0) × (𝑖 supp 0)))
311244, 310ssfid 9298 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) supp (0g𝑅)) ∈ Fin)
312214, 215, 238, 311isfsuppd 9403 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st𝑎)) · (𝑀 Σg (1st𝑎)))(.r𝑅)((𝑖‘(2nd𝑎)) · (𝑀 Σg (2nd𝑎))))) finSupp (0g𝑅))
313211, 312eqbrtrrid 5183 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) finSupp (0g𝑅))
31460ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝑅 ∈ CMnd)
3157ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 𝐴𝐵)
3162, 52, 199, 313, 314, 315gsumwrd2dccat 33052 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
317126oveq1d 7445 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))) = (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))
318 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑓 → (𝑖𝑣) = (𝑖𝑓))
319 oveq2 7438 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓))
320318, 319oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑓 → ((𝑖𝑣) · (𝑀 Σg 𝑣)) = ((𝑖𝑓) · (𝑀 Σg 𝑓)))
321320oveq2d 7446 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑓 → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))) = (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
322317, 321cbvmpov 7527 . . . . . . . . . . . . . . . 16 (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))
323322oveq2i 7441 . . . . . . . . . . . . . . 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 14744 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ Word 𝐴𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
326325adantll 714 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
327326oveq2d 7446 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) = (𝑀 Σg 𝑣))
328327oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
329328mpteq2dva 5247 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣))))
330329oveq2d 7446 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
331 df-ov 7433 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)
332188sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑔𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
333332ad4ant13 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
334187, 333, 50syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
3352, 4, 108mulgass3 20369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ Ring ∧ ((𝑖𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
336181, 186, 334, 192, 335syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
337336oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔𝑤) · ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔𝑤) · ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))))
338119ad4ant13 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔𝑤) ∈ ℤ)
3392, 4, 108mulgass2 20322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ Ring ∧ ((𝑔𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))))
340181, 338, 334, 193, 339syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑀 Σg 𝑤)(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓)))))
3412, 108, 181, 334, 192ringcld 20276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)
3422, 4mulgass 19141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ Grp ∧ ((𝑔𝑤) ∈ ℤ ∧ (𝑖𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))))
343183, 338, 186, 341, 342syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))) = ((𝑔𝑤) · ((𝑖𝑓) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))))
344337, 340, 3433eqtr4d 2784 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
3453, 108mgpplusg 20155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (.r𝑅) = (+g𝑀)
34649, 345gsumccat 18866 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))
347187, 333, 190, 346syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓)))
348347oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · ((𝑀 Σg 𝑤)(.r𝑅)(𝑀 Σg 𝑓))))
349344, 348eqtr4d 2777 . . . . . . . . . . . . . . . . . . . . . . . . 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 1109 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴) → (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))) = (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
353352mpoeq3dva 7509 . . . . . . . . . . . . . . . . . . . . 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 7449 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → ((𝑔𝑤) · (𝑖𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
357 oveq12 7439 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
358357oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
359356, 358oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
360359adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ (𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) → (((𝑔𝑤) · (𝑖𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
361 pfxcl 14711 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴)
362361ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴)
363 swrdcl 14679 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ Word 𝐴 → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
364363ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
365 ovexd 7465 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) ∈ V)
366353, 360, 362, 364, 365ovmpod 7584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
367331, 366eqtr3id 2788 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
368367mpteq2dva 5247 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))))
369368oveq2d 7446 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))))
370 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))
371 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣))
372371oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣)))
373 fvoveq1 7453 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗)))
374 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑣𝑡 = 𝑣)
375371opeq2d 4884 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑣 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑣)⟩)
376374, 375oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑣 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))
377376fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑣 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
378373, 377oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
379378adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 = 𝑣𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
380372, 379sumeq12dv 15738 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
381 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴)
382 fzfid 14010 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin)
383294ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ)
384383, 362ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ)
385184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ)
386385, 364ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) ∈ ℤ)
387384, 386zmulcld 12725 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℤ)
388387zcnd 12720 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
389382, 388fsumcl 15765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
390370, 380, 381, 389fvmptd3 7038 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
391390oveq1d 7445 . . . . . . . . . . . . . . . . . 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 3994 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵)
39649gsumwcl 18864 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵)
397393, 395, 396syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵)
3982, 4, 392, 382, 397, 387gsummulgc2 33045 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
399391, 398eqtr4d 2777 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
400330, 369, 3993eqtr4rd 2785 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))
401400mpteq2dva 5247 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)))))
402401oveq2d 7446 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔𝑤) · (𝑀 Σg 𝑤))(.r𝑅)((𝑖𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
403316, 324, 4023eqtr4d 2784 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔𝑢) · (𝑀 Σg 𝑢))(.r𝑅)((𝑖𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
404176, 180, 4033eqtr3d 2782 . . . . . . . . . . . 12 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))(.r𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
405 fveq1 6905 . . . . . . . . . . . . . . . . . 18 (𝑔 = → (𝑔𝑤) = (𝑤))
406405oveq1d 7445 . . . . . . . . . . . . . . . . 17 (𝑔 = → ((𝑔𝑤) · (𝑀 Σg 𝑤)) = ((𝑤) · (𝑀 Σg 𝑤)))
407406mpteq2dv 5249 . . . . . . . . . . . . . . . 16 (𝑔 = → (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤))))
408407oveq2d 7446 . . . . . . . . . . . . . . 15 (𝑔 = → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))))
409408cbvmptv 5260 . . . . . . . . . . . . . 14 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))))
410 fveq1 6905 . . . . . . . . . . . . . . . . . . 19 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
411410oveq1d 7445 . . . . . . . . . . . . . . . . . 18 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
412411mpteq2dv 5249 . . . . . . . . . . . . . . . . 17 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
413412oveq2d 7446 . . . . . . . . . . . . . . . 16 ( = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
414413eqeq2d 2745 . . . . . . . . . . . . . . 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 5150 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0))
41678a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ℤ ∈ V)
417 fzfid 14010 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin)
418294ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ)
419 pfxcl 14711 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴)
420419ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴)
421418, 420ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ)
422184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ)
423 swrdcl 14679 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ Word 𝐴 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
424423ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
425422, 424ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) ∈ ℤ)
426421, 425zmulcld 12725 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
427417, 426fsumzcl 15767 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
428427fmpttd 7134 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))):Word 𝐴⟶ℤ)
429416, 109, 428elmapdd 8879 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ (ℤ ↑m Word 𝐴))
430 0zd 12622 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → 0 ∈ ℤ)
431428ffund 6740 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))))
432 ccatfn 14606 . . . . . . . . . . . . . . . . . . . . 21 ++ Fn (V × V)
433 fnfun 6668 . . . . . . . . . . . . . . . . . . . . 21 ( ++ Fn (V × V) → Fun ++ )
434432, 433ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Fun ++
435 imafi 9350 . . . . . . . . . . . . . . . . . . . 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 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤)))
439 fvoveq1 7453 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗)))
440 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑤𝑡 = 𝑤)
441437opeq2d 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑤 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑤)⟩)
442440, 441oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑤 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))
443442fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑤 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
444439, 443oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
445444adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 = 𝑤𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
446438, 445sumeq12dv 15738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
447 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣))
448447eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣)))
449 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
450449eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴)
456455adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴)
457 pfxcl 14711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 32696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 32696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤 ∈ Word 𝐴𝑗 ∈ (0...(♯‘𝑤))) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
471468, 469, 470syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
472471eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
473448, 450, 461, 467, 4722rspcedvdw 3635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
474 fnov 7563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( ++ Fn (V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)))
475432, 474mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))
476200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⊤ → 𝑤 ∈ V)
477 ssv 4019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 supp 0) ⊆ V
478477a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⊤ → (𝑔 supp 0) ⊆ V)
479 ssv 4019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 supp 0) ⊆ V
480479a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⊤ → (𝑖 supp 0) ⊆ V)
481475, 476, 478, 480elimampo 7569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⊤ → (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)))
482481mptru 1543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0)
490 df-ne 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 992 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ)
498497zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ)
499184ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ)
500499, 464ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℤ)
501500zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℂ)
502498, 501mul0ord 11910 . . . . . . . . . . . . . . . . . . . . . . . . 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 15734 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))0)
505 fzssuz 13601 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(♯‘𝑤)) ⊆ (ℤ‘0)
506 sumz 15754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...(♯‘𝑤)) ⊆ (ℤ‘0) ∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
507506orcs 875 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0...(♯‘𝑤)) ⊆ (ℤ‘0) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
508505, 507mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
509504, 508eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
510446, 509sylan9eqr 2796 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = 0)
511 0zd 12622 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈ ℤ)
512370, 510, 455, 511fvmptd2 7023 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑔𝐹) ∧ 𝑖𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) = 0)
513428, 512suppss 8217 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ⊆ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
514436, 513ssfid 9298 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ∈ Fin)
515429, 430, 431, 514isfsuppd 9403 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0)
516415, 429, 515elrabd 3696 . . . . . . . . . . . . . . . 16 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
517516, 6eleqtrrdi 2849 . . . . . . . . . . . . . . 15 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ 𝐹)
518 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
519518, 145oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
520519cbvmptv 5260 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
521520oveq2i 7441 . . . . . . . . . . . . . . . 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 3624 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → ∃𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑤) · (𝑀 Σg 𝑤)))))
524 ovexd 7465 . . . . . . . . . . . . . 14 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V)
525409, 523, 524elrnmptd 5976 . . . . . . . . . . . . 13 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
526525, 8eleqtrrdi 2849 . . . . . . . . . . . 12 (((𝜑𝑔𝐹) ∧ 𝑖𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆)
527404, 526eqeltrd 2838 . . . . . . . . . . 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 2838 . . . . . 6 (((((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
5338eleq2i 2830 . . . . . . . . 9 (𝑦𝑆𝑦 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
534169oveq2d 7446 . . . . . . . . . . . 12 (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
535534cbvmptv 5260 . . . . . . . . . . 11 (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) = (𝑖𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤)))))
536535elrnmpt 5971 . . . . . . . . . 10 (𝑦 ∈ V → (𝑦 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖𝑤) · (𝑀 Σg 𝑤))))))
537536elv 3482 . . . . . . . . 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 3159 . . . . 5 (((((𝜑𝑥𝑆) ∧ 𝑦𝑆) ∧ 𝑔𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
5428eleq2i 2830 . . . . . . 7 (𝑥𝑆𝑥 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
54371elrnmpt 5971 . . . . . . . 8 (𝑥 ∈ V → (𝑥 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))))
544543elv 3482 . . . . . . 7 (𝑥 ∈ ran (𝑔𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
545542, 544sylbb 219 . . . . . 6 (𝑥𝑆 → ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
546545ad2antlr 727 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑦𝑆) → ∃𝑔𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔𝑤) · (𝑀 Σg 𝑤)))))
547541, 546r19.29a 3159 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑦𝑆) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
548547anasss 466 . . 3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥(.r𝑅)𝑦) ∈ 𝑆)
549548ralrimivva 3199 . 2 (𝜑 → ∀𝑥𝑆𝑦𝑆 (𝑥(.r𝑅)𝑦) ∈ 𝑆)
5502, 24, 108issubrg2 20608 . . 3 (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r𝑅) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(.r𝑅)𝑦) ∈ 𝑆)))
551550biimpar 477 . 2 ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r𝑅) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(.r𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅))
5521, 9, 104, 549, 551syl13anc 1371 1 (𝜑𝑆 ∈ (SubRing‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wtru 1537  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  cun 3960  wss 3962  c0 4338  ifcif 4530  {csn 4630  cop 4636   class class class wbr 5147  cmpt 5230   × cxp 5686  ran crn 5689  cima 5691  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  cmpo 7432  1st c1st 8010  2nd c2nd 8011   supp csupp 8183  m cmap 8864  Fincfn 8983   finSupp cfsupp 9398  cc 11150  0cc0 11152  1c1 11153   · cmul 11157  cz 12610  cuz 12875  ...cfz 13543  chash 14365  Word cword 14548   ++ cconcat 14604   substr csubstr 14674   prefix cpfx 14704  Σcsu 15718  Basecbs 17244  .rcmulr 17298  0gc0g 17485   Σg cgsu 17486  Mndcmnd 18759  Grpcgrp 18963  .gcmg 19097  SubGrpcsubg 19150  CMndccmn 19812  mulGrpcmgp 20151  1rcur 20198  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-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-cnfld 21382  df-zring 21475
This theorem is referenced by:  elrgspnlem4  33234
  Copyright terms: Public domain W3C validator