Metamath Proof Explorer

Theorem gsumwun

Description: In a commutative ring, a group sum of a word W of characters taken from two submonoids E and F can be written as a simple sum. (Contributed by Thierry Arnoux, 6-Oct-2025)

Ref Expression
Hypotheses gsumwun.p 
|- .+ = ( +g ` M )
gsumwun.m 
|- ( ph -> M e. CMnd )
gsumwun.e 
|- ( ph -> E e. ( SubMnd ` M ) )
gsumwun.f 
|- ( ph -> F e. ( SubMnd ` M ) )
gsumwun.w 
|- ( ph -> W e. Word ( E u. F ) )
Assertion gsumwun 
|- ( ph -> E. e e. E E. f e. F ( M gsum W ) = ( e .+ f ) )

Proof

Step Hyp Ref Expression
1 gsumwun.p 
 |-  .+ = ( +g ` M )
2 gsumwun.m 
 |-  ( ph -> M e. CMnd )
3 gsumwun.e 
 |-  ( ph -> E e. ( SubMnd ` M ) )
4 gsumwun.f 
 |-  ( ph -> F e. ( SubMnd ` M ) )
5 gsumwun.w 
 |-  ( ph -> W e. Word ( E u. F ) )
6 oveq2 
 |-  ( v = (/) -> ( M gsum v ) = ( M gsum (/) ) )
7 6 eqeq1d 
 |-  ( v = (/) -> ( ( M gsum v ) = ( e .+ f ) <-> ( M gsum (/) ) = ( e .+ f ) ) )
8 7 2rexbidv 
 |-  ( v = (/) -> ( E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) <-> E. e e. E E. f e. F ( M gsum (/) ) = ( e .+ f ) ) )
9 8 imbi2d 
 |-  ( v = (/) -> ( ( ph -> E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) ) <-> ( ph -> E. e e. E E. f e. F ( M gsum (/) ) = ( e .+ f ) ) ) )
10 oveq2 
 |-  ( v = w -> ( M gsum v ) = ( M gsum w ) )
11 10 eqeq1d 
 |-  ( v = w -> ( ( M gsum v ) = ( e .+ f ) <-> ( M gsum w ) = ( e .+ f ) ) )
12 11 2rexbidv 
 |-  ( v = w -> ( E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) <-> E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) ) )
13 12 imbi2d 
 |-  ( v = w -> ( ( ph -> E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) ) <-> ( ph -> E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) ) ) )
14 oveq1 
 |-  ( e = i -> ( e .+ f ) = ( i .+ f ) )
15 14 eqeq2d 
 |-  ( e = i -> ( ( M gsum v ) = ( e .+ f ) <-> ( M gsum v ) = ( i .+ f ) ) )
16 oveq2 
 |-  ( f = j -> ( i .+ f ) = ( i .+ j ) )
17 16 eqeq2d 
 |-  ( f = j -> ( ( M gsum v ) = ( i .+ f ) <-> ( M gsum v ) = ( i .+ j ) ) )
18 15 17 cbvrex2vw 
 |-  ( E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) <-> E. i e. E E. j e. F ( M gsum v ) = ( i .+ j ) )
19 oveq2 
 |-  ( v = ( w ++ <" x "> ) -> ( M gsum v ) = ( M gsum ( w ++ <" x "> ) ) )
20 19 eqeq1d 
 |-  ( v = ( w ++ <" x "> ) -> ( ( M gsum v ) = ( i .+ j ) <-> ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) )
21 20 2rexbidv 
 |-  ( v = ( w ++ <" x "> ) -> ( E. i e. E E. j e. F ( M gsum v ) = ( i .+ j ) <-> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) )
22 18 21 bitrid 
 |-  ( v = ( w ++ <" x "> ) -> ( E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) <-> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) )
23 22 imbi2d 
 |-  ( v = ( w ++ <" x "> ) -> ( ( ph -> E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) ) <-> ( ph -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) ) )
24 oveq2 
 |-  ( v = W -> ( M gsum v ) = ( M gsum W ) )
25 24 eqeq1d 
 |-  ( v = W -> ( ( M gsum v ) = ( e .+ f ) <-> ( M gsum W ) = ( e .+ f ) ) )
26 25 2rexbidv 
 |-  ( v = W -> ( E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) <-> E. e e. E E. f e. F ( M gsum W ) = ( e .+ f ) ) )
27 26 imbi2d 
 |-  ( v = W -> ( ( ph -> E. e e. E E. f e. F ( M gsum v ) = ( e .+ f ) ) <-> ( ph -> E. e e. E E. f e. F ( M gsum W ) = ( e .+ f ) ) ) )
