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 B = Base R
elrgspn.m M = mulGrp R
elrgspn.x · ˙ = R
elrgspn.n N = RingSpan R
elrgspn.f F = f Word A | finSupp 0 f
elrgspn.r φ R Ring
elrgspn.a φ A B
Assertion elrgspn φ X N A g F X = R w Word A g w · ˙ M w

Proof

Step Hyp Ref Expression
1 elrgspn.b B = Base R
2 elrgspn.m M = mulGrp R
3 elrgspn.x · ˙ = R
4 elrgspn.n N = RingSpan R
5 elrgspn.f F = f Word A | finSupp 0 f
6 elrgspn.r φ R Ring
7 elrgspn.a φ A B
8 1 a1i φ B = Base R
9 4 a1i φ N = RingSpan R
10 eqidd φ N A = N A
11 6 8 7 9 10 rgspncl φ N A SubRing R
12 1 subrgss N A SubRing R N A B
13 11 12 syl φ N A B
14 13 sselda φ X N A X B
15 simpr φ g F X = R w Word A g w · ˙ M w X = R w Word A g w · ˙ M w
16 eqid 0 R = 0 R
17 6 ringcmnd φ R CMnd
18 17 adantr φ g F R CMnd
19 1 fvexi B V
20 19 a1i φ B V
21 20 7 ssexd φ A V
22 21 adantr φ g F A V
23 wrdexg A V Word A V
24 22 23 syl φ g F Word A V
25 6 ringgrpd φ R Grp
26 25 ad2antrr φ g F w Word A R Grp
27 zex V
28 27 a1i φ g F V
29 breq1 f = g finSupp 0 f finSupp 0 g
30 29 5 elrab2 g F g Word A finSupp 0 g
31 30 biimpi g F g Word A finSupp 0 g
32 31 simpld g F g Word A
33 32 adantl φ g F g Word A
34 24 28 33 elmaprd φ g F g : Word A
35 34 ffvelcdmda φ g F w Word A g w
36 2 ringmgp R Ring M Mnd
37 6 36 syl φ M Mnd
38 37 ad2antrr φ g F w Word A M Mnd
39 sswrd A B Word A Word B
40 7 39 syl φ Word A Word B
41 40 adantr φ g F Word A Word B
42 41 sselda φ g F w Word A w Word B
43 2 1 mgpbas B = Base M
44 43 gsumwcl M Mnd w Word B M w B
45 38 42 44 syl2anc φ g F w Word A M w B
46 1 3 26 35 45 mulgcld φ g F w Word A g w · ˙ M w B
47 46 fmpttd φ g F w Word A g w · ˙ M w : Word A B
48 34 feqmptd φ g F g = w Word A g w
49 31 simprd g F finSupp 0 g
50 49 adantl φ g F finSupp 0 g
51 48 50 eqbrtrrd φ g F finSupp 0 w Word A g w
52 1 16 3 mulg0 y B 0 · ˙ y = 0 R
53 52 adantl φ g F y B 0 · ˙ y = 0 R
54 fvexd φ g F 0 R V
55 51 53 35 45 54 fsuppssov1 φ g F finSupp 0 R w Word A g w · ˙ M w
56 1 16 18 24 47 55 gsumcl φ g F R w Word A g w · ˙ M w B
57 56 adantr φ g F X = R w Word A g w · ˙ M w R w Word A g w · ˙ M w B
58 15 57 eqeltrd φ g F X = R w Word A g w · ˙ M w X B
59 58 r19.29an φ g F X = R w Word A g w · ˙ M w X B
60 6 adantr φ X B R Ring
61 7 adantr φ X B A B
62 fveq1 h = i h w = i w
63 62 oveq1d h = i h w · ˙ M w = i w · ˙ M w
64 63 mpteq2dv h = i w Word A h w · ˙ M w = w Word A i w · ˙ M w
65 fveq2 w = v i w = i v
66 oveq2 w = v M w = M v
67 65 66 oveq12d w = v i w · ˙ M w = i v · ˙ M v
68 67 cbvmptv w Word A i w · ˙ M w = v Word A i v · ˙ M v
69 64 68 eqtrdi h = i w Word A h w · ˙ M w = v Word A i v · ˙ M v
70 69 oveq2d h = i R w Word A h w · ˙ M w = R v Word A i v · ˙ M v
71 70 cbvmptv h F R w Word A h w · ˙ M w = i F R v Word A i v · ˙ M v
72 71 rneqi ran h F R w Word A h w · ˙ M w = ran i F R v Word A i v · ˙ M v
73 1 2 3 4 5 60 61 72 elrgspnlem4 φ X B N A = ran h F R w Word A h w · ˙ M w
74 73 eleq2d φ X B X N A X ran h F R w Word A h w · ˙ M w
75 fveq1 h = g h w = g w
76 75 oveq1d h = g h w · ˙ M w = g w · ˙ M w
77 76 mpteq2dv h = g w Word A h w · ˙ M w = w Word A g w · ˙ M w
78 77 oveq2d h = g R w Word A h w · ˙ M w = R w Word A g w · ˙ M w
79 78 cbvmptv h F R w Word A h w · ˙ M w = g F R w Word A g w · ˙ M w
80 79 elrnmpt X B X ran h F R w Word A h w · ˙ M w g F X = R w Word A g w · ˙ M w
81 80 adantl φ X B X ran h F R w Word A h w · ˙ M w g F X = R w Word A g w · ˙ M w
82 74 81 bitrd φ X B X N A g F X = R w Word A g w · ˙ M w
83 14 59 82 bibiad φ X N A g F X = R w Word A g w · ˙ M w