Metamath Proof Explorer


Theorem elrgspnlem3

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 elrgspnlem3 ( 𝜑𝐴𝑆 )

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 eqid ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
10 fveq1 ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) → ( 𝑔𝑤 ) = ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) )
11 10 oveq1d ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
12 11 mpteq2dv ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
13 12 oveq2d ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
14 13 eqeq2d ( 𝑔 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) → ( 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ↔ 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
15 breq1 ( 𝑓 = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) → ( 𝑓 finSupp 0 ↔ ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) finSupp 0 ) )
16 zex ℤ ∈ V
17 16 a1i ( ( 𝜑𝑥𝐴 ) → ℤ ∈ V )
18 1 fvexi 𝐵 ∈ V
19 18 a1i ( 𝜑𝐵 ∈ V )
20 19 7 ssexd ( 𝜑𝐴 ∈ V )
21 wrdexg ( 𝐴 ∈ V → Word 𝐴 ∈ V )
22 20 21 syl ( 𝜑 → Word 𝐴 ∈ V )
23 22 adantr ( ( 𝜑𝑥𝐴 ) → Word 𝐴 ∈ V )
24 1zzd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ 𝑣 = ⟨“ 𝑥 ”⟩ ) → 1 ∈ ℤ )
25 0zd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑣 ∈ Word 𝐴 ) ∧ ¬ 𝑣 = ⟨“ 𝑥 ”⟩ ) → 0 ∈ ℤ )
26 24 25 ifclda ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑣 ∈ Word 𝐴 ) → if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ∈ ℤ )
27 26 fmpttd ( ( 𝜑𝑥𝐴 ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) : Word 𝐴 ⟶ ℤ )
28 17 23 27 elmapdd ( ( 𝜑𝑥𝐴 ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ∈ ( ℤ ↑m Word 𝐴 ) )
29 28 elexd ( ( 𝜑𝑥𝐴 ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ∈ V )
30 27 ffund ( ( 𝜑𝑥𝐴 ) → Fun ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) )
31 0zd ( ( 𝜑𝑥𝐴 ) → 0 ∈ ℤ )
32 snfi { ⟨“ 𝑥 ”⟩ } ∈ Fin
33 32 a1i ( ( 𝜑𝑥𝐴 ) → { ⟨“ 𝑥 ”⟩ } ∈ Fin )
34 eldifsni ( 𝑣 ∈ ( Word 𝐴 ∖ { ⟨“ 𝑥 ”⟩ } ) → 𝑣 ≠ ⟨“ 𝑥 ”⟩ )
35 34 adantl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ { ⟨“ 𝑥 ”⟩ } ) ) → 𝑣 ≠ ⟨“ 𝑥 ”⟩ )
36 35 neneqd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ { ⟨“ 𝑥 ”⟩ } ) ) → ¬ 𝑣 = ⟨“ 𝑥 ”⟩ )
37 36 iffalsed ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑣 ∈ ( Word 𝐴 ∖ { ⟨“ 𝑥 ”⟩ } ) ) → if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) = 0 )
38 37 23 suppss2 ( ( 𝜑𝑥𝐴 ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) supp 0 ) ⊆ { ⟨“ 𝑥 ”⟩ } )
39 suppssfifsupp ( ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ∈ V ∧ Fun ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ∧ 0 ∈ ℤ ) ∧ ( { ⟨“ 𝑥 ”⟩ } ∈ Fin ∧ ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) supp 0 ) ⊆ { ⟨“ 𝑥 ”⟩ } ) ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) finSupp 0 )
40 29 30 31 33 38 39 syl32anc ( ( 𝜑𝑥𝐴 ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) finSupp 0 )
41 15 28 40 elrabd ( ( 𝜑𝑥𝐴 ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ∈ { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 } )
42 41 5 eleqtrrdi ( ( 𝜑𝑥𝐴 ) → ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ∈ 𝐹 )
43 eqeq2 ( 𝑥 = if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) → ( ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = 𝑥 ↔ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) ) )
44 eqeq2 ( ( 0g𝑅 ) = if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) → ( ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) ↔ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) ) )
45 eqid ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) = ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) )
46 simpr ( ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) ∧ 𝑣 = 𝑤 ) → 𝑣 = 𝑤 )
47 simplr ( ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) ∧ 𝑣 = 𝑤 ) → 𝑤 = ⟨“ 𝑥 ”⟩ )
48 46 47 eqtrd ( ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) ∧ 𝑣 = 𝑤 ) → 𝑣 = ⟨“ 𝑥 ”⟩ )
49 48 iftrued ( ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) ∧ 𝑣 = 𝑤 ) → if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) = 1 )
50 simplr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 𝑤 ∈ Word 𝐴 )
51 1zzd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 1 ∈ ℤ )
52 45 49 50 51 fvmptd2 ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) = 1 )
53 simpr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 𝑤 = ⟨“ 𝑥 ”⟩ )
54 53 oveq2d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg ⟨“ 𝑥 ”⟩ ) )
55 7 sselda ( ( 𝜑𝑥𝐴 ) → 𝑥𝐵 )
56 55 ad2antrr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 𝑥𝐵 )
57 2 1 mgpbas 𝐵 = ( Base ‘ 𝑀 )
58 57 gsumws1 ( 𝑥𝐵 → ( 𝑀 Σg ⟨“ 𝑥 ”⟩ ) = 𝑥 )
59 56 58 syl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( 𝑀 Σg ⟨“ 𝑥 ”⟩ ) = 𝑥 )
60 54 59 eqtrd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( 𝑀 Σg 𝑤 ) = 𝑥 )
61 52 60 oveq12d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 1 · 𝑥 ) )
62 1 3 mulg1 ( 𝑥𝐵 → ( 1 · 𝑥 ) = 𝑥 )
63 56 62 syl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( 1 · 𝑥 ) = 𝑥 )
64 61 63 eqtrd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = 𝑥 )
65 eqeq1 ( 𝑣 = 𝑤 → ( 𝑣 = ⟨“ 𝑥 ”⟩ ↔ 𝑤 = ⟨“ 𝑥 ”⟩ ) )
66 65 notbid ( 𝑣 = 𝑤 → ( ¬ 𝑣 = ⟨“ 𝑥 ”⟩ ↔ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) )
67 66 biimparc ( ( ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ∧ 𝑣 = 𝑤 ) → ¬ 𝑣 = ⟨“ 𝑥 ”⟩ )
68 67 adantll ( ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) ∧ 𝑣 = 𝑤 ) → ¬ 𝑣 = ⟨“ 𝑥 ”⟩ )
69 68 iffalsed ( ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) ∧ 𝑣 = 𝑤 ) → if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) = 0 )
70 simplr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 𝑤 ∈ Word 𝐴 )
71 0zd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 0 ∈ ℤ )
72 45 69 70 71 fvmptd2 ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) = 0 )
73 72 oveq1d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0 · ( 𝑀 Σg 𝑤 ) ) )
74 2 ringmgp ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
75 6 74 syl ( 𝜑𝑀 ∈ Mnd )
76 75 ad3antrrr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 𝑀 ∈ Mnd )
77 sswrd ( 𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵 )
78 7 77 syl ( 𝜑 → Word 𝐴 ⊆ Word 𝐵 )
79 78 adantr ( ( 𝜑𝑥𝐴 ) → Word 𝐴 ⊆ Word 𝐵 )
80 79 sselda ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
81 80 adantr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → 𝑤 ∈ Word 𝐵 )
82 57 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
83 76 81 82 syl2anc ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
84 eqid ( 0g𝑅 ) = ( 0g𝑅 )
85 1 84 3 mulg0 ( ( 𝑀 Σg 𝑤 ) ∈ 𝐵 → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
86 83 85 syl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( 0 · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
87 73 86 eqtrd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) ∧ ¬ 𝑤 = ⟨“ 𝑥 ”⟩ ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( 0g𝑅 ) )
88 43 44 64 87 ifbothda ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) )
89 88 mpteq2dva ( ( 𝜑𝑥𝐴 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) ) )
90 89 oveq2d ( ( 𝜑𝑥𝐴 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) ) ) )
91 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
92 6 91 syl ( 𝜑𝑅 ∈ Mnd )
93 92 adantr ( ( 𝜑𝑥𝐴 ) → 𝑅 ∈ Mnd )
94 simpr ( ( 𝜑𝑥𝐴 ) → 𝑥𝐴 )
95 94 s1cld ( ( 𝜑𝑥𝐴 ) → ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 )
96 eqid ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) )
97 7 1 sseqtrdi ( 𝜑𝐴 ⊆ ( Base ‘ 𝑅 ) )
98 97 sselda ( ( 𝜑𝑥𝐴 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
99 84 93 23 95 96 98 gsummptif1n0 ( ( 𝜑𝑥𝐴 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ if ( 𝑤 = ⟨“ 𝑥 ”⟩ , 𝑥 , ( 0g𝑅 ) ) ) ) = 𝑥 )
100 90 99 eqtr2d ( ( 𝜑𝑥𝐴 ) → 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ( 𝑣 ∈ Word 𝐴 ↦ if ( 𝑣 = ⟨“ 𝑥 ”⟩ , 1 , 0 ) ) ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
101 14 42 100 rspcedvdw ( ( 𝜑𝑥𝐴 ) → ∃ 𝑔𝐹 𝑥 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
102 9 101 94 elrnmptd ( ( 𝜑𝑥𝐴 ) → 𝑥 ∈ ran ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
103 102 8 eleqtrrdi ( ( 𝜑𝑥𝐴 ) → 𝑥𝑆 )
104 103 ex ( 𝜑 → ( 𝑥𝐴𝑥𝑆 ) )
105 104 ssrdv ( 𝜑𝐴𝑆 )