28 oveq1 
 |-  ( e = ( 0g ` M ) -> ( e .+ f ) = ( ( 0g ` M ) .+ f ) )
29 28 eqeq2d 
 |-  ( e = ( 0g ` M ) -> ( ( M gsum (/) ) = ( e .+ f ) <-> ( M gsum (/) ) = ( ( 0g ` M ) .+ f ) ) )
30 oveq2 
 |-  ( f = ( 0g ` M ) -> ( ( 0g ` M ) .+ f ) = ( ( 0g ` M ) .+ ( 0g ` M ) ) )
31 30 eqeq2d 
 |-  ( f = ( 0g ` M ) -> ( ( M gsum (/) ) = ( ( 0g ` M ) .+ f ) <-> ( M gsum (/) ) = ( ( 0g ` M ) .+ ( 0g ` M ) ) ) )
32 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
33 32 subm0cl 
 |-  ( E e. ( SubMnd ` M ) -> ( 0g ` M ) e. E )
34 3 33 syl 
 |-  ( ph -> ( 0g ` M ) e. E )
35 32 subm0cl 
 |-  ( F e. ( SubMnd ` M ) -> ( 0g ` M ) e. F )
36 4 35 syl 
 |-  ( ph -> ( 0g ` M ) e. F )
37 32 gsum0 
 |-  ( M gsum (/) ) = ( 0g ` M )
38 2 cmnmndd 
 |-  ( ph -> M e. Mnd )
39 eqid 
 |-  ( Base ` M ) = ( Base ` M )
40 39 32 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. ( Base ` M ) )
41 39 1 32 mndlid 
 |-  ( ( M e. Mnd /\ ( 0g ` M ) e. ( Base ` M ) ) -> ( ( 0g ` M ) .+ ( 0g ` M ) ) = ( 0g ` M ) )
42 38 40 41 syl2anc2 
 |-  ( ph -> ( ( 0g ` M ) .+ ( 0g ` M ) ) = ( 0g ` M ) )
43 37 42 eqtr4id 
 |-  ( ph -> ( M gsum (/) ) = ( ( 0g ` M ) .+ ( 0g ` M ) ) )
44 29 31 34 36 43 2rspcedvdw 
 |-  ( ph -> E. e e. E E. f e. F ( M gsum (/) ) = ( e .+ f ) )
45 oveq1 
 |-  ( i = ( e .+ x ) -> ( i .+ j ) = ( ( e .+ x ) .+ j ) )
46 45 eqeq2d 
 |-  ( i = ( e .+ x ) -> ( ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) <-> ( M gsum ( w ++ <" x "> ) ) = ( ( e .+ x ) .+ j ) ) )
47 oveq2 
 |-  ( j = f -> ( ( e .+ x ) .+ j ) = ( ( e .+ x ) .+ f ) )
48 47 eqeq2d 
 |-  ( j = f -> ( ( M gsum ( w ++ <" x "> ) ) = ( ( e .+ x ) .+ j ) <-> ( M gsum ( w ++ <" x "> ) ) = ( ( e .+ x ) .+ f ) ) )
49 3 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> E e. ( SubMnd ` M ) )
50 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> e e. E )
51 simpr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> x e. E )
52 1 49 50 51 submcld 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> ( e .+ x ) e. E )
53 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> f e. F )
54 38 ad5antr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> M e. Mnd )
55 39 submss 
 |-  ( E e. ( SubMnd ` M ) -> E C_ ( Base ` M ) )
56 3 55 syl 
 |-  ( ph -> E C_ ( Base ` M ) )
57 39 submss 
 |-  ( F e. ( SubMnd ` M ) -> F C_ ( Base ` M ) )
58 4 57 syl 
 |-  ( ph -> F C_ ( Base ` M ) )
59 56 58 unssd 
 |-  ( ph -> ( E u. F ) C_ ( Base ` M ) )
60 sswrd 
 |-  ( ( E u. F ) C_ ( Base ` M ) -> Word ( E u. F ) C_ Word ( Base ` M ) )
61 59 60 syl 
 |-  ( ph -> Word ( E u. F ) C_ Word ( Base ` M ) )
62 61 sselda 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> w e. Word ( Base ` M ) )
63 62 ad4antr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> w e. Word ( Base ` M ) )
64 59 adantr 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> ( E u. F ) C_ ( Base ` M ) )
65 64 sselda 
 |-  ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) -> x e. ( Base ` M ) )
66 65 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> x e. ( Base ` M ) )
67 39 1 gsumccatsn 
 |-  ( ( M e. Mnd /\ w e. Word ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( M gsum ( w ++ <" x "> ) ) = ( ( M gsum w ) .+ x ) )
68 54 63 66 67 syl3anc 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( M gsum ( w ++ <" x "> ) ) = ( ( M gsum w ) .+ x ) )
69 simpr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( M gsum w ) = ( e .+ f ) )
70 69 oveq1d 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( ( M gsum w ) .+ x ) = ( ( e .+ f ) .+ x ) )
71 56 ad2antrr 
 |-  ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) -> E C_ ( Base ` M ) )
72 71 sselda 
 |-  ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) -> e e. ( Base ` M ) )
73 72 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> e e. ( Base ` M ) )
74 58 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) -> F C_ ( Base ` M ) )
75 74 sselda 
 |-  ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) -> f e. ( Base ` M ) )
76 75 adantr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> f e. ( Base ` M ) )
77 2 ad5antr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> M e. CMnd )
78 39 1 cmncom 
 |-  ( ( M e. CMnd /\ f e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( f .+ x ) = ( x .+ f ) )
79 77 76 66 78 syl3anc 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( f .+ x ) = ( x .+ f ) )
80 39 1 54 73 76 66 79 mnd32g 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( ( e .+ f ) .+ x ) = ( ( e .+ x ) .+ f ) )
81 68 70 80 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( M gsum ( w ++ <" x "> ) ) = ( ( e .+ x ) .+ f ) )
82 81 adantr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> ( M gsum ( w ++ <" x "> ) ) = ( ( e .+ x ) .+ f ) )
83 46 48 52 53 82 2rspcedvdw 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. E ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) )
84 oveq1 
 |-  ( i = e -> ( i .+ j ) = ( e .+ j ) )
85 84 eqeq2d 
 |-  ( i = e -> ( ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) <-> ( M gsum ( w ++ <" x "> ) ) = ( e .+ j ) ) )
86 oveq2 
 |-  ( j = ( f .+ x ) -> ( e .+ j ) = ( e .+ ( f .+ x ) ) )
87 86 eqeq2d 
 |-  ( j = ( f .+ x ) -> ( ( M gsum ( w ++ <" x "> ) ) = ( e .+ j ) <-> ( M gsum ( w ++ <" x "> ) ) = ( e .+ ( f .+ x ) ) ) )
88 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> e e. E )
89 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> F e. ( SubMnd ` M ) )
90 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> f e. F )
91 simpr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> x e. F )
92 1 89 90 91 submcld 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> ( f .+ x ) e. F )
93 39 1 54 73 76 66 mndassd 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( ( e .+ f ) .+ x ) = ( e .+ ( f .+ x ) ) )
94 68 70 93 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( M gsum ( w ++ <" x "> ) ) = ( e .+ ( f .+ x ) ) )
95 94 adantr 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> ( M gsum ( w ++ <" x "> ) ) = ( e .+ ( f .+ x ) ) )
96 85 87 88 92 95 2rspcedvdw 
 |-  ( ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) /\ x e. F ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) )
97 elun 
 |-  ( x e. ( E u. F ) <-> ( x e. E \/ x e. F ) )
98 97 biimpi 
 |-  ( x e. ( E u. F ) -> ( x e. E \/ x e. F ) )
99 98 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> ( x e. E \/ x e. F ) )
100 83 96 99 mpjaodan 
 |-  ( ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( M gsum w ) = ( e .+ f ) ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) )
101 100 r19.29ffa 
 |-  ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) /\ E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) )
102 101 ex 
 |-  ( ( ( ph /\ w e. Word ( E u. F ) ) /\ x e. ( E u. F ) ) -> ( E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) )
103 102 expl 
 |-  ( ph -> ( ( w e. Word ( E u. F ) /\ x e. ( E u. F ) ) -> ( E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) ) )
104 103 com12 
 |-  ( ( w e. Word ( E u. F ) /\ x e. ( E u. F ) ) -> ( ph -> ( E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) ) )
105 104 a2d 
 |-  ( ( w e. Word ( E u. F ) /\ x e. ( E u. F ) ) -> ( ( ph -> E. e e. E E. f e. F ( M gsum w ) = ( e .+ f ) ) -> ( ph -> E. i e. E E. j e. F ( M gsum ( w ++ <" x "> ) ) = ( i .+ j ) ) ) )
106 9 13 23 27 44 105 wrdind 
 |-  ( W e. Word ( E u. F ) -> ( ph -> E. e e. E E. f e. F ( M gsum W ) = ( e .+ f ) ) )
107 5 106 mpcom 
 |-  ( ph -> E. e e. E E. f e. F ( M gsum W ) = ( e .+ f ) )