Metamath Proof Explorer


Theorem elrgspnlem4

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 elrgspnlem4 ( 𝜑 → ( 𝑁𝐴 ) = 𝑆 )

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 a1i ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
10 4 a1i ( 𝜑𝑁 = ( RingSpan ‘ 𝑅 ) )
11 eqidd ( 𝜑 → ( 𝑁𝐴 ) = ( 𝑁𝐴 ) )
12 6 9 7 10 11 rgspnval ( 𝜑 → ( 𝑁𝐴 ) = { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } )
13 sseq2 ( 𝑡 = 𝑆 → ( 𝐴𝑡𝐴𝑆 ) )
14 1 2 3 4 5 6 7 8 elrgspnlem2 ( 𝜑𝑆 ∈ ( SubRing ‘ 𝑅 ) )
15 1 2 3 4 5 6 7 8 elrgspnlem3 ( 𝜑𝐴𝑆 )
16 13 14 15 elrabd ( 𝜑𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } )
17 intss1 ( 𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } → { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } ⊆ 𝑆 )
18 16 17 syl ( 𝜑 { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } ⊆ 𝑆 )
19 simpr ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑠𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑠 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑠 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
20 eqidd ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → ( 𝑔 supp 0 ) = ( 𝑔 supp 0 ) )
21 oveq1 ( 𝑓 = 𝑔 → ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) )
22 21 eqeq1d ( 𝑓 = 𝑔 → ( ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) ↔ ( 𝑔 supp 0 ) = ( 𝑔 supp 0 ) ) )
23 fveq1 ( 𝑓 = 𝑔 → ( 𝑓𝑤 ) = ( 𝑔𝑤 ) )
24 23 oveq1d ( 𝑓 = 𝑔 → ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
25 24 mpteq2dv ( 𝑓 = 𝑔 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
26 25 oveq2d ( 𝑓 = 𝑔 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
27 26 eleq1d ( 𝑓 = 𝑔 → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ↔ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
28 22 27 imbi12d ( 𝑓 = 𝑔 → ( ( ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( 𝑔 supp 0 ) = ( 𝑔 supp 0 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
29 eqeq2 ( 𝑖 = ∅ → ( ( 𝑓 supp 0 ) = 𝑖 ↔ ( 𝑓 supp 0 ) = ∅ ) )
30 29 imbi1d ( 𝑖 = ∅ → ( ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( 𝑓 supp 0 ) = ∅ → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
31 30 ralbidv ( 𝑖 = ∅ → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ∅ → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
32 eqeq2 ( 𝑖 = → ( ( 𝑓 supp 0 ) = 𝑖 ↔ ( 𝑓 supp 0 ) = ) )
33 32 imbi1d ( 𝑖 = → ( ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
34 33 ralbidv ( 𝑖 = → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
35 eqeq2 ( 𝑖 = ( ∪ { 𝑥 } ) → ( ( 𝑓 supp 0 ) = 𝑖 ↔ ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) ) )
36 35 imbi1d ( 𝑖 = ( ∪ { 𝑥 } ) → ( ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
37 36 ralbidv ( 𝑖 = ( ∪ { 𝑥 } ) → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
38 eqeq2 ( 𝑖 = ( 𝑔 supp 0 ) → ( ( 𝑓 supp 0 ) = 𝑖 ↔ ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) ) )
39 38 imbi1d ( 𝑖 = ( 𝑔 supp 0 ) → ( ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
40 39 ralbidv ( 𝑖 = ( 𝑔 supp 0 ) → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
41 eqid ( 0g𝑅 ) = ( 0g𝑅 )
42 6 ringcmnd ( 𝜑𝑅 ∈ CMnd )
43 42 ad5antr ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → 𝑅 ∈ CMnd )
44 1 fvexi 𝐵 ∈ V
45 44 a1i ( 𝜑𝐵 ∈ V )
46 45 7 ssexd ( 𝜑𝐴 ∈ V )
47 wrdexg ( 𝐴 ∈ V → Word 𝐴 ∈ V )
48 46 47 syl ( 𝜑 → Word 𝐴 ∈ V )
49 48 ad5antr ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → Word 𝐴 ∈ V )
50 simp-4l ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) → 𝜑 )
51 5 reqabi ( 𝑓𝐹 ↔ ( 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑓 finSupp 0 ) )
52 51 simplbi ( 𝑓𝐹𝑓 ∈ ( ℤ ↑m Word 𝐴 ) )
53 52 adantl ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) → 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) )
54 zex ℤ ∈ V
55 54 a1i ( 𝜑 → ℤ ∈ V )
56 55 48 elmapd ( 𝜑 → ( 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑓 : Word 𝐴 ⟶ ℤ ) )
57 56 biimpa ( ( 𝜑𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ) → 𝑓 : Word 𝐴 ⟶ ℤ )
58 50 53 57 syl2anc ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) → 𝑓 : Word 𝐴 ⟶ ℤ )
59 58 ffnd ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) → 𝑓 Fn Word 𝐴 )
60 59 ad2antrr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 𝑓 Fn Word 𝐴 )
61 49 adantr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → Word 𝐴 ∈ V )
62 0zd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 0 ∈ ℤ )
63 simpr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) )
64 63 eldifad ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 𝑤 ∈ Word 𝐴 )
65 63 eldifbd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ¬ 𝑤 ∈ ∅ )
66 simplr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ( 𝑓 supp 0 ) = ∅ )
67 65 66 neleqtrrd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ¬ 𝑤 ∈ ( 𝑓 supp 0 ) )
68 64 67 eldifd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑓 supp 0 ) ) )
69 60 61 62 68 fvdifsupp ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ( 𝑓𝑤 ) = 0 )
70 69 oveq1d ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
71 2 ringmgp ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
72 6 71 syl ( 𝜑𝑀 ∈ Mnd )
73 72 ad6antr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 𝑀 ∈ Mnd )
74 sswrd ( 𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵 )
75 7 74 syl ( 𝜑 → Word 𝐴 ⊆ Word 𝐵 )
76 75 ad6antr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → Word 𝐴 ⊆ Word 𝐵 )
77 76 64 sseldd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → 𝑤 ∈ Word 𝐵 )
78 2 1 mgpbas 𝐵 = ( Base ‘ 𝑀 )
79 78 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
80 73 77 79 syl2anc ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
81 1 41 3 mulg0 ( ( 𝑀 Σg 𝑤 ) ∈ 𝐵 → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
82 80 81 syl ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
83 70 82 eqtrd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ∅ ) ) → ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
84 0fi ∅ ∈ Fin
85 84 a1i ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ∅ ∈ Fin )
86 6 ringgrpd ( 𝜑𝑅 ∈ Grp )
87 86 ad6antr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
88 58 ad2antrr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑓 : Word 𝐴 ⟶ ℤ )
89 simpr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐴 )
90 88 89 ffvelcdmd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑓𝑤 ) ∈ ℤ )
91 72 ad6antr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑀 ∈ Mnd )
92 75 ad6antr ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → Word 𝐴 ⊆ Word 𝐵 )
93 92 89 sseldd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
94 91 93 79 syl2anc ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
95 1 3 87 90 94 mulgcld ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
96 0ss ∅ ⊆ Word 𝐴
97 96 a1i ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ∅ ⊆ Word 𝐴 )
98 1 41 43 49 83 85 95 97 gsummptres2 ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ ∅ ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
99 mpt0 ( 𝑤 ∈ ∅ ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ∅
100 99 a1i ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 𝑤 ∈ ∅ ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ∅ )
101 100 oveq2d ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 𝑅 Σg ( 𝑤 ∈ ∅ ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ∅ ) )
102 41 gsum0 ( 𝑅 Σg ∅ ) = ( 0g𝑅 )
103 102 a1i ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 𝑅 Σg ∅ ) = ( 0g𝑅 ) )
104 98 101 103 3eqtrd ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 0g𝑅 ) )
105 subrgsubg ( 𝑡 ∈ ( SubRing ‘ 𝑅 ) → 𝑡 ∈ ( SubGrp ‘ 𝑅 ) )
106 41 subg0cl ( 𝑡 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g𝑅 ) ∈ 𝑡 )
107 105 106 syl ( 𝑡 ∈ ( SubRing ‘ 𝑅 ) → ( 0g𝑅 ) ∈ 𝑡 )
108 107 adantl ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) → ( 0g𝑅 ) ∈ 𝑡 )
109 108 ad4antr ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 0g𝑅 ) ∈ 𝑡 )
110 104 109 eqeltrd ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) ∧ ( 𝑓 supp 0 ) = ∅ ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 )
111 110 ex ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ 𝑓𝐹 ) → ( ( 𝑓 supp 0 ) = ∅ → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
112 111 ralrimiva ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ∅ → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
113 42 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑅 ∈ CMnd )
114 48 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → Word 𝐴 ∈ V )
115 simp-5l ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) → 𝜑 )
116 breq1 ( 𝑓 = 𝑒 → ( 𝑓 finSupp 0 ↔ 𝑒 finSupp 0 ) )
117 116 5 elrab2 ( 𝑒𝐹 ↔ ( 𝑒 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑒 finSupp 0 ) )
118 117 simplbi ( 𝑒𝐹𝑒 ∈ ( ℤ ↑m Word 𝐴 ) )
119 55 48 elmapd ( 𝜑 → ( 𝑒 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑒 : Word 𝐴 ⟶ ℤ ) )
120 119 biimpa ( ( 𝜑𝑒 ∈ ( ℤ ↑m Word 𝐴 ) ) → 𝑒 : Word 𝐴 ⟶ ℤ )
121 118 120 sylan2 ( ( 𝜑𝑒𝐹 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
122 115 121 sylancom ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
123 122 adantl3r ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
124 123 ffnd ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) → 𝑒 Fn Word 𝐴 )
125 124 ad2antrr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → 𝑒 Fn Word 𝐴 )
126 114 adantr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → Word 𝐴 ∈ V )
127 0zd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → 0 ∈ ℤ )
128 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) )
129 125 126 127 128 fvdifsupp ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → ( 𝑒𝑤 ) = 0 )
130 129 oveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
131 72 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → 𝑀 ∈ Mnd )
132 75 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → Word 𝐴 ⊆ Word 𝐵 )
133 128 eldifad ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → 𝑤 ∈ Word 𝐴 )
134 132 133 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → 𝑤 ∈ Word 𝐵 )
135 131 134 79 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
136 135 81 syl ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
137 130 136 eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) ) → ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
138 117 simprbi ( 𝑒𝐹𝑒 finSupp 0 )
139 138 ad2antlr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑒 finSupp 0 )
140 139 fsuppimpd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒 supp 0 ) ∈ Fin )
141 86 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
142 123 ad2antrr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
143 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐴 )
144 142 143 ffvelcdmd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑒𝑤 ) ∈ ℤ )
145 72 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑀 ∈ Mnd )
146 75 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → Word 𝐴 ⊆ Word 𝐵 )
147 146 sselda ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
148 145 147 79 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
149 1 3 141 144 148 mulgcld ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
150 suppssdm ( 𝑒 supp 0 ) ⊆ dom 𝑒
151 123 adantr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑒 : Word 𝐴 ⟶ ℤ )
152 150 151 fssdm ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒 supp 0 ) ⊆ Word 𝐴 )
153 1 41 113 114 137 140 149 152 gsummptres2 ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ ( 𝑒 supp 0 ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
154 153 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ ( 𝑒 supp 0 ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
155 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) )
156 155 mpteq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑤 ∈ ( 𝑒 supp 0 ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ ( ∪ { 𝑥 } ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
157 156 oveq2d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ ( 𝑒 supp 0 ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ ( ∪ { 𝑥 } ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
158 eqid ( +g𝑅 ) = ( +g𝑅 )
159 breq1 ( 𝑓 = 𝑔 → ( 𝑓 finSupp 0 ↔ 𝑔 finSupp 0 ) )
160 159 5 elrab2 ( 𝑔𝐹 ↔ ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
161 160 simprbi ( 𝑔𝐹𝑔 finSupp 0 )
162 161 adantl ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → 𝑔 finSupp 0 )
163 162 fsuppimpd ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → ( 𝑔 supp 0 ) ∈ Fin )
164 163 ad4antr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑔 supp 0 ) ∈ Fin )
165 simp-4r ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ⊆ ( 𝑔 supp 0 ) )
166 164 165 ssfid ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ∈ Fin )
167 86 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → 𝑅 ∈ Grp )
168 151 adantr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
169 suppssdm ( 𝑔 supp 0 ) ⊆ dom 𝑔
170 simp-7l ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝜑 )
171 simp-5r ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑔𝐹 )
172 160 simplbi ( 𝑔𝐹𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
173 55 48 elmapd ( 𝜑 → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ↔ 𝑔 : Word 𝐴 ⟶ ℤ ) )
174 173 biimpa ( ( 𝜑𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
175 172 174 sylan2 ( ( 𝜑𝑔𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
176 170 171 175 syl2anc ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑔 : Word 𝐴 ⟶ ℤ )
177 169 176 fssdm ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑔 supp 0 ) ⊆ Word 𝐴 )
178 165 177 sstrd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ⊆ Word 𝐴 )
179 178 sselda ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → 𝑤 ∈ Word 𝐴 )
180 168 179 ffvelcdmd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( 𝑒𝑤 ) ∈ ℤ )
181 179 148 syldan ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
182 1 3 167 180 181 mulgcld ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
183 simpllr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) )
184 183 eldifbd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ¬ 𝑥 )
185 170 86 syl ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑅 ∈ Grp )
186 183 eldifad ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑥 ∈ ( 𝑔 supp 0 ) )
187 177 186 sseldd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑥 ∈ Word 𝐴 )
188 151 187 ffvelcdmd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒𝑥 ) ∈ ℤ )
189 170 72 syl ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑀 ∈ Mnd )
190 146 187 sseldd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑥 ∈ Word 𝐵 )
191 78 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑥 ) ∈ 𝐵 )
192 189 190 191 syl2anc ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑀 Σg 𝑥 ) ∈ 𝐵 )
193 1 3 185 188 192 mulgcld ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) ∈ 𝐵 )
194 fveq2 ( 𝑤 = 𝑥 → ( 𝑒𝑤 ) = ( 𝑒𝑥 ) )
195 oveq2 ( 𝑤 = 𝑥 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 𝑥 ) )
196 194 195 oveq12d ( 𝑤 = 𝑥 → ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) )
197 1 158 113 166 182 183 184 193 196 gsumunsn ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ ( ∪ { 𝑥 } ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) ) )
198 197 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ ( ∪ { 𝑥 } ) ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) ) )
199 154 157 198 3eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) ) )
200 105 ad8antlr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑡 ∈ ( SubGrp ‘ 𝑅 ) )
201 124 adantr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑒 Fn Word 𝐴 )
202 0zd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 0 ∈ ℤ )
203 201 187 202 fmptunsnop ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) )
204 203 adantr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) )
205 204 fveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) ‘ 𝑤 ) = ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) )
206 eqid ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) = ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) )
207 eqidd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ 𝑦 = 𝑥 ) → 0 = 0 )
208 201 ad3antrrr ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑒 Fn Word 𝐴 )
209 114 ad3antrrr ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → Word 𝐴 ∈ V )
210 0zd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 0 ∈ ℤ )
211 simplr ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑦 = 𝑤 )
212 simpllr ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑤 ∈ ( Word 𝐴 ) )
213 212 eldifad ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑤 ∈ Word 𝐴 )
214 211 213 eqeltrd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑦 ∈ Word 𝐴 )
215 simp-4r ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) )
216 212 eldifbd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ¬ 𝑤 )
217 211 216 eqneltrd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ¬ 𝑦 )
218 simpr ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ¬ 𝑦 = 𝑥 )
219 218 neqned ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑦𝑥 )
220 nelsn ( 𝑦𝑥 → ¬ 𝑦 ∈ { 𝑥 } )
221 219 220 syl ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ¬ 𝑦 ∈ { 𝑥 } )
222 nelun ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( ¬ 𝑦 ∈ ( 𝑒 supp 0 ) ↔ ( ¬ 𝑦 ∧ ¬ 𝑦 ∈ { 𝑥 } ) ) )
223 222 biimpar ( ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ∧ ( ¬ 𝑦 ∧ ¬ 𝑦 ∈ { 𝑥 } ) ) → ¬ 𝑦 ∈ ( 𝑒 supp 0 ) )
224 215 217 221 223 syl12anc ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ¬ 𝑦 ∈ ( 𝑒 supp 0 ) )
225 214 224 eldifd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑦 ∈ ( Word 𝐴 ∖ ( 𝑒 supp 0 ) ) )
226 208 209 210 225 fvdifsupp ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) ∧ ¬ 𝑦 = 𝑥 ) → ( 𝑒𝑦 ) = 0 )
227 207 226 ifeqda ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) ∧ 𝑦 = 𝑤 ) → if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) = 0 )
228 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → 𝑤 ∈ ( Word 𝐴 ) )
229 228 eldifad ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → 𝑤 ∈ Word 𝐴 )
230 0zd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → 0 ∈ ℤ )
231 206 227 229 230 fvmptd2 ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) ‘ 𝑤 ) = 0 )
232 205 231 eqtr3d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) = 0 )
233 232 oveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
234 229 148 syldan ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
235 234 81 syl ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
236 233 235 eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ ( Word 𝐴 ) ) → ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
237 203 adantr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) )
238 237 fveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) ‘ 𝑤 ) = ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) )
239 0zd ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ 𝑦 = 𝑥 ) → 0 ∈ ℤ )
240 151 ad2antrr ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
241 simplr ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑦 ∈ Word 𝐴 )
242 240 241 ffvelcdmd ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → ( 𝑒𝑦 ) ∈ ℤ )
243 239 242 ifclda ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) → if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ∈ ℤ )
244 243 fmpttd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) : Word 𝐴 ⟶ ℤ )
245 244 ffvelcdmda ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) ‘ 𝑤 ) ∈ ℤ )
246 238 245 eqeltrrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) ∈ ℤ )
247 1 3 141 246 148 mulgcld ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
248 1 41 113 114 236 166 247 178 gsummptres2 ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
249 248 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
250 203 adantr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) )
251 250 fveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) ‘ 𝑤 ) = ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) )
252 simpr ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
253 simplr ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → 𝑤 )
254 252 253 eqeltrd ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → 𝑦 )
255 184 ad2antrr ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → ¬ 𝑥 )
256 nelneq ( ( 𝑦 ∧ ¬ 𝑥 ) → ¬ 𝑦 = 𝑥 )
257 254 255 256 syl2anc ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → ¬ 𝑦 = 𝑥 )
258 257 iffalsed ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) = ( 𝑒𝑦 ) )
259 252 fveq2d ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → ( 𝑒𝑦 ) = ( 𝑒𝑤 ) )
260 258 259 eqtrd ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) ∧ 𝑦 = 𝑤 ) → if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) = ( 𝑒𝑤 ) )
261 206 260 179 180 fvmptd2 ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) ‘ 𝑤 ) = ( 𝑒𝑤 ) )
262 251 261 eqtr3d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) = ( 𝑒𝑤 ) )
263 262 oveq1d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑤 ) → ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
264 263 mpteq2dva ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑤 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
265 264 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑤 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
266 265 oveq2d ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
267 249 266 eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
268 simplr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑒𝐹 )
269 268 resexd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∈ V )
270 snex { ⟨ 𝑥 , 0 ⟩ } ∈ V
271 270 a1i ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → { ⟨ 𝑥 , 0 ⟩ } ∈ V )
272 269 271 202 suppun2 ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) = ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) supp 0 ) ∪ ( { ⟨ 𝑥 , 0 ⟩ } supp 0 ) ) )
273 114 202 201 fdifsupp ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) supp 0 ) = ( ( 𝑒 supp 0 ) ∖ { 𝑥 } ) )
274 simpr ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) )
275 274 difeq1d ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 supp 0 ) ∖ { 𝑥 } ) = ( ( ∪ { 𝑥 } ) ∖ { 𝑥 } ) )
276 disjsn ( ( ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 )
277 undif5 ( ( ∩ { 𝑥 } ) = ∅ → ( ( ∪ { 𝑥 } ) ∖ { 𝑥 } ) = )
278 276 277 sylbir ( ¬ 𝑥 → ( ( ∪ { 𝑥 } ) ∖ { 𝑥 } ) = )
279 184 278 syl ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ∪ { 𝑥 } ) ∖ { 𝑥 } ) = )
280 273 275 279 3eqtrd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) supp 0 ) = )
281 vex 𝑥 ∈ V
282 c0ex 0 ∈ V
283 281 282 xpsn ( { 𝑥 } × { 0 } ) = { ⟨ 𝑥 , 0 ⟩ }
284 283 oveq1i ( ( { 𝑥 } × { 0 } ) supp 0 ) = ( { ⟨ 𝑥 , 0 ⟩ } supp 0 )
285 fczsupp0 ( ( { 𝑥 } × { 0 } ) supp 0 ) = ∅
286 284 285 eqtr3i ( { ⟨ 𝑥 , 0 ⟩ } supp 0 ) = ∅
287 286 a1i ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( { ⟨ 𝑥 , 0 ⟩ } supp 0 ) = ∅ )
288 280 287 uneq12d ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) supp 0 ) ∪ ( { ⟨ 𝑥 , 0 ⟩ } supp 0 ) ) = ( ∪ ∅ ) )
289 un0 ( ∪ ∅ ) =
290 289 a1i ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ∪ ∅ ) = )
291 272 288 290 3eqtrd ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) = )
292 291 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) = )
293 oveq1 ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( 𝑓 supp 0 ) = ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) )
294 293 eqeq1d ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( ( 𝑓 supp 0 ) = ↔ ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) = ) )
295 fveq1 ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( 𝑓𝑤 ) = ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) )
296 295 oveq1d ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
297 296 mpteq2dv ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
298 297 oveq2d ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
299 298 eleq1d ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ↔ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
300 294 299 imbi12d ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
301 simpllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
302 breq1 ( 𝑓 = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) → ( 𝑓 finSupp 0 ↔ ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) finSupp 0 ) )
303 54 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ℤ ∈ V )
304 114 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → Word 𝐴 ∈ V )
305 203 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) = ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) )
306 0zd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ 𝑦 = 𝑥 ) → 0 ∈ ℤ )
307 simp-10l ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝜑 )
308 simp-4r ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑒𝐹 )
309 307 308 121 syl2anc ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑒 : Word 𝐴 ⟶ ℤ )
310 simplr ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → 𝑦 ∈ Word 𝐴 )
311 309 310 ffvelcdmd ( ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) ∧ ¬ 𝑦 = 𝑥 ) → ( 𝑒𝑦 ) ∈ ℤ )
312 306 311 ifclda ( ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) ∧ 𝑦 ∈ Word 𝐴 ) → if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ∈ ℤ )
313 312 fmpttd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑦 ∈ Word 𝐴 ↦ if ( 𝑦 = 𝑥 , 0 , ( 𝑒𝑦 ) ) ) : Word 𝐴 ⟶ ℤ )
314 305 313 feq1dd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) : Word 𝐴 ⟶ ℤ )
315 303 304 314 elmapdd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ∈ ( ℤ ↑m Word 𝐴 ) )
316 0zd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 0 ∈ ℤ )
317 314 ffund ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → Fun ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) )
318 166 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ∈ Fin )
319 292 318 eqeltrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) ∈ Fin )
320 315 316 317 319 isfsuppd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) finSupp 0 )
321 302 315 320 elrabd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
322 321 5 eleqtrrdi ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ∈ 𝐹 )
323 300 301 322 rspcdva ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
324 292 323 mpd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( ( 𝑒 ↾ ( Word 𝐴 ∖ { 𝑥 } ) ) ∪ { ⟨ 𝑥 , 0 ⟩ } ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 )
325 267 324 eqeltrrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 )
326 86 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑅 ∈ Grp )
327 2 subrgsubm ( 𝑡 ∈ ( SubRing ‘ 𝑅 ) → 𝑡 ∈ ( SubMnd ‘ 𝑀 ) )
328 327 ad8antlr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑡 ∈ ( SubMnd ‘ 𝑀 ) )
329 sswrd ( 𝐴𝑡 → Word 𝐴 ⊆ Word 𝑡 )
330 329 ad7antlr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → Word 𝐴 ⊆ Word 𝑡 )
331 187 adantllr ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑥 ∈ Word 𝐴 )
332 330 331 sseldd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑥 ∈ Word 𝑡 )
333 gsumwsubmcl ( ( 𝑡 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑥 ∈ Word 𝑡 ) → ( 𝑀 Σg 𝑥 ) ∈ 𝑡 )
334 328 332 333 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑀 Σg 𝑥 ) ∈ 𝑡 )
335 123 ad4ant13 ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → 𝑒 : Word 𝐴 ⟶ ℤ )
336 335 331 ffvelcdmd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑒𝑥 ) ∈ ℤ )
337 1 3 326 334 200 336 subgmulgcld ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) ∈ 𝑡 )
338 158 200 325 337 subgcld ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( ( 𝑅 Σg ( 𝑤 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ( +g𝑅 ) ( ( 𝑒𝑥 ) · ( 𝑀 Σg 𝑥 ) ) ) ∈ 𝑡 )
339 199 338 eqeltrd ( ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) ∧ ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 )
340 339 ex ( ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) ∧ 𝑒𝐹 ) → ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
341 340 ralrimiva ( ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ∧ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) → ∀ 𝑒𝐹 ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
342 341 ex ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ⊆ ( 𝑔 supp 0 ) ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) → ∀ 𝑒𝐹 ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
343 342 anasss ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ( ⊆ ( 𝑔 supp 0 ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ) → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) → ∀ 𝑒𝐹 ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
344 oveq1 ( 𝑒 = 𝑓 → ( 𝑒 supp 0 ) = ( 𝑓 supp 0 ) )
345 344 eqeq1d ( 𝑒 = 𝑓 → ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) ↔ ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) ) )
346 fveq1 ( 𝑒 = 𝑓 → ( 𝑒𝑤 ) = ( 𝑓𝑤 ) )
347 346 oveq1d ( 𝑒 = 𝑓 → ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
348 347 mpteq2dv ( 𝑒 = 𝑓 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
349 348 oveq2d ( 𝑒 = 𝑓 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
350 349 eleq1d ( 𝑒 = 𝑓 → ( ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ↔ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
351 345 350 imbi12d ( 𝑒 = 𝑓 → ( ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ( ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
352 351 cbvralvw ( ∀ 𝑒𝐹 ( ( 𝑒 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑒𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ↔ ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
353 343 352 imbitrdi ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) ∧ ( ⊆ ( 𝑔 supp 0 ) ∧ 𝑥 ∈ ( ( 𝑔 supp 0 ) ∖ ) ) ) → ( ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) → ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ( ∪ { 𝑥 } ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) ) )
354 31 34 37 40 112 353 163 findcard2d ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → ∀ 𝑓𝐹 ( ( 𝑓 supp 0 ) = ( 𝑔 supp 0 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑓𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
355 simpr ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → 𝑔𝐹 )
356 28 354 355 rspcdva ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → ( ( 𝑔 supp 0 ) = ( 𝑔 supp 0 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 ) )
357 20 356 mpd ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 )
358 357 ad4ant13 ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑠𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑠 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝑡 )
359 19 358 eqeltrd ( ( ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑠𝑆 ) ∧ 𝑔𝐹 ) ∧ 𝑠 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑠𝑡 )
360 eqid ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
361 8 eleq2i ( 𝑠𝑆𝑠 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
362 361 biimpi ( 𝑠𝑆𝑠 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
363 362 adantl ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑠𝑆 ) → 𝑠 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
364 360 363 elrnmpt2d ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑠𝑆 ) → ∃ 𝑔𝐹 𝑠 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
365 359 364 r19.29a ( ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) ∧ 𝑠𝑆 ) → 𝑠𝑡 )
366 365 ex ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) → ( 𝑠𝑆𝑠𝑡 ) )
367 366 ssrdv ( ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝐴𝑡 ) → 𝑆𝑡 )
368 367 ex ( ( 𝜑𝑡 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐴𝑡𝑆𝑡 ) )
369 368 ralrimiva ( 𝜑 → ∀ 𝑡 ∈ ( SubRing ‘ 𝑅 ) ( 𝐴𝑡𝑆𝑡 ) )
370 ssintrab ( 𝑆 { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } ↔ ∀ 𝑡 ∈ ( SubRing ‘ 𝑅 ) ( 𝐴𝑡𝑆𝑡 ) )
371 369 370 sylibr ( 𝜑𝑆 { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } )
372 18 371 eqssd ( 𝜑 { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } = 𝑆 )
373 12 372 eqtrd ( 𝜑 → ( 𝑁𝐴 ) = 𝑆 )