This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 ) )