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

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 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )