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 
|- .x. = ( .g ` R )
elrgspn.n 
|- N = ( RingSpan ` R )
elrgspn.f 
|- F = { f e. ( ZZ ^m Word A ) | f finSupp 0 }
elrgspn.r 
|- ( ph -> R e. Ring )
elrgspn.a 
|- ( ph -> A C_ B )
Assertion elrgspn 
|- ( ph -> ( X e. ( N ` A ) <-> E. g e. F X = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) )

Proof

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