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

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