Metamath Proof Explorer


Theorem elrgspnlem1

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 elrgspnlem1 ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝑅 ) )

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 6 ringgrpd ( 𝜑𝑅 ∈ Grp )
10 simpr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
11 eqid ( 0g𝑅 ) = ( 0g𝑅 )
12 6 ringcmnd ( 𝜑𝑅 ∈ CMnd )
13 12 adantr ( ( 𝜑𝑔𝐹 ) → 𝑅 ∈ CMnd )
14 1 fvexi 𝐵 ∈ V
15 14 a1i ( 𝜑𝐵 ∈ V )
16 15 7 ssexd ( 𝜑𝐴 ∈ V )
17 wrdexg ( 𝐴 ∈ V → Word 𝐴 ∈ V )
18 16 17 syl ( 𝜑 → Word 𝐴 ∈ V )
19 18 adantr ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ∈ V )
20 9 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
21 5 ssrab3 𝐹 ⊆ ( ℤ ↑m Word 𝐴 )
22 21 a1i ( 𝜑𝐹 ⊆ ( ℤ ↑m Word 𝐴 ) )
23 22 sselda ( ( 𝜑𝑔𝐹 ) → 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
24 zex ℤ ∈ V
25 24 a1i ( 𝜑 → ℤ ∈ V )
26 25 18 elmapd ( 𝜑 → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑔 : Word 𝐴 ⟶ ℤ ) )
27 26 adantr ( ( 𝜑𝑔𝐹 ) → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑔 : Word 𝐴 ⟶ ℤ ) )
28 23 27 mpbid ( ( 𝜑𝑔𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
29 28 ffvelcdmda ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) ∈ ℤ )
30 2 ringmgp ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
31 6 30 syl ( 𝜑𝑀 ∈ Mnd )
32 sswrd ( 𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵 )
33 7 32 syl ( 𝜑 → Word 𝐴 ⊆ Word 𝐵 )
34 33 sselda ( ( 𝜑𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
35 2 1 mgpbas 𝐵 = ( Base ‘ 𝑀 )
36 35 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
37 31 34 36 syl2an2r ( ( 𝜑𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
38 37 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
39 1 3 20 29 38 mulgcld ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
40 39 fmpttd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) : Word 𝐴𝐵 )
41 fvexd ( ( 𝜑𝑔𝐹 ) → ( 0g𝑅 ) ∈ V )
42 0zd ( ( 𝜑𝑔𝐹 ) → 0 ∈ ℤ )
43 ssidd ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ⊆ Word 𝐴 )
44 breq1 ( 𝑓 = 𝑔 → ( 𝑓 finSupp 0 ↔ 𝑔 finSupp 0 ) )
45 44 5 elrab2 ( 𝑔𝐹 ↔ ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
46 45 simprbi ( 𝑔𝐹𝑔 finSupp 0 )
47 46 adantl ( ( 𝜑𝑔𝐹 ) → 𝑔 finSupp 0 )
48 1 11 3 mulg0 ( 𝑦𝐵 → ( 0 · 𝑦 ) = ( 0g𝑅 ) )
49 48 adantl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑦𝐵 ) → ( 0 · 𝑦 ) = ( 0g𝑅 ) )
50 41 42 19 43 38 28 47 49 fisuppov1 ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
51 1 11 13 19 40 50 gsumcl ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
52 51 ad4ant13 ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
53 10 52 eqeltrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑥𝐵 )
54 8 eleq2i ( 𝑥𝑆𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
55 eqid ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
56 55 elrnmpt ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
57 56 elv ( 𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
58 54 57 sylbb ( 𝑥𝑆 → ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
59 58 adantl ( ( 𝜑𝑥𝑆 ) → ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
60 53 59 r19.29a ( ( 𝜑𝑥𝑆 ) → 𝑥𝐵 )
61 60 1 eleqtrdi ( ( 𝜑𝑥𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
62 61 ex ( 𝜑 → ( 𝑥𝑆𝑥 ∈ ( Base ‘ 𝑅 ) ) )
63 62 ssrdv ( 𝜑𝑆 ⊆ ( Base ‘ 𝑅 ) )
64 63 1 sseqtrrdi ( 𝜑𝑆𝐵 )
65 breq1 ( 𝑓 = ( Word 𝐴 × { 0 } ) → ( 𝑓 finSupp 0 ↔ ( Word 𝐴 × { 0 } ) finSupp 0 ) )
66 0z 0 ∈ ℤ
67 66 fconst6 ( Word 𝐴 × { 0 } ) : Word 𝐴 ⟶ ℤ
68 67 a1i ( 𝜑 → ( Word 𝐴 × { 0 } ) : Word 𝐴 ⟶ ℤ )
69 25 18 68 elmapdd ( 𝜑 → ( Word 𝐴 × { 0 } ) ∈ ( ℤ ↑m Word 𝐴 ) )
70 c0ex 0 ∈ V
71 70 a1i ( 𝜑 → 0 ∈ V )
72 18 71 fczfsuppd ( 𝜑 → ( Word 𝐴 × { 0 } ) finSupp 0 )
73 65 69 72 elrabd ( 𝜑 → ( Word 𝐴 × { 0 } ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
74 73 5 eleqtrrdi ( 𝜑 → ( Word 𝐴 × { 0 } ) ∈ 𝐹 )
75 simplr ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑔 = ( Word 𝐴 × { 0 } ) )
76 75 fveq1d ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) = ( ( Word 𝐴 × { 0 } ) ‘ 𝑤 ) )
77 70 fconst ( Word 𝐴 × { 0 } ) : Word 𝐴 ⟶ { 0 }
78 77 a1i ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( Word 𝐴 × { 0 } ) : Word 𝐴 ⟶ { 0 } )
79 simpr ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐴 )
80 fvconst ( ( ( Word 𝐴 × { 0 } ) : Word 𝐴 ⟶ { 0 } ∧ 𝑤 ∈ Word 𝐴 ) → ( ( Word 𝐴 × { 0 } ) ‘ 𝑤 ) = 0 )
81 78 79 80 syl2anc ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( Word 𝐴 × { 0 } ) ‘ 𝑤 ) = 0 )
82 76 81 eqtrd ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) = 0 )
83 82 oveq1d ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
84 37 adantlr ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
85 1 11 3 mulg0 ( ( 𝑀 Σg 𝑤 ) ∈ 𝐵 → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
86 84 85 syl ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
87 83 86 eqtrd ( ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
88 87 mpteq2dva ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) )
89 88 oveq2d ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) ) )
90 12 cmnmndd ( 𝜑𝑅 ∈ Mnd )
91 11 gsumz ( ( 𝑅 ∈ Mnd ∧ Word 𝐴 ∈ V ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) ) = ( 0g𝑅 ) )
92 90 18 91 syl2anc ( 𝜑 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) ) = ( 0g𝑅 ) )
93 92 adantr ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) ) = ( 0g𝑅 ) )
94 89 93 eqtrd ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 0g𝑅 ) )
95 94 eqeq2d ( ( 𝜑𝑔 = ( Word 𝐴 × { 0 } ) ) → ( ( 0g𝑅 ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ↔ ( 0g𝑅 ) = ( 0g𝑅 ) ) )
96 eqidd ( 𝜑 → ( 0g𝑅 ) = ( 0g𝑅 ) )
97 74 95 96 rspcedvd ( 𝜑 → ∃ 𝑔𝐹 ( 0g𝑅 ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
98 fvexd ( 𝜑 → ( 0g𝑅 ) ∈ V )
99 55 97 98 elrnmptd ( 𝜑 → ( 0g𝑅 ) ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
100 99 8 eleqtrrdi ( 𝜑 → ( 0g𝑅 ) ∈ 𝑆 )
101 100 ne0d ( 𝜑𝑆 ≠ ∅ )
102 simpllr ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
103 simpr ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
104 102 103 oveq12d ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
105 eqid ( +g𝑅 ) = ( +g𝑅 )
106 13 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑅 ∈ CMnd )
107 19 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → Word 𝐴 ∈ V )
108 39 adantlr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
109 9 ad2antrr ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
110 breq1 ( 𝑓 = 𝑖 → ( 𝑓 finSupp 0 ↔ 𝑖 finSupp 0 ) )
111 110 5 elrab2 ( 𝑖𝐹 ↔ ( 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑖 finSupp 0 ) )
112 111 simplbi ( 𝑖𝐹𝑖 ∈ ( ℤ ↑m Word 𝐴 ) )
113 112 adantl ( ( 𝜑𝑖𝐹 ) → 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) )
114 25 18 elmapd ( 𝜑 → ( 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑖 : Word 𝐴 ⟶ ℤ ) )
115 114 adantr ( ( 𝜑𝑖𝐹 ) → ( 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑖 : Word 𝐴 ⟶ ℤ ) )
116 113 115 mpbid ( ( 𝜑𝑖𝐹 ) → 𝑖 : Word 𝐴 ⟶ ℤ )
117 116 ffvelcdmda ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑖𝑤 ) ∈ ℤ )
118 37 adantlr ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
119 1 3 109 117 118 mulgcld ( ( ( 𝜑𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
120 119 adantllr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
121 eqidd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
122 eqidd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
123 50 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
124 50 ralrimiva ( 𝜑 → ∀ 𝑔𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
125 fveq1 ( 𝑔 = 𝑖 → ( 𝑔𝑤 ) = ( 𝑖𝑤 ) )
126 125 oveq1d ( 𝑔 = 𝑖 → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
127 126 mpteq2dv ( 𝑔 = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
128 127 breq1d ( 𝑔 = 𝑖 → ( ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) ↔ ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) ) )
129 128 cbvralvw ( ∀ 𝑔𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) ↔ ∀ 𝑖𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
130 124 129 sylib ( 𝜑 → ∀ 𝑖𝐹 ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
131 130 r19.21bi ( ( 𝜑𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
132 131 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
133 1 11 105 106 107 108 120 121 122 123 132 gsummptfsadd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
134 28 ffnd ( ( 𝜑𝑔𝐹 ) → 𝑔 Fn Word 𝐴 )
135 134 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 Fn Word 𝐴 )
136 116 ffnd ( ( 𝜑𝑖𝐹 ) → 𝑖 Fn Word 𝐴 )
137 136 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 Fn Word 𝐴 )
138 inidm ( Word 𝐴 ∩ Word 𝐴 ) = Word 𝐴
139 eqidd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) = ( 𝑔𝑤 ) )
140 eqidd ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑖𝑤 ) = ( 𝑖𝑤 ) )
141 135 137 107 107 138 139 140 ofval ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) = ( ( 𝑔𝑤 ) + ( 𝑖𝑤 ) ) )
142 141 oveq1d ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑔𝑤 ) + ( 𝑖𝑤 ) ) · ( 𝑀 Σg 𝑤 ) ) )
143 20 adantlr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
144 29 adantlr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) ∈ ℤ )
145 117 adantllr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑖𝑤 ) ∈ ℤ )
146 38 adantlr ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
147 1 3 105 mulgdir ( ( 𝑅 ∈ Grp ∧ ( ( 𝑔𝑤 ) ∈ ℤ ∧ ( 𝑖𝑤 ) ∈ ℤ ∧ ( 𝑀 Σg 𝑤 ) ∈ 𝐵 ) ) → ( ( ( 𝑔𝑤 ) + ( 𝑖𝑤 ) ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
148 143 144 145 146 147 syl13anc ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) + ( 𝑖𝑤 ) ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
149 142 148 eqtr2d ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
150 149 mpteq2dva ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
151 150 oveq2d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
152 133 151 eqtr3d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
153 fveq1 ( 𝑔 = → ( 𝑔𝑤 ) = ( 𝑤 ) )
154 153 oveq1d ( 𝑔 = → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
155 154 mpteq2dv ( 𝑔 = → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
156 155 oveq2d ( 𝑔 = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
157 156 cbvmptv ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
158 fveq1 ( = ( 𝑔f + 𝑖 ) → ( 𝑤 ) = ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) )
159 158 oveq1d ( = ( 𝑔f + 𝑖 ) → ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
160 159 mpteq2dv ( = ( 𝑔f + 𝑖 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
161 160 oveq2d ( = ( 𝑔f + 𝑖 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
162 161 eqeq2d ( = ( 𝑔f + 𝑖 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ↔ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
163 breq1 ( 𝑓 = ( 𝑔f + 𝑖 ) → ( 𝑓 finSupp 0 ↔ ( 𝑔f + 𝑖 ) finSupp 0 ) )
164 24 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ℤ ∈ V )
165 zaddcl ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
166 165 adantl ( ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
167 28 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
168 116 adantlr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 : Word 𝐴 ⟶ ℤ )
169 166 167 168 107 107 138 off ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f + 𝑖 ) : Word 𝐴 ⟶ ℤ )
170 164 107 169 elmapdd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f + 𝑖 ) ∈ ( ℤ ↑m Word 𝐴 ) )
171 zringring ring ∈ Ring
172 ringmnd ( ℤring ∈ Ring → ℤring ∈ Mnd )
173 171 172 ax-mp ring ∈ Mnd
174 173 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ℤring ∈ Mnd )
175 23 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
176 112 adantl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) )
177 47 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 finSupp 0 )
178 zring0 0 = ( 0g ‘ ℤring )
179 177 178 breqtrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑔 finSupp ( 0g ‘ ℤring ) )
180 111 simprbi ( 𝑖𝐹𝑖 finSupp 0 )
181 180 adantl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 finSupp 0 )
182 181 178 breqtrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 𝑖 finSupp ( 0g ‘ ℤring ) )
183 zringbas ℤ = ( Base ‘ ℤring )
184 183 mndpfsupp ( ( ( ℤring ∈ Mnd ∧ Word 𝐴 ∈ V ) ∧ ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑖 ∈ ( ℤ ↑m Word 𝐴 ) ) ∧ ( 𝑔 finSupp ( 0g ‘ ℤring ) ∧ 𝑖 finSupp ( 0g ‘ ℤring ) ) ) → ( 𝑔f ( +g ‘ ℤring ) 𝑖 ) finSupp ( 0g ‘ ℤring ) )
185 174 107 175 176 179 182 184 syl222anc ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f ( +g ‘ ℤring ) 𝑖 ) finSupp ( 0g ‘ ℤring ) )
186 zringplusg + = ( +g ‘ ℤring )
187 186 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → + = ( +g ‘ ℤring ) )
188 187 ofeqd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∘f + = ∘f ( +g ‘ ℤring ) )
189 188 oveqd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f + 𝑖 ) = ( 𝑔f ( +g ‘ ℤring ) 𝑖 ) )
190 178 a1i ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → 0 = ( 0g ‘ ℤring ) )
191 185 189 190 3brtr4d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f + 𝑖 ) finSupp 0 )
192 163 170 191 elrabd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f + 𝑖 ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
193 192 5 eleqtrrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑔f + 𝑖 ) ∈ 𝐹 )
194 eqidd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
195 162 193 194 rspcedvdw ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ∃ 𝐹 ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
196 ovexd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ V )
197 157 195 196 elrnmptd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
198 197 8 eleqtrrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔f + 𝑖 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑆 )
199 152 198 eqeltrd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
200 199 adantllr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
201 200 adantllr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑖𝐹 ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
202 201 ad4ant13 ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∈ 𝑆 )
203 104 202 eqeltrd ( ( ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ∧ 𝑖𝐹 ) ∧ 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 )
204 8 eleq2i ( 𝑦𝑆𝑦 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
205 127 oveq2d ( 𝑔 = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
206 205 cbvmptv ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑖𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
207 206 elrnmpt ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
208 207 elv ( 𝑦 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
209 204 208 sylbb ( 𝑦𝑆 → ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
210 209 adantl ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
211 210 ad2antrr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ∃ 𝑖𝐹 𝑦 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
212 203 211 r19.29a ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 )
213 59 adantr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
214 212 213 r19.29a ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑦𝑆 ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 )
215 214 ralrimiva ( ( 𝜑𝑥𝑆 ) → ∀ 𝑦𝑆 ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 )
216 9 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑅 ∈ Grp )
217 29 znegcld ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → - ( 𝑔𝑤 ) ∈ ℤ )
218 1 3 20 217 38 mulgcld ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
219 218 fmpttd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) : Word 𝐴𝐵 )
220 28 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
221 simpr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐴 )
222 220 221 fvco3d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) ‘ 𝑤 ) = ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ‘ ( 𝑔𝑤 ) ) )
223 eqid ( 𝑧 ∈ ℤ ↦ - 𝑧 ) = ( 𝑧 ∈ ℤ ↦ - 𝑧 )
224 negeq ( 𝑧 = ( 𝑔𝑤 ) → - 𝑧 = - ( 𝑔𝑤 ) )
225 223 224 29 217 fvmptd3 ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ‘ ( 𝑔𝑤 ) ) = - ( 𝑔𝑤 ) )
226 222 225 eqtrd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) ‘ 𝑤 ) = - ( 𝑔𝑤 ) )
227 226 oveq1d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
228 227 mpteq2dva ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
229 simpr ( ( 𝜑𝑧 ∈ ℤ ) → 𝑧 ∈ ℤ )
230 229 znegcld ( ( 𝜑𝑧 ∈ ℤ ) → - 𝑧 ∈ ℤ )
231 230 fmpttd ( 𝜑 → ( 𝑧 ∈ ℤ ↦ - 𝑧 ) : ℤ ⟶ ℤ )
232 231 adantr ( ( 𝜑𝑔𝐹 ) → ( 𝑧 ∈ ℤ ↦ - 𝑧 ) : ℤ ⟶ ℤ )
233 232 28 fcod ( ( 𝜑𝑔𝐹 ) → ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) : Word 𝐴 ⟶ ℤ )
234 24 a1i ( ( 𝜑𝑔𝐹 ) → ℤ ∈ V )
235 negeq ( 𝑧 = 0 → - 𝑧 = - 0 )
236 neg0 - 0 = 0
237 235 236 eqtrdi ( 𝑧 = 0 → - 𝑧 = 0 )
238 0zd ( 𝜑 → 0 ∈ ℤ )
239 223 237 238 238 fvmptd3 ( 𝜑 → ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ‘ 0 ) = 0 )
240 239 adantr ( ( 𝜑𝑔𝐹 ) → ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ‘ 0 ) = 0 )
241 42 28 232 19 234 47 240 fsuppco2 ( ( 𝜑𝑔𝐹 ) → ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) finSupp 0 )
242 41 42 19 43 38 233 241 49 fisuppov1 ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑧 ∈ ℤ ↦ - 𝑧 ) ∘ 𝑔 ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
243 228 242 eqbrtrrd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
244 1 11 13 19 219 243 gsumcl ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
245 244 ad4ant13 ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
246 10 oveq1d ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
247 eqidd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
248 eqidd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
249 1 11 105 13 19 39 218 247 248 50 243 gsummptfsadd ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
250 249 ad4ant13 ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
251 29 zcnd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) ∈ ℂ )
252 251 negidd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) + - ( 𝑔𝑤 ) ) = 0 )
253 252 oveq1d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) + - ( 𝑔𝑤 ) ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
254 1 3 105 mulgdir ( ( 𝑅 ∈ Grp ∧ ( ( 𝑔𝑤 ) ∈ ℤ ∧ - ( 𝑔𝑤 ) ∈ ℤ ∧ ( 𝑀 Σg 𝑤 ) ∈ 𝐵 ) ) → ( ( ( 𝑔𝑤 ) + - ( 𝑔𝑤 ) ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
255 20 29 217 38 254 syl13anc ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) + - ( 𝑔𝑤 ) ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
256 38 85 syl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
257 253 255 256 3eqtr3d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 0g𝑅 ) )
258 257 mpteq2dva ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) )
259 258 oveq2d ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) ) )
260 92 adantr ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( 0g𝑅 ) ) ) = ( 0g𝑅 ) )
261 259 260 eqtrd ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 0g𝑅 ) )
262 261 ad4ant13 ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ( +g𝑅 ) ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 0g𝑅 ) )
263 246 250 262 3eqtr2d ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑥 ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 0g𝑅 ) )
264 eqid ( invg𝑅 ) = ( invg𝑅 )
265 1 105 11 264 grpinvid1 ( ( 𝑅 ∈ Grp ∧ 𝑥𝐵 ∧ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 ) → ( ( ( invg𝑅 ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ↔ ( 𝑥 ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 0g𝑅 ) ) )
266 265 biimpar ( ( ( 𝑅 ∈ Grp ∧ 𝑥𝐵 ∧ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 ) ∧ ( 𝑥 ( +g𝑅 ) ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 0g𝑅 ) ) → ( ( invg𝑅 ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
267 216 53 245 263 266 syl31anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( ( invg𝑅 ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
268 fveq1 ( = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) → ( 𝑤 ) = ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) )
269 268 oveq1d ( = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) → ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
270 269 mpteq2dv ( = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
271 270 oveq2d ( = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
272 271 eqeq2d ( = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ↔ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
273 breq1 ( 𝑓 = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) → ( 𝑓 finSupp 0 ↔ ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) finSupp 0 ) )
274 28 ffvelcdmda ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → ( 𝑔𝑣 ) ∈ ℤ )
275 274 znegcld ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ Word 𝐴 ) → - ( 𝑔𝑣 ) ∈ ℤ )
276 275 fmpttd ( ( 𝜑𝑔𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) : Word 𝐴 ⟶ ℤ )
277 234 19 276 elmapdd ( ( 𝜑𝑔𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ∈ ( ℤ ↑m Word 𝐴 ) )
278 276 ffund ( ( 𝜑𝑔𝐹 ) → Fun ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) )
279 134 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → 𝑔 Fn Word 𝐴 )
280 19 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → Word 𝐴 ∈ V )
281 0zd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → 0 ∈ ℤ )
282 simpr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) )
283 279 280 281 282 fvdifsupp ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → ( 𝑔𝑣 ) = 0 )
284 283 negeqd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → - ( 𝑔𝑣 ) = - 0 )
285 284 236 eqtrdi ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ ( 𝑔 supp 0 ) ) ) → - ( 𝑔𝑣 ) = 0 )
286 285 19 suppss2 ( ( 𝜑𝑔𝐹 ) → ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) supp 0 ) ⊆ ( 𝑔 supp 0 ) )
287 277 42 278 47 286 fsuppsssuppgd ( ( 𝜑𝑔𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) finSupp 0 )
288 273 277 287 elrabd ( ( 𝜑𝑔𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
289 288 5 eleqtrrdi ( ( 𝜑𝑔𝐹 ) → ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ∈ 𝐹 )
290 eqid ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) = ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) )
291 fveq2 ( 𝑣 = 𝑤 → ( 𝑔𝑣 ) = ( 𝑔𝑤 ) )
292 291 negeqd ( 𝑣 = 𝑤 → - ( 𝑔𝑣 ) = - ( 𝑔𝑤 ) )
293 290 292 221 217 fvmptd3 ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) = - ( 𝑔𝑤 ) )
294 293 eqcomd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → - ( 𝑔𝑤 ) = ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) )
295 294 oveq1d ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
296 295 mpteq2dva ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
297 296 oveq2d ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ - ( 𝑔𝑣 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
298 272 289 297 rspcedvdw ( ( 𝜑𝑔𝐹 ) → ∃ 𝐹 ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
299 157 298 244 elrnmptd ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
300 299 8 eleqtrrdi ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑆 )
301 300 ad4ant13 ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( - ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑆 )
302 267 301 eqeltrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( ( invg𝑅 ) ‘ 𝑥 ) ∈ 𝑆 )
303 302 59 r19.29a ( ( 𝜑𝑥𝑆 ) → ( ( invg𝑅 ) ‘ 𝑥 ) ∈ 𝑆 )
304 215 303 jca ( ( 𝜑𝑥𝑆 ) → ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝑅 ) ‘ 𝑥 ) ∈ 𝑆 ) )
305 304 ralrimiva ( 𝜑 → ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝑅 ) ‘ 𝑥 ) ∈ 𝑆 ) )
306 1 105 264 issubg2 ( 𝑅 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝑆𝐵𝑆 ≠ ∅ ∧ ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝑅 ) ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
307 306 biimpar ( ( 𝑅 ∈ Grp ∧ ( 𝑆𝐵𝑆 ≠ ∅ ∧ ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝑅 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝑅 ) ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
308 9 64 101 305 307 syl13anc ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝑅 ) )