Metamath Proof Explorer


Theorem elrgspnlem2

Description: Lemma for elrgspn . (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses 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 elrgspnlem2 ( 𝜑𝑆 ∈ ( SubRing ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 elrgspn.b 𝐵 = ( Base ‘ 𝑅 )
2 elrgspn.m 𝑀 = ( mulGrp ‘ 𝑅 )
3 elrgspn.x · = ( .g𝑅 )
4 elrgspn.n 𝑁 = ( RingSpan ‘ 𝑅 )
5 elrgspn.f 𝐹 = { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 }
6 elrgspn.r ( 𝜑𝑅 ∈ Ring )
7 elrgspn.a ( 𝜑𝐴𝐵 )
8 elrgspnlem1.1 𝑆 = ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
9 1 2 3 4 5 6 7 8 elrgspnlem1 ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
10 eqeq2 ( ( 1r𝑅 ) = if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) → ( ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 1r𝑅 ) ↔ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) )
11 eqeq2 ( ( 0g𝑅 ) = if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) → ( ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) ↔ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) )
12 simpr ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → 𝑤 = ∅ )
13 12 fveq2d ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) = ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ ∅ ) )
14 eqid ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) )
15 simpr ( ( 𝜑𝑣 = ∅ ) → 𝑣 = ∅ )
16 15 iftrued ( ( 𝜑𝑣 = ∅ ) → if ( 𝑣 = ∅ , 1 , 0 ) = 1 )
17 wrd0 ∅ ∈ Word 𝐴
18 17 a1i ( 𝜑 → ∅ ∈ Word 𝐴 )
19 1zzd ( 𝜑 → 1 ∈ ℤ )
20 14 16 18 19 fvmptd2 ( 𝜑 → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ ∅ ) = 1 )
21 20 ad2antrr ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ ∅ ) = 1 )
22 13 21 eqtrd ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) = 1 )
23 12 oveq2d ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg ∅ ) )
24 eqid ( 1r𝑅 ) = ( 1r𝑅 )
25 2 24 ringidval ( 1r𝑅 ) = ( 0g𝑀 )
26 25 gsum0 ( 𝑀 Σg ∅ ) = ( 1r𝑅 )
27 23 26 eqtrdi ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( 𝑀 Σg 𝑤 ) = ( 1r𝑅 ) )
28 22 27 oveq12d ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 1 · ( 1r𝑅 ) ) )
29 1 24 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ 𝐵 )
30 6 29 syl ( 𝜑 → ( 1r𝑅 ) ∈ 𝐵 )
31 1 3 mulg1 ( ( 1r𝑅 ) ∈ 𝐵 → ( 1 · ( 1r𝑅 ) ) = ( 1r𝑅 ) )
32 30 31 syl ( 𝜑 → ( 1 · ( 1r𝑅 ) ) = ( 1r𝑅 ) )
33 32 ad2antrr ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( 1 · ( 1r𝑅 ) ) = ( 1r𝑅 ) )
34 28 33 eqtrd ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ∅ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 1r𝑅 ) )
35 eqeq1 ( 𝑣 = 𝑤 → ( 𝑣 = ∅ ↔ 𝑤 = ∅ ) )
36 35 notbid ( 𝑣 = 𝑤 → ( ¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅ ) )
37 36 biimparc ( ( ¬ 𝑤 = ∅ ∧ 𝑣 = 𝑤 ) → ¬ 𝑣 = ∅ )
38 37 adantll ( ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) ∧ 𝑣 = 𝑤 ) → ¬ 𝑣 = ∅ )
39 38 iffalsed ( ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) ∧ 𝑣 = 𝑤 ) → if ( 𝑣 = ∅ , 1 , 0 ) = 0 )
40 simplr ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) → 𝑤 ∈ Word 𝐴 )
41 0zd ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) → 0 ∈ ℤ )
42 14 39 40 41 fvmptd2 ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) = 0 )
43 42 oveq1d ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
44 2 ringmgp ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
45 6 44 syl ( 𝜑𝑀 ∈ Mnd )
46 sswrd ( 𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵 )
47 7 46 syl ( 𝜑 → Word 𝐴 ⊆ Word 𝐵 )
48 47 sselda ( ( 𝜑𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
49 2 1 mgpbas 𝐵 = ( Base ‘ 𝑀 )
50 49 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
51 45 48 50 syl2an2r ( ( 𝜑𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
52 eqid ( 0g𝑅 ) = ( 0g𝑅 )
53 1 52 3 mulg0 ( ( 𝑀 Σg 𝑤 ) ∈ 𝐵 → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
54 51 53 syl ( ( 𝜑𝑤 ∈ Word 𝐴 ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
55 54 adantr ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
56 43 55 eqtrd ( ( ( 𝜑𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ∅ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
57 10 11 34 56 ifbothda ( ( 𝜑𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) )
58 57 mpteq2dva ( 𝜑 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) )
59 58 oveq2d ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) )
60 6 ringcmnd ( 𝜑𝑅 ∈ CMnd )
61 60 cmnmndd ( 𝜑𝑅 ∈ Mnd )
62 1 fvexi 𝐵 ∈ V
63 62 a1i ( 𝜑𝐵 ∈ V )
64 63 7 ssexd ( 𝜑𝐴 ∈ V )
65 wrdexg ( 𝐴 ∈ V → Word 𝐴 ∈ V )
66 64 65 syl ( 𝜑 → Word 𝐴 ∈ V )
67 eqid ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) )
68 30 1 eleqtrdi ( 𝜑 → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
69 52 61 66 18 67 68 gsummptif1n0 ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ∅ , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) = ( 1r𝑅 ) )
70 59 69 eqtrd ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 1r𝑅 ) )
71 eqid ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
72 fveq1 ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) → ( 𝑔𝑤 ) = ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) )
73 72 oveq1d ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
74 73 mpteq2dv ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
75 74 oveq2d ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
76 75 eqeq2d ( 𝑔 = ( 𝑣 ∈ 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 ( 𝑓 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) → ( 𝑓 finSupp 0 ↔ ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) finSupp 0 ) )
78 zex ℤ ∈ V
79 78 a1i ( 𝜑 → ℤ ∈ V )
80 1zzd ( ( ( 𝜑𝑣 ∈ Word 𝐴 ) ∧ 𝑣 = ∅ ) → 1 ∈ ℤ )
81 0zd ( ( ( 𝜑𝑣 ∈ Word 𝐴 ) ∧ ¬ 𝑣 = ∅ ) → 0 ∈ ℤ )
82 80 81 ifclda ( ( 𝜑𝑣 ∈ Word 𝐴 ) → if ( 𝑣 = ∅ , 1 , 0 ) ∈ ℤ )
83 82 fmpttd ( 𝜑 → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) : Word 𝐴 ⟶ ℤ )
84 79 66 83 elmapdd ( 𝜑 → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ∈ ( ℤ ↑m Word 𝐴 ) )
85 66 mptexd ( 𝜑 → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ∈ V )
86 83 ffund ( 𝜑 → Fun ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) )
87 0zd ( 𝜑 → 0 ∈ ℤ )
88 snfi { ∅ } ∈ Fin
89 88 a1i ( 𝜑 → { ∅ } ∈ Fin )
90 eldifsni ( 𝑣 ∈ ( Word 𝐴 ∖ { ∅ } ) → 𝑣 ≠ ∅ )
91 90 adantl ( ( 𝜑𝑣 ∈ ( Word 𝐴 ∖ { ∅ } ) ) → 𝑣 ≠ ∅ )
92 91 neneqd ( ( 𝜑𝑣 ∈ ( Word 𝐴 ∖ { ∅ } ) ) → ¬ 𝑣 = ∅ )
93 92 iffalsed ( ( 𝜑𝑣 ∈ ( Word 𝐴 ∖ { ∅ } ) ) → if ( 𝑣 = ∅ , 1 , 0 ) = 0 )
94 93 66 suppss2 ( 𝜑 → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) supp 0 ) ⊆ { ∅ } )
95 suppssfifsupp ( ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ∈ V ∧ Fun ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ∧ 0 ∈ ℤ ) ∧ ( { ∅ } ∈ Fin ∧ ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) supp 0 ) ⊆ { ∅ } ) ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) finSupp 0 )
96 85 86 87 89 94 95 syl32anc ( 𝜑 → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) finSupp 0 )
97 77 84 96 elrabd ( 𝜑 → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
98 97 5 eleqtrrdi ( 𝜑 → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ∈ 𝐹 )
99 eqidd ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
100 76 98 99 rspcedvdw ( 𝜑 → ∃ 𝑔𝐹 ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
101 ovexd ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ V )
102 71 100 101 elrnmptd ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
103 102 8 eleqtrrdi ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ∅ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑆 )
104 70 103 eqeltrrd ( 𝜑 → ( 1r𝑅 ) ∈ 𝑆 )
105 simpllr ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
106 simpr ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
107 105 106 oveq12d ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
108 eqid ( .r𝑅 ) = ( .r𝑅 )
109 66 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → Word 𝐴 ∈ V )
110 6 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑅 ∈ Ring )
111 6 ringgrpd ( 𝜑𝑅 ∈ Grp )
112 111 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
113 5 ssrab3 𝐹 ⊆ ( ℤ ↑m Word 𝐴 )
114 113 a1i ( 𝜑𝐹 ⊆ ( ℤ ↑m Word 𝐴 ) )
115 114 sselda ( ( 𝜑𝑔𝐹 ) → 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
116 79 66 elmapd ( 𝜑 → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑔 : Word 𝐴 ⟶ ℤ ) )
117 116 adantr ( ( 𝜑𝑔𝐹 ) → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑔 : Word 𝐴 ⟶ ℤ ) )
118 115 117 mpbid ( ( 𝜑𝑔𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
119 118 ffvelcdmda ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) ∈ ℤ )
120 51 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
121 1 3 112 119 120 mulgcld ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
122 121 adantlr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
123 122 ralrimiva ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∀ 𝑤 ∈ Word 𝐴 ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
124 fveq2 ( 𝑢 = 𝑤 → ( 𝑔𝑢 ) = ( 𝑔𝑤 ) )
125 oveq2 ( 𝑢 = 𝑤 → ( 𝑀 Σg 𝑢 ) = ( 𝑀 Σg 𝑤 ) )
126 124 125 oveq12d ( 𝑢 = 𝑤 → ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) = ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
127 126 eleq1d ( 𝑢 = 𝑤 → ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ∈ 𝐵 ↔ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 ) )
128 127 cbvralvw ( ∀ 𝑢 ∈ Word 𝐴 ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ∈ 𝐵 ↔ ∀ 𝑤 ∈ Word 𝐴 ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
129 123 128 sylibr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∀ 𝑢 ∈ Word 𝐴 ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ∈ 𝐵 )
130 129 r19.21bi ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑢 ∈ Word 𝐴 ) → ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ∈ 𝐵 )
131 111 ad2antrr ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
132 breq1 ( 𝑓 = 𝑖 → ( 𝑓 finSupp 0 ↔ 𝑖 finSupp 0 ) )
133 132 5 elrab2 ( 𝑖𝐹 ↔ ( 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑖 finSupp 0 ) )
134 133 simplbi ( 𝑖𝐹𝑖 ∈ ( ℤ ↑m Word 𝐴 ) )
135 134 adantl ( ( 𝜑𝑖𝐹 ) → 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) )
136 79 66 elmapd ( 𝜑 → ( 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑖 : Word 𝐴 ⟶ ℤ ) )
137 136 adantr ( ( 𝜑𝑖𝐹 ) → ( 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑖 : Word 𝐴 ⟶ ℤ ) )
138 135 137 mpbid ( ( 𝜑𝑖𝐹 ) → 𝑖 : Word 𝐴 ⟶ ℤ )
139 138 ffvelcdmda ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑖𝑤 ) ∈ ℤ )
140 51 adantlr ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
141 1 3 131 139 140 mulgcld ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
142 141 adantllr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
143 142 ralrimiva ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∀ 𝑤 ∈ Word 𝐴 ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
144 fveq2 ( 𝑣 = 𝑤 → ( 𝑖𝑣 ) = ( 𝑖𝑤 ) )
145 oveq2 ( 𝑣 = 𝑤 → ( 𝑀 Σg 𝑣 ) = ( 𝑀 Σg 𝑤 ) )
146 144 145 oveq12d ( 𝑣 = 𝑤 → ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) = ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
147 146 eleq1d ( 𝑣 = 𝑤 → ( ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ∈ 𝐵 ↔ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 ) )
148 147 cbvralvw ( ∀ 𝑣 ∈ Word 𝐴 ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ∈ 𝐵 ↔ ∀ 𝑤 ∈ Word 𝐴 ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
149 143 148 sylibr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∀ 𝑣 ∈ Word 𝐴 ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ∈ 𝐵 )
150 149 r19.21bi ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ∈ 𝐵 )
151 126 cbvmptv ( 𝑢 ∈ Word 𝐴 ↦ ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
152 fvexd ( ( 𝜑𝑔𝐹 ) → ( 0g𝑅 ) ∈ V )
153 0zd ( ( 𝜑𝑔𝐹 ) → 0 ∈ ℤ )
154 66 adantr ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ∈ V )
155 ssidd ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ⊆ Word 𝐴 )
156 breq1 ( 𝑓 = 𝑔 → ( 𝑓 finSupp 0 ↔ 𝑔 finSupp 0 ) )
157 156 5 elrab2 ( 𝑔𝐹 ↔ ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
158 157 simprbi ( 𝑔𝐹𝑔 finSupp 0 )
159 158 adantl ( ( 𝜑𝑔𝐹 ) → 𝑔 finSupp 0 )
160 1 52 3 mulg0 ( 𝑦𝐵 → ( 0 · 𝑦 ) = ( 0g𝑅 ) )
161 160 adantl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑦𝐵 ) → ( 0 · 𝑦 ) = ( 0g𝑅 ) )
162 152 153 154 155 120 118 159 161 fisuppov1 ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
163 162 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
164 151 163 eqbrtrid ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑢 ∈ Word 𝐴 ↦ ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ) finSupp ( 0g𝑅 ) )
165 146 cbvmptv ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
166 162 ralrimiva ( 𝜑 → ∀ 𝑔𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
167 fveq1 ( 𝑔 = 𝑖 → ( 𝑔𝑤 ) = ( 𝑖𝑤 ) )
168 167 oveq1d ( 𝑔 = 𝑖 → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
169 168 mpteq2dv ( 𝑔 = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
170 169 breq1d ( 𝑔 = 𝑖 → ( ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) ↔ ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) ) )
171 170 cbvralvw ( ∀ 𝑔𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) ↔ ∀ 𝑖𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
172 166 171 sylib ( 𝜑 → ∀ 𝑖𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
173 172 r19.21bi ( ( 𝜑𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
174 173 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
175 165 174 eqbrtrid ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) finSupp ( 0g𝑅 ) )
176 1 108 52 109 109 110 130 150 164 175 gsumdixp ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 ↦ ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) = ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 , 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) )
177 151 oveq2i ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 ↦ ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
178 165 oveq2i ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
179 177 178 oveq12i ( ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 ↦ ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
180 179 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 ↦ ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
181 110 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → 𝑅 ∈ Ring )
182 122 adantr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
183 111 ad4antr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
184 138 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 : Word 𝐴 ⟶ ℤ )
185 184 ffvelcdmda ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( 𝑖𝑓 ) ∈ ℤ )
186 185 adantlr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( 𝑖𝑓 ) ∈ ℤ )
187 45 ad4antr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → 𝑀 ∈ Mnd )
188 47 adantr ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ⊆ Word 𝐵 )
189 188 ad2antrr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → Word 𝐴 ⊆ Word 𝐵 )
190 189 sselda ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → 𝑓 ∈ Word 𝐵 )
191 49 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐵 )
192 187 190 191 syl2anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐵 )
193 1 3 183 186 192 mulgcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ∈ 𝐵 )
194 1 108 181 182 193 ringcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ∈ 𝐵 )
195 194 anasss ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ ( 𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴 ) ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ∈ 𝐵 )
196 195 ralrimivva ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∀ 𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴 ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ∈ 𝐵 )
197 eqid ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) = ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) )
198 197 fmpo ( ∀ 𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴 ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ∈ 𝐵 ↔ ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
199 196 198 sylib ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
200 vex 𝑤 ∈ V
201 vex 𝑓 ∈ V
202 200 201 op1std ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 1st𝑎 ) = 𝑤 )
203 202 fveq2d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 𝑔 ‘ ( 1st𝑎 ) ) = ( 𝑔𝑤 ) )
204 202 oveq2d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 𝑀 Σg ( 1st𝑎 ) ) = ( 𝑀 Σg 𝑤 ) )
205 203 204 oveq12d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) = ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
206 200 201 op2ndd ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 2nd𝑎 ) = 𝑓 )
207 206 fveq2d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 𝑖 ‘ ( 2nd𝑎 ) ) = ( 𝑖𝑓 ) )
208 206 oveq2d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 𝑀 Σg ( 2nd𝑎 ) ) = ( 𝑀 Σg 𝑓 ) )
209 207 208 oveq12d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) = ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) )
210 205 209 oveq12d ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) )
211 210 mpompt ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) = ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) )
212 66 66 xpexd ( 𝜑 → ( Word 𝐴 × Word 𝐴 ) ∈ V )
213 212 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( Word 𝐴 × Word 𝐴 ) ∈ V )
214 213 mptexd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) ∈ V )
215 fvexd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 0g𝑅 ) ∈ V )
216 110 adantr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑅 ∈ Ring )
217 111 ad3antrrr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑅 ∈ Grp )
218 118 ad2antrr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
219 xp1st ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) → ( 1st𝑎 ) ∈ Word 𝐴 )
220 219 adantl ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 1st𝑎 ) ∈ Word 𝐴 )
221 218 220 ffvelcdmd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑔 ‘ ( 1st𝑎 ) ) ∈ ℤ )
222 216 44 syl ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑀 ∈ Mnd )
223 188 ad2antrr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → Word 𝐴 ⊆ Word 𝐵 )
224 223 220 sseldd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 1st𝑎 ) ∈ Word 𝐵 )
225 49 gsumwcl ( ( 𝑀 ∈ Mnd ∧ ( 1st𝑎 ) ∈ Word 𝐵 ) → ( 𝑀 Σg ( 1st𝑎 ) ) ∈ 𝐵 )
226 222 224 225 syl2anc ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑀 Σg ( 1st𝑎 ) ) ∈ 𝐵 )
227 1 3 217 221 226 mulgcld ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ∈ 𝐵 )
228 184 adantr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑖 : Word 𝐴 ⟶ ℤ )
229 xp2nd ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) → ( 2nd𝑎 ) ∈ Word 𝐴 )
230 229 adantl ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 2nd𝑎 ) ∈ Word 𝐴 )
231 228 230 ffvelcdmd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑖 ‘ ( 2nd𝑎 ) ) ∈ ℤ )
232 223 230 sseldd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 2nd𝑎 ) ∈ Word 𝐵 )
233 49 gsumwcl ( ( 𝑀 ∈ Mnd ∧ ( 2nd𝑎 ) ∈ Word 𝐵 ) → ( 𝑀 Σg ( 2nd𝑎 ) ) ∈ 𝐵 )
234 222 232 233 syl2anc ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑀 Σg ( 2nd𝑎 ) ) ∈ 𝐵 )
235 1 3 217 231 234 mulgcld ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ∈ 𝐵 )
236 1 108 216 227 235 ringcld ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ∈ 𝐵 )
237 236 fmpttd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
238 237 ffund ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → Fun ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) )
239 159 fsuppimpd ( ( 𝜑𝑔𝐹 ) → ( 𝑔 supp 0 ) ∈ Fin )
240 133 simprbi ( 𝑖𝐹𝑖 finSupp 0 )
241 240 adantl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 finSupp 0 )
242 241 fsuppimpd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑖 supp 0 ) ∈ Fin )
243 xpfi ( ( ( 𝑔 supp 0 ) ∈ Fin ∧ ( 𝑖 supp 0 ) ∈ Fin ) → ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ∈ Fin )
244 239 242 243 syl2an2r ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ∈ Fin )
245 118 ffnd ( ( 𝜑𝑔𝐹 ) → 𝑔 Fn Word 𝐴 )
246 245 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 Fn Word 𝐴 )
247 246 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → 𝑔 Fn Word 𝐴 )
248 109 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → Word 𝐴 ∈ V )
249 0zd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → 0 ∈ ℤ )
250 xp1st ( 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) → ( 1st𝑎 ) ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) )
251 250 adantl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 1st𝑎 ) ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) )
252 247 248 249 251 fvdifsupp ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 𝑔 ‘ ( 1st𝑎 ) ) = 0 )
253 252 oveq1d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) = ( 0 · ( 𝑀 Σg ( 1st𝑎 ) ) ) )
254 45 ad4antr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → 𝑀 ∈ Mnd )
255 188 ad3antrrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → Word 𝐴 ⊆ Word 𝐵 )
256 251 eldifad ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 1st𝑎 ) ∈ Word 𝐴 )
257 255 256 sseldd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 1st𝑎 ) ∈ Word 𝐵 )
258 254 257 225 syl2anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 𝑀 Σg ( 1st𝑎 ) ) ∈ 𝐵 )
259 1 52 3 mulg0 ( ( 𝑀 Σg ( 1st𝑎 ) ) ∈ 𝐵 → ( 0 · ( 𝑀 Σg ( 1st𝑎 ) ) ) = ( 0g𝑅 ) )
260 258 259 syl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 0 · ( 𝑀 Σg ( 1st𝑎 ) ) ) = ( 0g𝑅 ) )
261 253 260 eqtrd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) = ( 0g𝑅 ) )
262 261 oveq1d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( ( 0g𝑅 ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) )
263 110 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → 𝑅 ∈ Ring )
264 111 ad4antr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → 𝑅 ∈ Grp )
265 184 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → 𝑖 : Word 𝐴 ⟶ ℤ )
266 xp2nd ( 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) → ( 2nd𝑎 ) ∈ Word 𝐴 )
267 266 adantl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 2nd𝑎 ) ∈ Word 𝐴 )
268 265 267 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 𝑖 ‘ ( 2nd𝑎 ) ) ∈ ℤ )
269 255 267 sseldd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 2nd𝑎 ) ∈ Word 𝐵 )
270 254 269 233 syl2anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( 𝑀 Σg ( 2nd𝑎 ) ) ∈ 𝐵 )
271 1 3 264 268 270 mulgcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ∈ 𝐵 )
272 1 108 52 263 271 ringlzd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( ( 0g𝑅 ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( 0g𝑅 ) )
273 262 272 eqtrd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( 0g𝑅 ) )
274 138 ffnd ( ( 𝜑𝑖𝐹 ) → 𝑖 Fn Word 𝐴 )
275 274 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 Fn Word 𝐴 )
276 275 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → 𝑖 Fn Word 𝐴 )
277 109 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → Word 𝐴 ∈ V )
278 0zd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → 0 ∈ ℤ )
279 xp2nd ( 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) → ( 2nd𝑎 ) ∈ ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) )
280 279 adantl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 2nd𝑎 ) ∈ ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) )
281 276 277 278 280 fvdifsupp ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 𝑖 ‘ ( 2nd𝑎 ) ) = 0 )
282 281 oveq1d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) = ( 0 · ( 𝑀 Σg ( 2nd𝑎 ) ) ) )
283 45 ad4antr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → 𝑀 ∈ Mnd )
284 188 ad3antrrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → Word 𝐴 ⊆ Word 𝐵 )
285 280 eldifad ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 2nd𝑎 ) ∈ Word 𝐴 )
286 284 285 sseldd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 2nd𝑎 ) ∈ Word 𝐵 )
287 283 286 233 syl2anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 𝑀 Σg ( 2nd𝑎 ) ) ∈ 𝐵 )
288 1 52 3 mulg0 ( ( 𝑀 Σg ( 2nd𝑎 ) ) ∈ 𝐵 → ( 0 · ( 𝑀 Σg ( 2nd𝑎 ) ) ) = ( 0g𝑅 ) )
289 287 288 syl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 0 · ( 𝑀 Σg ( 2nd𝑎 ) ) ) = ( 0g𝑅 ) )
290 282 289 eqtrd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) = ( 0g𝑅 ) )
291 290 oveq2d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( 0g𝑅 ) ) )
292 110 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → 𝑅 ∈ Ring )
293 111 ad4antr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → 𝑅 ∈ Grp )
294 118 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
295 294 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
296 xp1st ( 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) → ( 1st𝑎 ) ∈ Word 𝐴 )
297 296 adantl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 1st𝑎 ) ∈ Word 𝐴 )
298 295 297 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 𝑔 ‘ ( 1st𝑎 ) ) ∈ ℤ )
299 284 297 sseldd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 1st𝑎 ) ∈ Word 𝐵 )
300 283 299 225 syl2anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( 𝑀 Σg ( 1st𝑎 ) ) ∈ 𝐵 )
301 1 3 293 298 300 mulgcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ∈ 𝐵 )
302 1 108 52 292 301 ringrzd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( 0g𝑅 ) ) = ( 0g𝑅 ) )
303 291 302 eqtrd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ∧ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( 0g𝑅 ) )
304 simpr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) → 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) )
305 difxp ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) = ( ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ∪ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) )
306 304 305 eleqtrdi ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) → 𝑎 ∈ ( ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ∪ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) )
307 elun ( 𝑎 ∈ ( ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ∪ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) ↔ ( 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ∨ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) )
308 306 307 sylib ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) → ( 𝑎 ∈ ( ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) × Word 𝐴 ) ∨ 𝑎 ∈ ( Word 𝐴 × ( Word 𝐴 ∖ ( 𝑖 supp 0 ) ) ) ) )
309 273 303 308 mpjaodan ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑎 ∈ ( ( Word 𝐴 × Word 𝐴 ) ∖ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) → ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) = ( 0g𝑅 ) )
310 309 213 suppss2 ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) supp ( 0g𝑅 ) ) ⊆ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) )
311 244 310 ssfid ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) supp ( 0g𝑅 ) ) ∈ Fin )
312 214 215 238 311 isfsuppd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( ( ( 𝑔 ‘ ( 1st𝑎 ) ) · ( 𝑀 Σg ( 1st𝑎 ) ) ) ( .r𝑅 ) ( ( 𝑖 ‘ ( 2nd𝑎 ) ) · ( 𝑀 Σg ( 2nd𝑎 ) ) ) ) ) finSupp ( 0g𝑅 ) )
313 211 312 eqbrtrrid ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) finSupp ( 0g𝑅 ) )
314 60 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑅 ∈ CMnd )
315 7 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝐴𝐵 )
316 1 52 199 313 314 315 gsumwrd2dccat ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) ) ) ) ) )
317 126 oveq1d ( 𝑢 = 𝑤 → ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) )
318 fveq2 ( 𝑣 = 𝑓 → ( 𝑖𝑣 ) = ( 𝑖𝑓 ) )
319 oveq2 ( 𝑣 = 𝑓 → ( 𝑀 Σg 𝑣 ) = ( 𝑀 Σg 𝑓 ) )
320 318 319 oveq12d ( 𝑣 = 𝑓 → ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) = ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) )
321 320 oveq2d ( 𝑣 = 𝑓 → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) )
322 317 321 cbvmpov ( 𝑢 ∈ Word 𝐴 , 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) )
323 322 oveq2i ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 , 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) )
324 323 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 , 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ) )
325 pfxcctswrd ( ( 𝑣 ∈ Word 𝐴𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) = 𝑣 )
326 325 adantll ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) = 𝑣 )
327 326 oveq2d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) = ( 𝑀 Σg 𝑣 ) )
328 327 oveq2d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) = ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) )
329 328 mpteq2dva ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) ) = ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) ) )
330 329 oveq2d ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
331 df-ov ( ( 𝑣 prefix 𝑗 ) ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) = ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ )
332 188 sselda ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
333 332 ad4ant13 ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
334 187 333 50 syl2anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
335 1 3 108 mulgass3 ( ( 𝑅 ∈ Ring ∧ ( ( 𝑖𝑓 ) ∈ ℤ ∧ ( 𝑀 Σg 𝑤 ) ∈ 𝐵 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐵 ) ) → ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( 𝑖𝑓 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) )
336 181 186 334 192 335 syl13anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( 𝑖𝑓 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) )
337 336 oveq2d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) = ( ( 𝑔𝑤 ) · ( ( 𝑖𝑓 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) ) )
338 119 ad4ant13 ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) ∈ ℤ )
339 1 3 108 mulgass2 ( ( 𝑅 ∈ Ring ∧ ( ( 𝑔𝑤 ) ∈ ℤ ∧ ( 𝑀 Σg 𝑤 ) ∈ 𝐵 ∧ ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ∈ 𝐵 ) ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( 𝑔𝑤 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) )
340 181 338 334 193 339 syl13anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( 𝑔𝑤 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) )
341 1 108 181 334 192 ringcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ∈ 𝐵 )
342 1 3 mulgass ( ( 𝑅 ∈ Grp ∧ ( ( 𝑔𝑤 ) ∈ ℤ ∧ ( 𝑖𝑓 ) ∈ ℤ ∧ ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ∈ 𝐵 ) ) → ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) = ( ( 𝑔𝑤 ) · ( ( 𝑖𝑓 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) ) )
343 183 338 186 341 342 syl13anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) = ( ( 𝑔𝑤 ) · ( ( 𝑖𝑓 ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) ) )
344 337 340 343 3eqtr4d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) )
345 2 108 mgpplusg ( .r𝑅 ) = ( +g𝑀 )
346 49 345 gsumccat ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵𝑓 ∈ Word 𝐵 ) → ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) = ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) )
347 187 333 190 346 syl3anc ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) = ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) )
348 347 oveq2d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( ( 𝑀 Σg 𝑤 ) ( .r𝑅 ) ( 𝑀 Σg 𝑓 ) ) ) )
349 344 348 eqtr4d ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) )
350 349 adantllr ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) )
351 350 adantllr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) )
352 351 3impa ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) ∧ 𝑤 ∈ Word 𝐴𝑓 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) )
353 352 mpoeq3dva ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) = ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) ) )
354 fveq2 ( 𝑤 = ( 𝑣 prefix 𝑗 ) → ( 𝑔𝑤 ) = ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) )
355 fveq2 ( 𝑓 = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) → ( 𝑖𝑓 ) = ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) )
356 354 355 oveqan12d ( ( 𝑤 = ( 𝑣 prefix 𝑗 ) ∧ 𝑓 = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) → ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) = ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) )
357 oveq12 ( ( 𝑤 = ( 𝑣 prefix 𝑗 ) ∧ 𝑓 = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) → ( 𝑤 ++ 𝑓 ) = ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) )
358 357 oveq2d ( ( 𝑤 = ( 𝑣 prefix 𝑗 ) ∧ 𝑓 = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) → ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) = ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) )
359 356 358 oveq12d ( ( 𝑤 = ( 𝑣 prefix 𝑗 ) ∧ 𝑓 = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) → ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) = ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) )
360 359 adantl ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) ∧ ( 𝑤 = ( 𝑣 prefix 𝑗 ) ∧ 𝑓 = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) → ( ( ( 𝑔𝑤 ) · ( 𝑖𝑓 ) ) · ( 𝑀 Σg ( 𝑤 ++ 𝑓 ) ) ) = ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) )
361 pfxcl ( 𝑣 ∈ Word 𝐴 → ( 𝑣 prefix 𝑗 ) ∈ Word 𝐴 )
362 361 ad2antlr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( 𝑣 prefix 𝑗 ) ∈ Word 𝐴 )
363 swrdcl ( 𝑣 ∈ Word 𝐴 → ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ∈ Word 𝐴 )
364 363 ad2antlr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ∈ Word 𝐴 )
365 ovexd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) ∈ V )
366 353 360 362 364 365 ovmpod ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( 𝑣 prefix 𝑗 ) ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) = ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) )
367 331 366 eqtr3id ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) = ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) )
368 367 mpteq2dva ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) ) = ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) ) )
369 368 oveq2d ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg ( ( 𝑣 prefix 𝑗 ) ++ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ) ) ) )
370 eqid ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) = ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) )
371 fveq2 ( 𝑡 = 𝑣 → ( ♯ ‘ 𝑡 ) = ( ♯ ‘ 𝑣 ) )
372 371 oveq2d ( 𝑡 = 𝑣 → ( 0 ... ( ♯ ‘ 𝑡 ) ) = ( 0 ... ( ♯ ‘ 𝑣 ) ) )
373 fvoveq1 ( 𝑡 = 𝑣 → ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) = ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) )
374 id ( 𝑡 = 𝑣𝑡 = 𝑣 )
375 371 opeq2d ( 𝑡 = 𝑣 → ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ = ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ )
376 374 375 oveq12d ( 𝑡 = 𝑣 → ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) = ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) )
377 376 fveq2d ( 𝑡 = 𝑣 → ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) = ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) )
378 373 377 oveq12d ( 𝑡 = 𝑣 → ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) )
379 378 adantr ( ( 𝑡 = 𝑣𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) )
380 372 379 sumeq12dv ( 𝑡 = 𝑣 → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) )
381 simpr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → 𝑣 ∈ Word 𝐴 )
382 fzfid ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 0 ... ( ♯ ‘ 𝑣 ) ) ∈ Fin )
383 294 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
384 383 362 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) ∈ ℤ )
385 184 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → 𝑖 : Word 𝐴 ⟶ ℤ )
386 385 364 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ∈ ℤ )
387 384 386 zmulcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ∈ ℤ )
388 387 zcnd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ) → ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ∈ ℂ )
389 382 388 fsumcl ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) ∈ ℂ )
390 370 380 381 389 fvmptd3 ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) = Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) )
391 390 oveq1d ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) = ( Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) )
392 111 ad3antrrr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
393 45 ad3antrrr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → 𝑀 ∈ Mnd )
394 315 46 syl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → Word 𝐴 ⊆ Word 𝐵 )
395 394 sselda ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → 𝑣 ∈ Word 𝐵 )
396 49 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑣 ) ∈ 𝐵 )
397 393 395 396 syl2anc ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑣 ) ∈ 𝐵 )
398 1 3 392 382 397 387 gsummulgc2 ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) )
399 391 398 eqtr4d ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( ( 𝑔 ‘ ( 𝑣 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ) ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
400 330 369 399 3eqtr4rd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) ) ) )
401 400 mpteq2dva ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) ) ) ) )
402 401 oveq2d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) ↦ ( ( 𝑤 ∈ Word 𝐴 , 𝑓 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( .r𝑅 ) ( ( 𝑖𝑓 ) · ( 𝑀 Σg 𝑓 ) ) ) ) ‘ ⟨ ( 𝑣 prefix 𝑗 ) , ( 𝑣 substr ⟨ 𝑗 , ( ♯ ‘ 𝑣 ) ⟩ ) ⟩ ) ) ) ) ) )
403 316 324 402 3eqtr4d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑢 ∈ Word 𝐴 , 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑢 ) · ( 𝑀 Σg 𝑢 ) ) ( .r𝑅 ) ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
404 176 180 403 3eqtr3d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
405 fveq1 ( 𝑔 = → ( 𝑔𝑤 ) = ( 𝑤 ) )
406 405 oveq1d ( 𝑔 = → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
407 406 mpteq2dv ( 𝑔 = → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
408 407 oveq2d ( 𝑔 = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
409 408 cbvmptv ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
410 fveq1 ( = ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) → ( 𝑤 ) = ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) )
411 410 oveq1d ( = ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) → ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
412 411 mpteq2dv ( = ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
413 412 oveq2d ( = ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
414 413 eqeq2d ( = ( 𝑡 ∈ 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 ( 𝑓 = ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) → ( 𝑓 finSupp 0 ↔ ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) finSupp 0 ) )
416 78 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ℤ ∈ V )
417 fzfid ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) → ( 0 ... ( ♯ ‘ 𝑡 ) ) ∈ Fin )
418 294 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
419 pfxcl ( 𝑡 ∈ Word 𝐴 → ( 𝑡 prefix 𝑗 ) ∈ Word 𝐴 )
420 419 ad2antlr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( 𝑡 prefix 𝑗 ) ∈ Word 𝐴 )
421 418 420 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) ∈ ℤ )
422 184 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → 𝑖 : Word 𝐴 ⟶ ℤ )
423 swrdcl ( 𝑡 ∈ Word 𝐴 → ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ∈ Word 𝐴 )
424 423 ad2antlr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ∈ Word 𝐴 )
425 422 424 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ∈ ℤ )
426 421 425 zmulcld ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ∈ ℤ )
427 417 426 fsumzcl ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑡 ∈ Word 𝐴 ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ∈ ℤ )
428 427 fmpttd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) : Word 𝐴 ⟶ ℤ )
429 416 109 428 elmapdd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ∈ ( ℤ ↑m Word 𝐴 ) )
430 0zd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 0 ∈ ℤ )
431 428 ffund ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → Fun ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) )
432 ccatfn ++ Fn ( V × V )
433 fnfun ( ++ Fn ( V × V ) → Fun ++ )
434 432 433 ax-mp Fun ++
435 imafi ( ( Fun ++ ∧ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ∈ Fin ) → ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ∈ Fin )
436 434 244 435 sylancr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ∈ Fin )
437 fveq2 ( 𝑡 = 𝑤 → ( ♯ ‘ 𝑡 ) = ( ♯ ‘ 𝑤 ) )
438 437 oveq2d ( 𝑡 = 𝑤 → ( 0 ... ( ♯ ‘ 𝑡 ) ) = ( 0 ... ( ♯ ‘ 𝑤 ) ) )
439 fvoveq1 ( 𝑡 = 𝑤 → ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) = ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) )
440 id ( 𝑡 = 𝑤𝑡 = 𝑤 )
441 437 opeq2d ( 𝑡 = 𝑤 → ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ = ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ )
442 440 441 oveq12d ( 𝑡 = 𝑤 → ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) = ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) )
443 442 fveq2d ( 𝑡 = 𝑤 → ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) = ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) )
444 439 443 oveq12d ( 𝑡 = 𝑤 → ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) )
445 444 adantr ( ( 𝑡 = 𝑤𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ) → ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) )
446 438 445 sumeq12dv ( 𝑡 = 𝑤 → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) )
447 oveq1 ( 𝑢 = ( 𝑤 prefix 𝑗 ) → ( 𝑢 ++ 𝑣 ) = ( ( 𝑤 prefix 𝑗 ) ++ 𝑣 ) )
448 447 eqeq2d ( 𝑢 = ( 𝑤 prefix 𝑗 ) → ( 𝑤 = ( 𝑢 ++ 𝑣 ) ↔ 𝑤 = ( ( 𝑤 prefix 𝑗 ) ++ 𝑣 ) ) )
449 oveq2 ( 𝑣 = ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) → ( ( 𝑤 prefix 𝑗 ) ++ 𝑣 ) = ( ( 𝑤 prefix 𝑗 ) ++ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) )
450 449 eqeq2d ( 𝑣 = ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) → ( 𝑤 = ( ( 𝑤 prefix 𝑗 ) ++ 𝑣 ) ↔ 𝑤 = ( ( 𝑤 prefix 𝑗 ) ++ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) )
451 246 ad4antr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑔 Fn Word 𝐴 )
452 109 ad4antr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → Word 𝐴 ∈ V )
453 0zd ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 0 ∈ ℤ )
454 simpr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) )
455 454 eldifad ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → 𝑤 ∈ Word 𝐴 )
456 455 adantr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → 𝑤 ∈ Word 𝐴 )
457 pfxcl ( 𝑤 ∈ Word 𝐴 → ( 𝑤 prefix 𝑗 ) ∈ Word 𝐴 )
458 456 457 syl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑤 prefix 𝑗 ) ∈ Word 𝐴 )
459 458 ad2antrr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( 𝑤 prefix 𝑗 ) ∈ Word 𝐴 )
460 simplr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 )
461 451 452 453 459 460 elsuppfnd ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( 𝑤 prefix 𝑗 ) ∈ ( 𝑔 supp 0 ) )
462 275 ad4antr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑖 Fn Word 𝐴 )
463 swrdcl ( 𝑤 ∈ Word 𝐴 → ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ∈ Word 𝐴 )
464 456 463 syl ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ∈ Word 𝐴 )
465 464 ad2antrr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ∈ Word 𝐴 )
466 simpr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 )
467 462 452 453 465 466 elsuppfnd ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ∈ ( 𝑖 supp 0 ) )
468 456 ad2antrr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑤 ∈ Word 𝐴 )
469 simpllr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) )
470 pfxcctswrd ( ( 𝑤 ∈ Word 𝐴𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑤 prefix 𝑗 ) ++ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 𝑤 )
471 468 469 470 syl2anc ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ( ( 𝑤 prefix 𝑗 ) ++ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 𝑤 )
472 471 eqcomd ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑤 = ( ( 𝑤 prefix 𝑗 ) ++ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) )
473 448 450 461 467 472 2rspcedvdw ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ∃ 𝑢 ∈ ( 𝑔 supp 0 ) ∃ 𝑣 ∈ ( 𝑖 supp 0 ) 𝑤 = ( 𝑢 ++ 𝑣 ) )
474 fnov ( ++ Fn ( V × V ) ↔ ++ = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑢 ++ 𝑣 ) ) )
475 432 474 mpbi ++ = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑢 ++ 𝑣 ) )
476 200 a1i ( ⊤ → 𝑤 ∈ V )
477 ssv ( 𝑔 supp 0 ) ⊆ V
478 477 a1i ( ⊤ → ( 𝑔 supp 0 ) ⊆ V )
479 ssv ( 𝑖 supp 0 ) ⊆ V
480 479 a1i ( ⊤ → ( 𝑖 supp 0 ) ⊆ V )
481 475 476 478 480 elimampo ( ⊤ → ( 𝑤 ∈ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑔 supp 0 ) ∃ 𝑣 ∈ ( 𝑖 supp 0 ) 𝑤 = ( 𝑢 ++ 𝑣 ) ) )
482 481 mptru ( 𝑤 ∈ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑔 supp 0 ) ∃ 𝑣 ∈ ( 𝑖 supp 0 ) 𝑤 = ( 𝑢 ++ 𝑣 ) )
483 473 482 sylibr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑤 ∈ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) )
484 483 anasss ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) ) → 𝑤 ∈ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) )
485 454 ad3antrrr ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) )
486 485 eldifbd ( ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ) ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) → ¬ 𝑤 ∈ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) )
487 486 anasss ( ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) ) → ¬ 𝑤 ∈ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) )
488 484 487 pm2.65da ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ¬ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) )
489 df-ne ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ↔ ¬ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 )
490 df-ne ( ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ↔ ¬ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 )
491 489 490 anbi12i ( ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) ↔ ( ¬ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∧ ¬ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) )
492 491 notbii ( ¬ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) ↔ ¬ ( ¬ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∧ ¬ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) )
493 pm4.57 ( ¬ ( ¬ ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∧ ¬ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) ↔ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∨ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) )
494 492 493 bitr2i ( ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∨ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) ↔ ¬ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ≠ 0 ∧ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ≠ 0 ) )
495 488 494 sylibr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∨ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) )
496 294 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
497 496 458 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ∈ ℤ )
498 497 zcnd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) ∈ ℂ )
499 184 ad2antrr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → 𝑖 : Word 𝐴 ⟶ ℤ )
500 499 464 ffvelcdmd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ∈ ℤ )
501 500 zcnd ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ∈ ℂ )
502 498 501 mul0ord ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) = 0 ↔ ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) = 0 ∨ ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) = 0 ) ) )
503 495 502 mpbird ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) = 0 )
504 503 sumeq2dv ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) = Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 0 )
505 fzssuz ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ( ℤ ‘ 0 )
506 sumz ( ( ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ( ℤ ‘ 0 ) ∨ ( 0 ... ( ♯ ‘ 𝑤 ) ) ∈ Fin ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 0 = 0 )
507 506 orcs ( ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ( ℤ ‘ 0 ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 0 = 0 )
508 505 507 mp1i ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 0 = 0 )
509 504 508 eqtrd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ( ( 𝑔 ‘ ( 𝑤 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ) ) = 0 )
510 446 509 sylan9eqr ( ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) ∧ 𝑡 = 𝑤 ) → Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) = 0 )
511 0zd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → 0 ∈ ℤ )
512 370 510 455 511 fvmptd2 ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) ) ) → ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) = 0 )
513 428 512 suppss ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) supp 0 ) ⊆ ( ++ “ ( ( 𝑔 supp 0 ) × ( 𝑖 supp 0 ) ) ) )
514 436 513 ssfid ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) supp 0 ) ∈ Fin )
515 429 430 431 514 isfsuppd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) finSupp 0 )
516 415 429 515 elrabd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
517 516 5 eleqtrrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ∈ 𝐹 )
518 fveq2 ( 𝑣 = 𝑤 → ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) = ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) )
519 518 145 oveq12d ( 𝑣 = 𝑤 → ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) = ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
520 519 cbvmptv ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
521 520 oveq2i ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
522 521 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
523 414 517 522 rspcedvdw ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∃ 𝐹 ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
524 ovexd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ∈ V )
525 409 523 524 elrnmptd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
526 525 8 eleqtrrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( ( 𝑡 ∈ Word 𝐴 ↦ Σ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑡 ) ) ( ( 𝑔 ‘ ( 𝑡 prefix 𝑗 ) ) · ( 𝑖 ‘ ( 𝑡 substr ⟨ 𝑗 , ( ♯ ‘ 𝑡 ) ⟩ ) ) ) ) ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) ∈ 𝑆 )
527 404 526 eqeltrd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
528 527 adantllr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
529 528 adantllr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
530 529 adantlr ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
531 530 adantr ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
532 107 531 eqeltrd ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 )
533 8 eleq2i ( 𝑦𝑆𝑦 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
534 169 oveq2d ( 𝑔 = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
535 534 cbvmptv ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑖𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
536 535 elrnmpt ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
537 536 elv ( 𝑦 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
538 533 537 sylbb ( 𝑦𝑆 → ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
539 538 adantl ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
540 539 ad2antrr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
541 532 540 r19.29a ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 )
542 8 eleq2i ( 𝑥𝑆𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
543 71 elrnmpt ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
544 543 elv ( 𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
545 542 544 sylbb ( 𝑥𝑆 → ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
546 545 ad2antlr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
547 541 546 r19.29a ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 )
548 547 anasss ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 )
549 548 ralrimivva ( 𝜑 → ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 )
550 1 24 108 issubrg2 ( 𝑅 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
551 550 biimpar ( ( 𝑅 ∈ Ring ∧ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
552 6 9 104 549 551 syl13anc ( 𝜑𝑆 ∈ ( SubRing ‘ 𝑅 ) )