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 )
elrgspn.1 
|- ( ph -> X e. 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 elrgspn.1 
 |-  ( ph -> X e. B )
9 fveq1 
 |-  ( h = i -> ( h ` w ) = ( i ` w ) )
10 9 oveq1d 
 |-  ( h = i -> ( ( h ` w ) .x. ( M gsum w ) ) = ( ( i ` w ) .x. ( M gsum w ) ) )
11 10 mpteq2dv 
 |-  ( h = i -> ( w e. Word A |-> ( ( h ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> ( ( i ` w ) .x. ( M gsum w ) ) ) )
12 fveq2 
 |-  ( w = v -> ( i ` w ) = ( i ` v ) )
13 oveq2 
 |-  ( w = v -> ( M gsum w ) = ( M gsum v ) )
14 12 13 oveq12d 
 |-  ( w = v -> ( ( i ` w ) .x. ( M gsum w ) ) = ( ( i ` v ) .x. ( M gsum v ) ) )
15 14 cbvmptv 
 |-  ( w e. Word A |-> ( ( i ` w ) .x. ( M gsum w ) ) ) = ( v e. Word A |-> ( ( i ` v ) .x. ( M gsum v ) ) )
16 11 15 eqtrdi 
 |-  ( h = i -> ( w e. Word A |-> ( ( h ` w ) .x. ( M gsum w ) ) ) = ( v e. Word A |-> ( ( i ` v ) .x. ( M gsum v ) ) ) )
17 16 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 ) ) ) ) )
18 17 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 ) ) ) ) )
19 18 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 ) ) ) ) )
20 1 2 3 4 5 6 7 19 elrgspnlem4 
 |-  ( ph -> ( N ` A ) = ran ( h e. F |-> ( R gsum ( w e. Word A |-> ( ( h ` w ) .x. ( M gsum w ) ) ) ) ) )
21 20 eleq2d 
 |-  ( ph -> ( X e. ( N ` A ) <-> X e. ran ( h e. F |-> ( R gsum ( w e. Word A |-> ( ( h ` w ) .x. ( M gsum w ) ) ) ) ) ) )
22 fveq1 
 |-  ( h = g -> ( h ` w ) = ( g ` w ) )
23 22 oveq1d 
 |-  ( h = g -> ( ( h ` w ) .x. ( M gsum w ) ) = ( ( g ` w ) .x. ( M gsum w ) ) )
24 23 mpteq2dv 
 |-  ( h = g -> ( w e. Word A |-> ( ( h ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) )
25 24 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 ) ) ) ) )
26 25 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 ) ) ) ) )
27 26 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 ) ) ) ) ) )
28 8 27 syl 
 |-  ( ph -> ( 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 ) ) ) ) ) )
29 21 28 bitrd 
 |-  ( ph -> ( X e. ( N ` A ) <-> E. g e. F X = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) )