Metamath Proof Explorer


Theorem gsumccatOLD

Description: Obsolete version of gsumccat as of 13-Jan-2024. Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses gsumwcl.b B = Base G
gsumsgrpccat.p + ˙ = + G
Assertion gsumccatOLD G Mnd W Word B X Word B G W ++ X = G W + ˙ G X

Proof

Step Hyp Ref Expression
1 gsumwcl.b B = Base G
2 gsumsgrpccat.p + ˙ = + G
3 oveq1 W = W ++ X = ++ X
4 3 oveq2d W = G W ++ X = G ++ X
5 oveq2 W = G W = G
6 eqid 0 G = 0 G
7 6 gsum0 G = 0 G
8 5 7 eqtrdi W = G W = 0 G
9 8 oveq1d W = G W + ˙ G X = 0 G + ˙ G X
10 4 9 eqeq12d W = G W ++ X = G W + ˙ G X G ++ X = 0 G + ˙ G X
11 oveq2 X = W ++ X = W ++
12 11 oveq2d X = G W ++ X = G W ++
13 oveq2 X = G X = G
14 13 7 eqtrdi X = G X = 0 G
15 14 oveq2d X = G W + ˙ G X = G W + ˙ 0 G
16 12 15 eqeq12d X = G W ++ X = G W + ˙ G X G W ++ = G W + ˙ 0 G
17 simpl1 G Mnd W Word B X Word B W X G Mnd
18 lennncl W Word B W W
19 18 3ad2antl2 G Mnd W Word B X Word B W W
20 19 adantrr G Mnd W Word B X Word B W X W
21 lennncl X Word B X X
22 21 3ad2antl3 G Mnd W Word B X Word B X X
23 22 adantrl G Mnd W Word B X Word B W X X
24 20 23 nnaddcld G Mnd W Word B X Word B W X W + X
25 nnm1nn0 W + X W + X - 1 0
26 24 25 syl G Mnd W Word B X Word B W X W + X - 1 0
27 nn0uz 0 = 0
28 26 27 eleqtrdi G Mnd W Word B X Word B W X W + X - 1 0
29 simpl2 G Mnd W Word B X Word B W X W Word B
30 simpl3 G Mnd W Word B X Word B W X X Word B
31 ccatcl W Word B X Word B W ++ X Word B
32 29 30 31 syl2anc G Mnd W Word B X Word B W X W ++ X Word B
33 wrdf W ++ X Word B W ++ X : 0 ..^ W ++ X B
34 32 33 syl G Mnd W Word B X Word B W X W ++ X : 0 ..^ W ++ X B
35 ccatlen W Word B X Word B W ++ X = W + X
36 29 30 35 syl2anc G Mnd W Word B X Word B W X W ++ X = W + X
37 36 oveq2d G Mnd W Word B X Word B W X 0 ..^ W ++ X = 0 ..^ W + X
38 20 nnzd G Mnd W Word B X Word B W X W
39 23 nnzd G Mnd W Word B X Word B W X X
40 38 39 zaddcld G Mnd W Word B X Word B W X W + X
41 fzoval W + X 0 ..^ W + X = 0 W + X - 1
42 40 41 syl G Mnd W Word B X Word B W X 0 ..^ W + X = 0 W + X - 1
43 37 42 eqtrd G Mnd W Word B X Word B W X 0 ..^ W ++ X = 0 W + X - 1
44 43 feq2d G Mnd W Word B X Word B W X W ++ X : 0 ..^ W ++ X B W ++ X : 0 W + X - 1 B
45 34 44 mpbid G Mnd W Word B X Word B W X W ++ X : 0 W + X - 1 B
46 1 2 17 28 45 gsumval2 G Mnd W Word B X Word B W X G W ++ X = seq 0 + ˙ W ++ X W + X - 1
47 nnm1nn0 W W 1 0
48 20 47 syl G Mnd W Word B X Word B W X W 1 0
49 48 27 eleqtrdi G Mnd W Word B X Word B W X W 1 0
50 wrdf W Word B W : 0 ..^ W B
51 29 50 syl G Mnd W Word B X Word B W X W : 0 ..^ W B
52 fzoval W 0 ..^ W = 0 W 1
53 38 52 syl G Mnd W Word B X Word B W X 0 ..^ W = 0 W 1
54 53 feq2d G Mnd W Word B X Word B W X W : 0 ..^ W B W : 0 W 1 B
55 51 54 mpbid G Mnd W Word B X Word B W X W : 0 W 1 B
56 1 2 17 49 55 gsumval2 G Mnd W Word B X Word B W X G W = seq 0 + ˙ W W 1
57 nnm1nn0 X X 1 0
58 23 57 syl G Mnd W Word B X Word B W X X 1 0
59 58 27 eleqtrdi G Mnd W Word B X Word B W X X 1 0
60 wrdf X Word B X : 0 ..^ X B
61 30 60 syl G Mnd W Word B X Word B W X X : 0 ..^ X B
62 fzoval X 0 ..^ X = 0 X 1
63 39 62 syl G Mnd W Word B X Word B W X 0 ..^ X = 0 X 1
64 63 feq2d G Mnd W Word B X Word B W X X : 0 ..^ X B X : 0 X 1 B
65 61 64 mpbid G Mnd W Word B X Word B W X X : 0 X 1 B
66 1 2 17 59 65 gsumval2 G Mnd W Word B X Word B W X G X = seq 0 + ˙ X X 1
67 56 66 oveq12d G Mnd W Word B X Word B W X G W + ˙ G X = seq 0 + ˙ W W 1 + ˙ seq 0 + ˙ X X 1
68 1 2 mndcl G Mnd x B y B x + ˙ y B
69 68 3expb G Mnd x B y B x + ˙ y B
70 17 69 sylan G Mnd W Word B X Word B W X x B y B x + ˙ y B
71 1 2 mndass G Mnd x B y B z B x + ˙ y + ˙ z = x + ˙ y + ˙ z
72 17 71 sylan G Mnd W Word B X Word B W X x B y B z B x + ˙ y + ˙ z = x + ˙ y + ˙ z
73 uzid W W W
74 38 73 syl G Mnd W Word B X Word B W X W W
75 uzaddcl W W X 1 0 W + X - 1 W
76 74 58 75 syl2anc G Mnd W Word B X Word B W X W + X - 1 W
77 20 nncnd G Mnd W Word B X Word B W X W
78 23 nncnd G Mnd W Word B X Word B W X X
79 1cnd G Mnd W Word B X Word B W X 1
80 77 78 79 addsubassd G Mnd W Word B X Word B W X W + X - 1 = W + X - 1
81 ax-1cn 1
82 npcan W 1 W - 1 + 1 = W
83 77 81 82 sylancl G Mnd W Word B X Word B W X W - 1 + 1 = W
84 83 fveq2d G Mnd W Word B X Word B W X W - 1 + 1 = W
85 76 80 84 3eltr4d G Mnd W Word B X Word B W X W + X - 1 W - 1 + 1
86 45 ffvelrnda G Mnd W Word B X Word B W X x 0 W + X - 1 W ++ X x B
87 70 72 85 49 86 seqsplit G Mnd W Word B X Word B W X seq 0 + ˙ W ++ X W + X - 1 = seq 0 + ˙ W ++ X W 1 + ˙ seq W - 1 + 1 + ˙ W ++ X W + X - 1
88 simpll2 G Mnd W Word B X Word B W X x 0 W 1 W Word B
89 simpll3 G Mnd W Word B X Word B W X x 0 W 1 X Word B
90 53 eleq2d G Mnd W Word B X Word B W X x 0 ..^ W x 0 W 1
91 90 biimpar G Mnd W Word B X Word B W X x 0 W 1 x 0 ..^ W
92 ccatval1 W Word B X Word B x 0 ..^ W W ++ X x = W x
93 88 89 91 92 syl3anc G Mnd W Word B X Word B W X x 0 W 1 W ++ X x = W x
94 49 93 seqfveq G Mnd W Word B X Word B W X seq 0 + ˙ W ++ X W 1 = seq 0 + ˙ W W 1
95 77 addid2d G Mnd W Word B X Word B W X 0 + W = W
96 83 95 eqtr4d G Mnd W Word B X Word B W X W - 1 + 1 = 0 + W
97 96 seqeq1d G Mnd W Word B X Word B W X seq W - 1 + 1 + ˙ W ++ X = seq 0 + W + ˙ W ++ X
98 77 78 addcomd G Mnd W Word B X Word B W X W + X = X + W
99 98 oveq1d G Mnd W Word B X Word B W X W + X - 1 = X + W - 1
100 78 77 79 addsubd G Mnd W Word B X Word B W X X + W - 1 = X - 1 + W
101 99 100 eqtrd G Mnd W Word B X Word B W X W + X - 1 = X - 1 + W
102 97 101 fveq12d G Mnd W Word B X Word B W X seq W - 1 + 1 + ˙ W ++ X W + X - 1 = seq 0 + W + ˙ W ++ X X - 1 + W
103 simpll2 G Mnd W Word B X Word B W X x 0 X 1 W Word B
104 simpll3 G Mnd W Word B X Word B W X x 0 X 1 X Word B
105 63 eleq2d G Mnd W Word B X Word B W X x 0 ..^ X x 0 X 1
106 105 biimpar G Mnd W Word B X Word B W X x 0 X 1 x 0 ..^ X
107 ccatval3 W Word B X Word B x 0 ..^ X W ++ X x + W = X x
108 103 104 106 107 syl3anc G Mnd W Word B X Word B W X x 0 X 1 W ++ X x + W = X x
109 108 eqcomd G Mnd W Word B X Word B W X x 0 X 1 X x = W ++ X x + W
110 59 38 109 seqshft2 G Mnd W Word B X Word B W X seq 0 + ˙ X X 1 = seq 0 + W + ˙ W ++ X X - 1 + W
111 102 110 eqtr4d G Mnd W Word B X Word B W X seq W - 1 + 1 + ˙ W ++ X W + X - 1 = seq 0 + ˙ X X 1
112 94 111 oveq12d G Mnd W Word B X Word B W X seq 0 + ˙ W ++ X W 1 + ˙ seq W - 1 + 1 + ˙ W ++ X W + X - 1 = seq 0 + ˙ W W 1 + ˙ seq 0 + ˙ X X 1
113 87 112 eqtrd G Mnd W Word B X Word B W X seq 0 + ˙ W ++ X W + X - 1 = seq 0 + ˙ W W 1 + ˙ seq 0 + ˙ X X 1
114 67 113 eqtr4d G Mnd W Word B X Word B W X G W + ˙ G X = seq 0 + ˙ W ++ X W + X - 1
115 46 114 eqtr4d G Mnd W Word B X Word B W X G W ++ X = G W + ˙ G X
116 115 anassrs G Mnd W Word B X Word B W X G W ++ X = G W + ˙ G X
117 simpl2 G Mnd W Word B X Word B W W Word B
118 ccatrid W Word B W ++ = W
119 117 118 syl G Mnd W Word B X Word B W W ++ = W
120 119 oveq2d G Mnd W Word B X Word B W G W ++ = G W
121 simpl1 G Mnd W Word B X Word B W G Mnd
122 1 gsumwcl G Mnd W Word B G W B
123 122 3adant3 G Mnd W Word B X Word B G W B
124 123 adantr G Mnd W Word B X Word B W G W B
125 1 2 6 mndrid G Mnd G W B G W + ˙ 0 G = G W
126 121 124 125 syl2anc G Mnd W Word B X Word B W G W + ˙ 0 G = G W
127 120 126 eqtr4d G Mnd W Word B X Word B W G W ++ = G W + ˙ 0 G
128 16 116 127 pm2.61ne G Mnd W Word B X Word B W G W ++ X = G W + ˙ G X
129 ccatlid X Word B ++ X = X
130 129 3ad2ant3 G Mnd W Word B X Word B ++ X = X
131 130 oveq2d G Mnd W Word B X Word B G ++ X = G X
132 simp1 G Mnd W Word B X Word B G Mnd
133 1 gsumwcl G Mnd X Word B G X B
134 1 2 6 mndlid G Mnd G X B 0 G + ˙ G X = G X
135 132 133 134 3imp3i2an G Mnd W Word B X Word B 0 G + ˙ G X = G X
136 131 135 eqtr4d G Mnd W Word B X Word B G ++ X = 0 G + ˙ G X
137 10 128 136 pm2.61ne G Mnd W Word B X Word B G W ++ X = G W + ˙ G X