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

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 𝑤 ) ) ) ) ) )