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

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