Metamath Proof Explorer


Theorem elrgspn

Description: Membership in the subring generated by the subset A . An element X lies in that subring if and only if X is a linear combination with integer coefficients of products of elements of A . (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 ( 𝜑𝐴𝐵 )
Assertion elrgspn ( 𝜑 → ( 𝑋 ∈ ( 𝑁𝐴 ) ↔ ∃ 𝑔𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )

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 1 a1i ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
9 4 a1i ( 𝜑𝑁 = ( RingSpan ‘ 𝑅 ) )
10 eqidd ( 𝜑 → ( 𝑁𝐴 ) = ( 𝑁𝐴 ) )
11 6 8 7 9 10 rgspncl ( 𝜑 → ( 𝑁𝐴 ) ∈ ( SubRing ‘ 𝑅 ) )
12 1 subrgss ( ( 𝑁𝐴 ) ∈ ( SubRing ‘ 𝑅 ) → ( 𝑁𝐴 ) ⊆ 𝐵 )
13 11 12 syl ( 𝜑 → ( 𝑁𝐴 ) ⊆ 𝐵 )
14 13 sselda ( ( 𝜑𝑋 ∈ ( 𝑁𝐴 ) ) → 𝑋𝐵 )
15 simpr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
16 eqid ( 0g𝑅 ) = ( 0g𝑅 )
17 6 ringcmnd ( 𝜑𝑅 ∈ CMnd )
18 17 adantr ( ( 𝜑𝑔𝐹 ) → 𝑅 ∈ CMnd )
19 1 fvexi 𝐵 ∈ V
20 19 a1i ( 𝜑𝐵 ∈ V )
21 20 7 ssexd ( 𝜑𝐴 ∈ V )
22 21 adantr ( ( 𝜑𝑔𝐹 ) → 𝐴 ∈ V )
23 wrdexg ( 𝐴 ∈ V → Word 𝐴 ∈ V )
24 22 23 syl ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ∈ V )
25 6 ringgrpd ( 𝜑𝑅 ∈ Grp )
26 25 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
27 zex ℤ ∈ V
28 27 a1i ( ( 𝜑𝑔𝐹 ) → ℤ ∈ V )
29 breq1 ( 𝑓 = 𝑔 → ( 𝑓 finSupp 0 ↔ 𝑔 finSupp 0 ) )
30 29 5 elrab2 ( 𝑔𝐹 ↔ ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
31 30 biimpi ( 𝑔𝐹 → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
32 31 simpld ( 𝑔𝐹𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
33 32 adantl ( ( 𝜑𝑔𝐹 ) → 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
34 24 28 33 elmaprd ( ( 𝜑𝑔𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
35 34 ffvelcdmda ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔𝑤 ) ∈ ℤ )
36 2 ringmgp ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
37 6 36 syl ( 𝜑𝑀 ∈ Mnd )
38 37 ad2antrr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑀 ∈ Mnd )
39 sswrd ( 𝐴𝐵 → Word 𝐴 ⊆ Word 𝐵 )
40 7 39 syl ( 𝜑 → Word 𝐴 ⊆ Word 𝐵 )
41 40 adantr ( ( 𝜑𝑔𝐹 ) → Word 𝐴 ⊆ Word 𝐵 )
42 41 sselda ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
43 2 1 mgpbas 𝐵 = ( Base ‘ 𝑀 )
44 43 gsumwcl ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
45 38 42 44 syl2anc ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
46 1 3 26 35 45 mulgcld ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
47 46 fmpttd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) : Word 𝐴𝐵 )
48 34 feqmptd ( ( 𝜑𝑔𝐹 ) → 𝑔 = ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑔𝑤 ) ) )
49 31 simprd ( 𝑔𝐹𝑔 finSupp 0 )
50 49 adantl ( ( 𝜑𝑔𝐹 ) → 𝑔 finSupp 0 )
51 48 50 eqbrtrrd ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑔𝑤 ) ) finSupp 0 )
52 1 16 3 mulg0 ( 𝑦𝐵 → ( 0 · 𝑦 ) = ( 0g𝑅 ) )
53 52 adantl ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑦𝐵 ) → ( 0 · 𝑦 ) = ( 0g𝑅 ) )
54 fvexd ( ( 𝜑𝑔𝐹 ) → ( 0g𝑅 ) ∈ V )
55 51 53 35 45 54 fsuppssov1 ( ( 𝜑𝑔𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g𝑅 ) )
56 1 16 18 24 47 55 gsumcl ( ( 𝜑𝑔𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
57 56 adantr ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
58 15 57 eqeltrd ( ( ( 𝜑𝑔𝐹 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑋𝐵 )
59 58 r19.29an ( ( 𝜑 ∧ ∃ 𝑔𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑋𝐵 )
60 6 adantr ( ( 𝜑𝑋𝐵 ) → 𝑅 ∈ Ring )
61 7 adantr ( ( 𝜑𝑋𝐵 ) → 𝐴𝐵 )
62 fveq1 ( = 𝑖 → ( 𝑤 ) = ( 𝑖𝑤 ) )
63 62 oveq1d ( = 𝑖 → ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
64 63 mpteq2dv ( = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
65 fveq2 ( 𝑤 = 𝑣 → ( 𝑖𝑤 ) = ( 𝑖𝑣 ) )
66 oveq2 ( 𝑤 = 𝑣 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 𝑣 ) )
67 65 66 oveq12d ( 𝑤 = 𝑣 → ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) )
68 67 cbvmptv ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) )
69 64 68 eqtrdi ( = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) )
70 69 oveq2d ( = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
71 70 cbvmptv ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑖𝐹 ↦ ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
72 71 rneqi ran ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ran ( 𝑖𝐹 ↦ ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
73 1 2 3 4 5 60 61 72 elrgspnlem4 ( ( 𝜑𝑋𝐵 ) → ( 𝑁𝐴 ) = ran ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
74 73 eleq2d ( ( 𝜑𝑋𝐵 ) → ( 𝑋 ∈ ( 𝑁𝐴 ) ↔ 𝑋 ∈ ran ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ) )
75 fveq1 ( = 𝑔 → ( 𝑤 ) = ( 𝑔𝑤 ) )
76 75 oveq1d ( = 𝑔 → ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
77 76 mpteq2dv ( = 𝑔 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
78 77 oveq2d ( = 𝑔 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
79 78 cbvmptv ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
80 79 elrnmpt ( 𝑋𝐵 → ( 𝑋 ∈ ran ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
81 80 adantl ( ( 𝜑𝑋𝐵 ) → ( 𝑋 ∈ ran ( 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
82 74 81 bitrd ( ( 𝜑𝑋𝐵 ) → ( 𝑋 ∈ ( 𝑁𝐴 ) ↔ ∃ 𝑔𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
83 14 59 82 bibiad ( 𝜑 → ( 𝑋 ∈ ( 𝑁𝐴 ) ↔ ∃ 𝑔𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )