Metamath Proof Explorer

Theorem elrgspnlem3

Description: Lemma for elrgspn . (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 )
elrgspnlem1.1 
|- S = ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
Assertion elrgspnlem3 
|- ( ph -> A C_ S )

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 elrgspnlem1.1 
 |-  S = ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
9 eqid 
 |-  ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) = ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
10 fveq1 
 |-  ( g = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) -> ( g ` w ) = ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) )
11 10 oveq1d 
 |-  ( g = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) -> ( ( g ` w ) .x. ( M gsum w ) ) = ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) )
12 11 mpteq2dv 
 |-  ( g = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) -> ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) ) )
13 12 oveq2d 
 |-  ( g = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) -> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. Word A |-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) ) ) )
14 13 eqeq2d 
 |-  ( g = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) -> ( x = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) <-> x = ( R gsum ( w e. Word A |-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) ) ) ) )
15 breq1 
 |-  ( f = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) -> ( f finSupp 0 <-> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) finSupp 0 ) )
16 zex 
 |-  ZZ e. _V
17 16 a1i 
 |-  ( ( ph /\ x e. A ) -> ZZ e. _V )
18 1 fvexi 
 |-  B e. _V
19 18 a1i 
 |-  ( ph -> B e. _V )
20 19 7 ssexd 
 |-  ( ph -> A e. _V )
21 wrdexg 
 |-  ( A e. _V -> Word A e. _V )
22 20 21 syl 
 |-  ( ph -> Word A e. _V )
23 22 adantr 
 |-  ( ( ph /\ x e. A ) -> Word A e. _V )
24 1zzd 
 |-  ( ( ( ( ph /\ x e. A ) /\ v e. Word A ) /\ v = <" x "> ) -> 1 e. ZZ )
25 0zd 
 |-  ( ( ( ( ph /\ x e. A ) /\ v e. Word A ) /\ -. v = <" x "> ) -> 0 e. ZZ )
26 24 25 ifclda 
 |-  ( ( ( ph /\ x e. A ) /\ v e. Word A ) -> if ( v = <" x "> , 1 , 0 ) e. ZZ )
27 26 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) : Word A --> ZZ )
28 17 23 27 elmapdd 
 |-  ( ( ph /\ x e. A ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) e. ( ZZ ^m Word A ) )
29 28 elexd 
 |-  ( ( ph /\ x e. A ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) e. _V )
30 27 ffund 
 |-  ( ( ph /\ x e. A ) -> Fun ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) )
31 0zd 
 |-  ( ( ph /\ x e. A ) -> 0 e. ZZ )
32 snfi 
 |-  { <" x "> } e. Fin
33 32 a1i 
 |-  ( ( ph /\ x e. A ) -> { <" x "> } e. Fin )
34 eldifsni 
 |-  ( v e. ( Word A \ { <" x "> } ) -> v =/= <" x "> )
35 34 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ v e. ( Word A \ { <" x "> } ) ) -> v =/= <" x "> )
36 35 neneqd 
 |-  ( ( ( ph /\ x e. A ) /\ v e. ( Word A \ { <" x "> } ) ) -> -. v = <" x "> )
37 36 iffalsed 
 |-  ( ( ( ph /\ x e. A ) /\ v e. ( Word A \ { <" x "> } ) ) -> if ( v = <" x "> , 1 , 0 ) = 0 )
38 37 23 suppss2 
 |-  ( ( ph /\ x e. A ) -> ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) supp 0 ) C_ { <" x "> } )
39 suppssfifsupp 
 |-  ( ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) e. _V /\ Fun ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) /\ 0 e. ZZ ) /\ ( { <" x "> } e. Fin /\ ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) supp 0 ) C_ { <" x "> } ) ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) finSupp 0 )
40 29 30 31 33 38 39 syl32anc 
 |-  ( ( ph /\ x e. A ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) finSupp 0 )
41 15 28 40 elrabd 
 |-  ( ( ph /\ x e. A ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) e. { f e. ( ZZ ^m Word A ) | f finSupp 0 } )
42 41 5 eleqtrrdi 
 |-  ( ( ph /\ x e. A ) -> ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) e. F )
43 eqeq2 
 |-  ( x = if ( w = <" x "> , x , ( 0g ` R ) ) -> ( ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = x <-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = if ( w = <" x "> , x , ( 0g ` R ) ) ) )
44 eqeq2 
 |-  ( ( 0g ` R ) = if ( w = <" x "> , x , ( 0g ` R ) ) -> ( ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = ( 0g ` R ) <-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = if ( w = <" x "> , x , ( 0g ` R ) ) ) )
45 eqid 
 |-  ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) = ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) )
46 simpr 
 |-  ( ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) /\ v = w ) -> v = w )
47 simplr 
 |-  ( ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) /\ v = w ) -> w = <" x "> )
48 46 47 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) /\ v = w ) -> v = <" x "> )
49 48 iftrued 
 |-  ( ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) /\ v = w ) -> if ( v = <" x "> , 1 , 0 ) = 1 )
50 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> w e. Word A )
51 1zzd 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> 1 e. ZZ )
52 45 49 50 51 fvmptd2 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) = 1 )
53 simpr 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> w = <" x "> )
54 53 oveq2d 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( M gsum w ) = ( M gsum <" x "> ) )
55 7 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. B )
56 55 ad2antrr 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> x e. B )
57 2 1 mgpbas 
 |-  B = ( Base ` M )
58 57 gsumws1 
 |-  ( x e. B -> ( M gsum <" x "> ) = x )
59 56 58 syl 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( M gsum <" x "> ) = x )
60 54 59 eqtrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( M gsum w ) = x )
61 52 60 oveq12d 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = ( 1 .x. x ) )
62 1 3 mulg1 
 |-  ( x e. B -> ( 1 .x. x ) = x )
63 56 62 syl 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( 1 .x. x ) = x )
64 61 63 eqtrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ w = <" x "> ) -> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = x )
65 eqeq1 
 |-  ( v = w -> ( v = <" x "> <-> w = <" x "> ) )
66 65 notbid 
 |-  ( v = w -> ( -. v = <" x "> <-> -. w = <" x "> ) )
67 66 biimparc 
 |-  ( ( -. w = <" x "> /\ v = w ) -> -. v = <" x "> )
68 67 adantll 
 |-  ( ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) /\ v = w ) -> -. v = <" x "> )
69 68 iffalsed 
 |-  ( ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) /\ v = w ) -> if ( v = <" x "> , 1 , 0 ) = 0 )
70 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> w e. Word A )
71 0zd 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> 0 e. ZZ )
72 45 69 70 71 fvmptd2 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) = 0 )
73 72 oveq1d 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = ( 0 .x. ( M gsum w ) ) )
74 2 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
75 6 74 syl 
 |-  ( ph -> M e. Mnd )
76 75 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> M e. Mnd )
77 sswrd 
 |-  ( A C_ B -> Word A C_ Word B )
78 7 77 syl 
 |-  ( ph -> Word A C_ Word B )
79 78 adantr 
 |-  ( ( ph /\ x e. A ) -> Word A C_ Word B )
80 79 sselda 
 |-  ( ( ( ph /\ x e. A ) /\ w e. Word A ) -> w e. Word B )
81 80 adantr 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> w e. Word B )
82 57 gsumwcl 
 |-  ( ( M e. Mnd /\ w e. Word B ) -> ( M gsum w ) e. B )
83 76 81 82 syl2anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> ( M gsum w ) e. B )
84 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
85 1 84 3 mulg0 
 |-  ( ( M gsum w ) e. B -> ( 0 .x. ( M gsum w ) ) = ( 0g ` R ) )
86 83 85 syl 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> ( 0 .x. ( M gsum w ) ) = ( 0g ` R ) )
87 73 86 eqtrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ w e. Word A ) /\ -. w = <" x "> ) -> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = ( 0g ` R ) )
88 43 44 64 87 ifbothda 
 |-  ( ( ( ph /\ x e. A ) /\ w e. Word A ) -> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) = if ( w = <" x "> , x , ( 0g ` R ) ) )
89 88 mpteq2dva 
 |-  ( ( ph /\ x e. A ) -> ( w e. Word A |-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> if ( w = <" x "> , x , ( 0g ` R ) ) ) )
90 89 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( R gsum ( w e. Word A |-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. Word A |-> if ( w = <" x "> , x , ( 0g ` R ) ) ) ) )
91 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
92 6 91 syl 
 |-  ( ph -> R e. Mnd )
93 92 adantr 
 |-  ( ( ph /\ x e. A ) -> R e. Mnd )
94 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
95 94 s1cld 
 |-  ( ( ph /\ x e. A ) -> <" x "> e. Word A )
96 eqid 
 |-  ( w e. Word A |-> if ( w = <" x "> , x , ( 0g ` R ) ) ) = ( w e. Word A |-> if ( w = <" x "> , x , ( 0g ` R ) ) )
97 7 1 sseqtrdi 
 |-  ( ph -> A C_ ( Base ` R ) )
98 97 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. ( Base ` R ) )
99 84 93 23 95 96 98 gsummptif1n0 
 |-  ( ( ph /\ x e. A ) -> ( R gsum ( w e. Word A |-> if ( w = <" x "> , x , ( 0g ` R ) ) ) ) = x )
100 90 99 eqtr2d 
 |-  ( ( ph /\ x e. A ) -> x = ( R gsum ( w e. Word A |-> ( ( ( v e. Word A |-> if ( v = <" x "> , 1 , 0 ) ) ` w ) .x. ( M gsum w ) ) ) ) )
101 14 42 100 rspcedvdw 
 |-  ( ( ph /\ x e. A ) -> E. g e. F x = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
102 9 101 94 elrnmptd 
 |-  ( ( ph /\ x e. A ) -> x e. ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) )
103 102 8 eleqtrrdi 
 |-  ( ( ph /\ x e. A ) -> x e. S )
104 103 ex 
 |-  ( ph -> ( x e. A -> x e. S ) )
105 104 ssrdv 
 |-  ( ph -> A C_ S )