Theorem cpmadugsumlemF 20681

Description: Lemma F for cpmadugsum 20683. (Contributed by AV, 7-Nov-2019.)

Hypotheses

Ref	Expression
cpmadugsum.a	|- A = ( N Mat R )
cpmadugsum.b	|- B = ( Base ` A )
cpmadugsum.p	|- P = (Poly1 ` R )
cpmadugsum.y	|- Y = ( N Mat P )
cpmadugsum.t	|- T = ( N matToPolyMat R )
cpmadugsum.x	|- X = (var1 ` R )
cpmadugsum.e	|- .^ = (.g ` (mulGrp ` P ) )
cpmadugsum.m	|- .x. = ( .s ` Y )
cpmadugsum.r	|- .X. = ( .r ` Y )
cpmadugsum.1	|- .1. = ( 1r ` Y )
cpmadugsum.g	|- .+ = ( +g ` Y )
cpmadugsum.s	|- .- = ( -g ` Y )

Assertion

Ref

Expression

cpmadugsumlemF

|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )

Distinct variable groups:   B, i   i, M   i, N   R, i   i, X   i, Y   .X. , i   .x. , i   .1. , i   i, b   i, s   T, i   .^ , i   .- , i

Allowed substitution hints:   A( i, s, b)   B( s, b)   P( i, s, b)   .+ ( i, s, b)   R( s, b)   T( s, b)   .x. ( s, b)   .X. ( s, b)   .1. ( s, b)   .^ ( s, b)   M( s, b)   .- ( s, b)   N( s, b)   X( s, b)   Y( s, b)

Proof of Theorem cpmadugsumlemF

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnnn0 11299	. . . 4 |- ( s e. NN -> s e. NN0 )
2		cpmadugsum.a	. . . . 5 |- A = ( N Mat R )
3		cpmadugsum.b	. . . . 5 |- B = ( Base ` A )
4		cpmadugsum.p	. . . . 5 |- P = (Poly1 ` R )
5		cpmadugsum.y	. . . . 5 |- Y = ( N Mat P )
6		cpmadugsum.t	. . . . 5 |- T = ( N matToPolyMat R )
7		cpmadugsum.x	. . . . 5 |- X = (var1 ` R )
8		cpmadugsum.e	. . . . 5 |- .^ = (.g ` (mulGrp ` P ) )
9		cpmadugsum.m	. . . . 5 |- .x. = ( .s ` Y )
10		cpmadugsum.r	. . . . 5 |- .X. = ( .r ` Y )
11		cpmadugsum.1	. . . . 5 |- .1. = ( 1r ` Y )
12	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	cpmadugsumlemB 20679	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( X .x. .1. ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
13	1, 12	sylanr1 684	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( X .x. .1. ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
14	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	cpmadugsumlemC 20680	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
15	1, 14	sylanr1 684	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
16	13, 15	oveq12d 6668	. 2 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
17		nncn 11028	. . . . . . . . 9 |- ( s e. NN -> s e. CC )
18		npcan1 10455	. . . . . . . . . 10 |- ( s e. CC -> ( ( s - 1 ) + 1 ) = s )
19	18	eqcomd 2628	. . . . . . . . 9 |- ( s e. CC -> s = ( ( s - 1 ) + 1 ) )
20	17, 19	syl 17	. . . . . . . 8 |- ( s e. NN -> s = ( ( s - 1 ) + 1 ) )
21	20	oveq2d 6666	. . . . . . 7 |- ( s e. NN -> ( 0 ... s ) = ( 0 ... ( ( s - 1 ) + 1 ) ) )
22	21	mpteq1d 4738	. . . . . 6 |- ( s e. NN -> ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) )
23	22	oveq2d 6666	. . . . 5 |- ( s e. NN -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
24	23	ad2antrl 764	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
25		eqid 2622	. . . . 5 |- ( Base ` Y ) = ( Base ` Y )
26		cpmadugsum.g	. . . . 5 |- .+ = ( +g ` Y )
27		crngring 18558	. . . . . . . . . 10 |- ( R e. CRing -> R e. Ring )
28	27	anim2i 593	. . . . . . . . 9 |- ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
29	28	3adant3 1081	. . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
30	4, 5	pmatring 20498	. . . . . . . 8 |- ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
31	29, 30	syl 17	. . . . . . 7 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
32		ringcmn 18581	. . . . . . 7 |- ( Y e. Ring -> Y e. CMnd )
33	31, 32	syl 17	. . . . . 6 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. CMnd )
34	33	adantr 481	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. CMnd )
35		nnm1nn0 11334	. . . . . 6 |- ( s e. NN -> ( s - 1 ) e. NN0 )
36	35	ad2antrl 764	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s - 1 ) e. NN0 )
37		simpll1 1100	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> N e. Fin )
38	27	3ad2ant2 1083	. . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
39	38	adantr 481	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
40	39	adantr 481	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> R e. Ring )
41		elmapi 7879	. . . . . . . . . 10 |- ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
42	21	feq2d 6031	. . . . . . . . . 10 |- ( s e. NN -> ( b : ( 0 ... s ) --> B <-> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B ) )
43	41, 42	syl5ibcom 235	. . . . . . . . 9 |- ( b e. ( B ^m ( 0 ... s ) ) -> ( s e. NN -> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B ) )
44	43	impcom 446	. . . . . . . 8 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B )
45	44	adantl 482	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B )
46	45	ffvelrnda 6359	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> ( b ` i ) e. B )
47		elfznn0 12433	. . . . . . . 8 |- ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) -> i e. NN0 )
48	47	adantl 482	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> i e. NN0 )
49		1nn0 11308	. . . . . . . 8 |- 1 e. NN0
50	49	a1i 11	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> 1 e. NN0 )
51	48, 50	nn0addcld 11355	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> ( i + 1 ) e. NN0 )
52	2, 3, 6, 4, 5, 25, 9, 8, 7	mat2pmatscmxcl 20545	. . . . . 6 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` i ) e. B /\ ( i + 1 ) e. NN0 ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
53	37, 40, 46, 51, 52	syl22anc 1327	. . . . 5 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
54	25, 26, 34, 36, 53	gsummptfzsplit 18332	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( Y gsumg ( i e. { ( ( s - 1 ) + 1 ) } |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
55		ringmnd 18556	. . . . . . . 8 |- ( Y e. Ring -> Y e. Mnd )
56	31, 55	syl 17	. . . . . . 7 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Mnd )
57	56	adantr 481	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Mnd )
58		ovexd 6680	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s - 1 ) + 1 ) e. _V )
59		simpl1 1064	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
60		nn0fz0 12437	. . . . . . . . . . 11 |- ( s e. NN0 <-> s e. ( 0 ... s ) )
61	1, 60	sylib 208	. . . . . . . . . 10 |- ( s e. NN -> s e. ( 0 ... s ) )
62		ffvelrn 6357	. . . . . . . . . 10 |- ( ( b : ( 0 ... s ) --> B /\ s e. ( 0 ... s ) ) -> ( b ` s ) e. B )
63	41, 61, 62	syl2anr 495	. . . . . . . . 9 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` s ) e. B )
64	1	adantr 481	. . . . . . . . . 10 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
65	49	a1i 11	. . . . . . . . . 10 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> 1 e. NN0 )
66	64, 65	nn0addcld 11355	. . . . . . . . 9 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( s + 1 ) e. NN0 )
67	63, 66	jca 554	. . . . . . . 8 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( b ` s ) e. B /\ ( s + 1 ) e. NN0 ) )
68	67	adantl 482	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( b ` s ) e. B /\ ( s + 1 ) e. NN0 ) )
69	2, 3, 6, 4, 5, 25, 9, 8, 7	mat2pmatscmxcl 20545	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` s ) e. B /\ ( s + 1 ) e. NN0 ) ) -> ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
70	59, 39, 68, 69	syl21anc 1325	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
71		oveq1 6657	. . . . . . . . 9 |- ( i = ( ( s - 1 ) + 1 ) -> ( i + 1 ) = ( ( ( s - 1 ) + 1 ) + 1 ) )
72	71	oveq1d 6665	. . . . . . . 8 |- ( i = ( ( s - 1 ) + 1 ) -> ( ( i + 1 ) .^ X ) = ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) )
73		fveq2 6191	. . . . . . . . 9 |- ( i = ( ( s - 1 ) + 1 ) -> ( b ` i ) = ( b ` ( ( s - 1 ) + 1 ) ) )
74	73	fveq2d 6195	. . . . . . . 8 |- ( i = ( ( s - 1 ) + 1 ) -> ( T ` ( b ` i ) ) = ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) )
75	72, 74	oveq12d 6668	. . . . . . 7 |- ( i = ( ( s - 1 ) + 1 ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) ) )
76	17, 18	syl 17	. . . . . . . . . . 11 |- ( s e. NN -> ( ( s - 1 ) + 1 ) = s )
77	76	oveq1d 6665	. . . . . . . . . 10 |- ( s e. NN -> ( ( ( s - 1 ) + 1 ) + 1 ) = ( s + 1 ) )
78	77	oveq1d 6665	. . . . . . . . 9 |- ( s e. NN -> ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) = ( ( s + 1 ) .^ X ) )
79	76	fveq2d 6195	. . . . . . . . . 10 |- ( s e. NN -> ( b ` ( ( s - 1 ) + 1 ) ) = ( b ` s ) )
80	79	fveq2d 6195	. . . . . . . . 9 |- ( s e. NN -> ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) = ( T ` ( b ` s ) ) )
81	78, 80	oveq12d 6668	. . . . . . . 8 |- ( s e. NN -> ( ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
82	81	ad2antrl 764	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
83	75, 82	sylan9eqr 2678	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i = ( ( s - 1 ) + 1 ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
84	25, 57, 58, 70, 83	gsumsnd 18352	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. { ( ( s - 1 ) + 1 ) } |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
85	84	oveq2d 6666	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( Y gsumg ( i e. { ( ( s - 1 ) + 1 ) } |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
86	24, 54, 85	3eqtrd 2660	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
87	1	ad2antrl 764	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
88	4, 5	pmatlmod 20499	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. Ring ) -> Y e. LMod )
89	28, 88	syl 17	. . . . . . . . 9 |- ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
90	89	3adant3 1081	. . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
91	90	adantr 481	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. LMod )
92	91	adantr 481	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. LMod )
93	4	ply1ring 19618	. . . . . . . . . . . . 13 |- ( R e. Ring -> P e. Ring )
94	27, 93	syl 17	. . . . . . . . . . . 12 |- ( R e. CRing -> P e. Ring )
95	94	3ad2ant2 1083	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
96		eqid 2622	. . . . . . . . . . . 12 |- (mulGrp ` P ) = (mulGrp ` P )
97	96	ringmgp 18553	. . . . . . . . . . 11 |- ( P e. Ring -> (mulGrp ` P ) e. Mnd )
98	95, 97	syl 17	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> (mulGrp ` P ) e. Mnd )
99	98	adantr 481	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> (mulGrp ` P ) e. Mnd )
100	99	adantr 481	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> (mulGrp ` P ) e. Mnd )
101		elfznn0 12433	. . . . . . . . 9 |- ( i e. ( 0 ... s ) -> i e. NN0 )
102	101	adantl 482	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> i e. NN0 )
103		eqid 2622	. . . . . . . . . . . . 13 |- ( Base ` P ) = ( Base ` P )
104	7, 4, 103	vr1cl 19587	. . . . . . . . . . . 12 |- ( R e. Ring -> X e. ( Base ` P ) )
105	27, 104	syl 17	. . . . . . . . . . 11 |- ( R e. CRing -> X e. ( Base ` P ) )
106	105	3ad2ant2 1083	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` P ) )
107	106	adantr 481	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> X e. ( Base ` P ) )
108	107	adantr 481	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> X e. ( Base ` P ) )
109	96, 103	mgpbas 18495	. . . . . . . . 9 |- ( Base ` P ) = ( Base ` (mulGrp ` P ) )
110	109, 8	mulgnn0cl 17558	. . . . . . . 8 |- ( ( (mulGrp ` P ) e. Mnd /\ i e. NN0 /\ X e. ( Base ` P ) ) -> ( i .^ X ) e. ( Base ` P ) )
111	100, 102, 108, 110	syl3anc 1326	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
112	4	ply1crng 19568	. . . . . . . . . . . . . . 15 |- ( R e. CRing -> P e. CRing )
113	112	anim2i 593	. . . . . . . . . . . . . 14 |- ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
114	113	3adant3 1081	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
115	5	matsca2 20226	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ P e. CRing ) -> P = (Scalar ` Y ) )
116	114, 115	syl 17	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = (Scalar ` Y ) )
117	116	eqcomd 2628	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> (Scalar ` Y ) = P )
118	117	fveq2d 6195	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` (Scalar ` Y ) ) = ( Base ` P ) )
119	118	eleq2d 2687	. . . . . . . . 9 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` (Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
120	119	adantr 481	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( i .^ X ) e. ( Base ` (Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
121	120	adantr 481	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) e. ( Base ` (Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
122	111, 121	mpbird 247	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` (Scalar ` Y ) ) )
123	31	adantr 481	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
124	123	adantr 481	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. Ring )
125		simpll1 1100	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> N e. Fin )
126	39	adantr 481	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> R e. Ring )
127		simpll3 1102	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> M e. B )
128	6, 2, 3, 4, 5	mat2pmatbas 20531	. . . . . . . 8 |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
129	125, 126, 127, 128	syl3anc 1326	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` M ) e. ( Base ` Y ) )
130	87	adantr 481	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> s e. NN0 )
131		simprr 796	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
132	131	anim1i 592	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) )
133	2, 3, 4, 5, 6	m2pmfzmap 20552	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
134	125, 126, 130, 132, 133	syl31anc 1329	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
135	25, 10	ringcl 18561	. . . . . . 7 |- ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
136	124, 129, 134, 135	syl3anc 1326	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
137		eqid 2622	. . . . . . 7 |- (Scalar ` Y ) = (Scalar ` Y )
138		eqid 2622	. . . . . . 7 |- ( Base ` (Scalar ` Y ) ) = ( Base ` (Scalar ` Y ) )
139	25, 137, 9, 138	lmodvscl 18880	. . . . . 6 |- ( ( Y e. LMod /\ ( i .^ X ) e. ( Base ` (Scalar ` Y ) ) /\ ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
140	92, 122, 136, 139	syl3anc 1326	. . . . 5 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
141	25, 26, 34, 87, 140	gsummptfzsplitl 18333	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( Y gsumg ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
142		0nn0 11307	. . . . . . . 8 |- 0 e. NN0
143	142	a1i 11	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. NN0 )
144		eqid 2622	. . . . . . . . . . . . 13 |- ( 0g ` (mulGrp ` P ) ) = ( 0g ` (mulGrp ` P ) )
145	109, 144, 8	mulg0 17546	. . . . . . . . . . . 12 |- ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 0g ` (mulGrp ` P ) ) )
146	106, 145	syl 17	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ X ) = ( 0g ` (mulGrp ` P ) ) )
147	146	adantr 481	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ X ) = ( 0g ` (mulGrp ` P ) ) )
148	147	oveq1d 6665	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 0g ` (mulGrp ` P ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
149		eqid 2622	. . . . . . . . . . . . 13 |- ( 1r ` P ) = ( 1r ` P )
150	96, 149	ringidval 18503	. . . . . . . . . . . 12 |- ( 1r ` P ) = ( 0g ` (mulGrp ` P ) )
151	150	a1i 11	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1r ` P ) = ( 0g ` (mulGrp ` P ) ) )
152	151	eqcomd 2628	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0g ` (mulGrp ` P ) ) = ( 1r ` P ) )
153	152	oveq1d 6665	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0g ` (mulGrp ` P ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
154	116	adantr 481	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> P = (Scalar ` Y ) )
155	154	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1r ` P ) = ( 1r ` (Scalar ` Y ) ) )
156	155	oveq1d 6665	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 1r ` (Scalar ` Y ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
157	27, 128	syl3an2 1360	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
158	157	adantr 481	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
159		simpl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> b : ( 0 ... s ) --> B )
160		elnn0uz 11725	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. NN0 <-> s e. ( ZZ>= ` 0 ) )
161	1, 160	sylib 208	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. NN -> s e. ( ZZ>= ` 0 ) )
162		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... s ) )
163	161, 162	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( s e. NN -> 0 e. ( 0 ... s ) )
164	163	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> 0 e. ( 0 ... s ) )
165	159, 164	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 |- ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> ( b ` 0 ) e. B )
166	165	ex 450	. . . . . . . . . . . . . . . 16 |- ( b : ( 0 ... s ) --> B -> ( s e. NN -> ( b ` 0 ) e. B ) )
167	41, 166	syl 17	. . . . . . . . . . . . . . 15 |- ( b e. ( B ^m ( 0 ... s ) ) -> ( s e. NN -> ( b ` 0 ) e. B ) )
168	167	impcom 446	. . . . . . . . . . . . . 14 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` 0 ) e. B )
169	168	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` 0 ) e. B )
170	6, 2, 3, 4, 5	mat2pmatbas 20531	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
171	59, 39, 169, 170	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
172	25, 10	ringcl 18561	. . . . . . . . . . . 12 |- ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` 0 ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
173	123, 158, 171, 172	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
174		eqid 2622	. . . . . . . . . . . 12 |- ( 1r ` (Scalar ` Y ) ) = ( 1r ` (Scalar ` Y ) )
175	25, 137, 9, 174	lmodvs1 18891	. . . . . . . . . . 11 |- ( ( Y e. LMod /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) ) -> ( ( 1r ` (Scalar ` Y ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
176	91, 173, 175	syl2anc 693	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` (Scalar ` Y ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
177	156, 176	eqtrd 2656	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
178	148, 153, 177	3eqtrd 2660	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
179	178, 173	eqeltrd 2701	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. ( Base ` Y ) )
180		oveq1 6657	. . . . . . . . 9 |- ( i = 0 -> ( i .^ X ) = ( 0 .^ X ) )
181		fveq2 6191	. . . . . . . . . . 11 |- ( i = 0 -> ( b ` i ) = ( b ` 0 ) )
182	181	fveq2d 6195	. . . . . . . . . 10 |- ( i = 0 -> ( T ` ( b ` i ) ) = ( T ` ( b ` 0 ) ) )
183	182	oveq2d 6666	. . . . . . . . 9 |- ( i = 0 -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
184	180, 183	oveq12d 6668	. . . . . . . 8 |- ( i = 0 -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
185	184	adantl 482	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i = 0 ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
186	25, 57, 143, 179, 185	gsumsnd 18352	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
187	109, 150, 8	mulg0 17546	. . . . . . . . 9 |- ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
188	106, 187	syl 17	. . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ X ) = ( 1r ` P ) )
189	188	adantr 481	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ X ) = ( 1r ` P ) )
190	189	oveq1d 6665	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
191	186, 190, 177	3eqtrd 2660	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
192	191	oveq2d 6666	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( Y gsumg ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
193	141, 192	eqtrd 2656	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
194	86, 193	oveq12d 6668	. 2 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
195		fzfid 12772	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... ( s - 1 ) ) e. Fin )
196		simpll1 1100	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> N e. Fin )
197	39	adantr 481	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> R e. Ring )
198	41	adantl 482	. . . . . . . . . . 11 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
199	198	adantr 481	. . . . . . . . . 10 |- ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> b : ( 0 ... s ) --> B )
200		nnz 11399	. . . . . . . . . . . . . . . 16 |- ( s e. NN -> s e. ZZ )
201		fzoval 12471	. . . . . . . . . . . . . . . 16 |- ( s e. ZZ -> ( 0..^ s ) = ( 0 ... ( s - 1 ) ) )
202	200, 201	syl 17	. . . . . . . . . . . . . . 15 |- ( s e. NN -> ( 0..^ s ) = ( 0 ... ( s - 1 ) ) )
203	202	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( s e. NN -> ( 0 ... ( s - 1 ) ) = ( 0..^ s ) )
204	203	eleq2d 2687	. . . . . . . . . . . . 13 |- ( s e. NN -> ( i e. ( 0 ... ( s - 1 ) ) <-> i e. ( 0..^ s ) ) )
205		elfzofz 12485	. . . . . . . . . . . . 13 |- ( i e. ( 0..^ s ) -> i e. ( 0 ... s ) )
206	204, 205	syl6bi 243	. . . . . . . . . . . 12 |- ( s e. NN -> ( i e. ( 0 ... ( s - 1 ) ) -> i e. ( 0 ... s ) ) )
207	206	adantr 481	. . . . . . . . . . 11 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( i e. ( 0 ... ( s - 1 ) ) -> i e. ( 0 ... s ) ) )
208	207	imp 445	. . . . . . . . . 10 |- ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> i e. ( 0 ... s ) )
209	199, 208	ffvelrnd 6360	. . . . . . . . 9 |- ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( b ` i ) e. B )
210	209	adantll 750	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( b ` i ) e. B )
211		elfznn0 12433	. . . . . . . . . 10 |- ( i e. ( 0 ... ( s - 1 ) ) -> i e. NN0 )
212	211	adantl 482	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> i e. NN0 )
213	49	a1i 11	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> 1 e. NN0 )
214	212, 213	nn0addcld 11355	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( i + 1 ) e. NN0 )
215	196, 197, 210, 214, 52	syl22anc 1327	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
216	215	ralrimiva 2966	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 0 ... ( s - 1 ) ) ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
217	25, 34, 195, 216	gsummptcl 18366	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
218	25, 26	cmncom 18209	. . . . 5 |- ( ( Y e. CMnd /\ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
219	34, 217, 70, 218	syl3anc 1326	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
220	219	oveq1d 6665	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
221		ringgrp 18552	. . . . . . . . 9 |- ( Y e. Ring -> Y e. Grp )
222	31, 221	syl 17	. . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
223	222	adantr 481	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
224		fzfid 12772	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 ... s ) e. Fin )
225	91	adantr 481	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. LMod )
226	99	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> (mulGrp ` P ) e. Mnd )
227		elfznn 12370	. . . . . . . . . . . . . 14 |- ( i e. ( 1 ... s ) -> i e. NN )
228	227	nnnn0d 11351	. . . . . . . . . . . . 13 |- ( i e. ( 1 ... s ) -> i e. NN0 )
229	228	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> i e. NN0 )
230	107	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> X e. ( Base ` P ) )
231	226, 229, 230, 110	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
232	116	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` P ) = ( Base ` (Scalar ` Y ) ) )
233	232	adantr 481	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Base ` P ) = ( Base ` (Scalar ` Y ) ) )
234	233	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( Base ` P ) = ( Base ` (Scalar ` Y ) ) )
235	231, 234	eleqtrd 2703	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i .^ X ) e. ( Base ` (Scalar ` Y ) ) )
236	123	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. Ring )
237	158	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` M ) e. ( Base ` Y ) )
238		simpll1 1100	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> N e. Fin )
239	39	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> R e. Ring )
240	198	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
241	240	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> b : ( 0 ... s ) --> B )
242		1eluzge0 11732	. . . . . . . . . . . . . . . . 17 |- 1 e. ( ZZ>= ` 0 )
243		fzss1 12380	. . . . . . . . . . . . . . . . 17 |- ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... s ) C_ ( 0 ... s ) )
244	242, 243	mp1i 13	. . . . . . . . . . . . . . . 16 |- ( s e. NN -> ( 1 ... s ) C_ ( 0 ... s ) )
245	244	sseld 3602	. . . . . . . . . . . . . . 15 |- ( s e. NN -> ( i e. ( 1 ... s ) -> i e. ( 0 ... s ) ) )
246	245	ad2antrl 764	. . . . . . . . . . . . . 14 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) -> i e. ( 0 ... s ) ) )
247	246	imp 445	. . . . . . . . . . . . 13 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> i e. ( 0 ... s ) )
248	241, 247	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( b ` i ) e. B )
249	6, 2, 3, 4, 5	mat2pmatbas 20531	. . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. Ring /\ ( b ` i ) e. B ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
250	238, 239, 248, 249	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
251	236, 237, 250, 135	syl3anc 1326	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
252	225, 235, 251, 139	syl3anc 1326	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
253	252	ralrimiva 2966	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 1 ... s ) ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
254	25, 34, 224, 253	gsummptcl 18366	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) )
255		cpmadugsum.s	. . . . . . . 8 |- .- = ( -g ` Y )
256	25, 26, 255	grpaddsubass 17505	. . . . . . 7 |- ( ( Y e. Grp /\ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) /\ ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) )
257	223, 70, 217, 254, 256	syl13anc 1328	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) )
258		oveq1 6657	. . . . . . . . . . . . . . . 16 |- ( x = i -> ( x - 1 ) = ( i - 1 ) )
259	258	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( x = i -> ( ( x - 1 ) + 1 ) = ( ( i - 1 ) + 1 ) )
260	259	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( x = i -> ( ( ( x - 1 ) + 1 ) .^ X ) = ( ( ( i - 1 ) + 1 ) .^ X ) )
261	258	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( x = i -> ( b ` ( x - 1 ) ) = ( b ` ( i - 1 ) ) )
262	261	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( x = i -> ( T ` ( b ` ( x - 1 ) ) ) = ( T ` ( b ` ( i - 1 ) ) ) )
263	260, 262	oveq12d 6668	. . . . . . . . . . . . 13 |- ( x = i -> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) = ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
264	263	cbvmptv 4750	. . . . . . . . . . . 12 |- ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
265	227	nncnd 11036	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 1 ... s ) -> i e. CC )
266	265	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. CC )
267		npcan1 10455	. . . . . . . . . . . . . . . 16 |- ( i e. CC -> ( ( i - 1 ) + 1 ) = i )
268	266, 267	syl 17	. . . . . . . . . . . . . . 15 |- ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( i - 1 ) + 1 ) = i )
269	268	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( ( i - 1 ) + 1 ) .^ X ) = ( i .^ X ) )
270	269	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) = ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
271	270	mpteq2dva 4744	. . . . . . . . . . . 12 |- ( s e. NN -> ( i e. ( 1 ... s ) |-> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) )
272	264, 271	syl5eq 2668	. . . . . . . . . . 11 |- ( s e. NN -> ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) )
273	272	oveq2d 6666	. . . . . . . . . 10 |- ( s e. NN -> ( Y gsumg ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) = ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) )
274	273	ad2antrl 764	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) = ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) )
275	274	oveq1d 6665	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
276		eqid 2622	. . . . . . . . . . 11 |- ( 0g ` Y ) = ( 0g ` Y )
277		1zzd 11408	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. ZZ )
278		0zd 11389	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. ZZ )
279	36	nn0zd 11480	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s - 1 ) e. ZZ )
280		oveq1 6657	. . . . . . . . . . . . 13 |- ( i = ( x - 1 ) -> ( i + 1 ) = ( ( x - 1 ) + 1 ) )
281	280	oveq1d 6665	. . . . . . . . . . . 12 |- ( i = ( x - 1 ) -> ( ( i + 1 ) .^ X ) = ( ( ( x - 1 ) + 1 ) .^ X ) )
282		fveq2 6191	. . . . . . . . . . . . 13 |- ( i = ( x - 1 ) -> ( b ` i ) = ( b ` ( x - 1 ) ) )
283	282	fveq2d 6195	. . . . . . . . . . . 12 |- ( i = ( x - 1 ) -> ( T ` ( b ` i ) ) = ( T ` ( b ` ( x - 1 ) ) ) )
284	281, 283	oveq12d 6668	. . . . . . . . . . 11 |- ( i = ( x - 1 ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) )
285	25, 276, 34, 277, 278, 279, 215, 284	gsummptshft 18336	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsumg ( x e. ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) )
286		0p1e1 11132	. . . . . . . . . . . . . 14 |- ( 0 + 1 ) = 1
287	286	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 + 1 ) = 1 )
288	76	ad2antrl 764	. . . . . . . . . . . . 13 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s - 1 ) + 1 ) = s )
289	287, 288	oveq12d 6668	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) = ( 1 ... s ) )
290	289	mpteq1d 4738	. . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( x e. ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) = ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) )
291	290	oveq2d 6666	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( x e. ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) = ( Y gsumg ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) )
292	285, 291	eqtrd 2656	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsumg ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) )
293	292	oveq1d 6665	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
294		ringabl 18580	. . . . . . . . . . 11 |- ( Y e. Ring -> Y e. Abel )
295	31, 294	syl 17	. . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Abel )
296	295	adantr 481	. . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Abel )
297	227	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. NN )
298		nnz 11399	. . . . . . . . . . . . . . . . . 18 |- ( i e. NN -> i e. ZZ )
299		elfzm1b 12418	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ZZ /\ s e. ZZ ) -> ( i e. ( 1 ... s ) <-> ( i - 1 ) e. ( 0 ... ( s - 1 ) ) ) )
300	298, 200, 299	syl2an 494	. . . . . . . . . . . . . . . . 17 |- ( ( i e. NN /\ s e. NN ) -> ( i e. ( 1 ... s ) <-> ( i - 1 ) e. ( 0 ... ( s - 1 ) ) ) )
301	202	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. NN /\ s e. NN ) -> ( 0..^ s ) = ( 0 ... ( s - 1 ) ) )
302	301	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. NN /\ s e. NN ) -> ( 0 ... ( s - 1 ) ) = ( 0..^ s ) )
303	302	eleq2d 2687	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. NN /\ s e. NN ) -> ( ( i - 1 ) e. ( 0 ... ( s - 1 ) ) <-> ( i - 1 ) e. ( 0..^ s ) ) )
304		elfzofz 12485	. . . . . . . . . . . . . . . . . 18 |- ( ( i - 1 ) e. ( 0..^ s ) -> ( i - 1 ) e. ( 0 ... s ) )
305	303, 304	syl6bi 243	. . . . . . . . . . . . . . . . 17 |- ( ( i e. NN /\ s e. NN ) -> ( ( i - 1 ) e. ( 0 ... ( s - 1 ) ) -> ( i - 1 ) e. ( 0 ... s ) ) )
306	300, 305	sylbid 230	. . . . . . . . . . . . . . . 16 |- ( ( i e. NN /\ s e. NN ) -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
307	306	expimpd 629	. . . . . . . . . . . . . . 15 |- ( i e. NN -> ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) ) )
308	297, 307	mpcom 38	. . . . . . . . . . . . . 14 |- ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
309	308	ex 450	. . . . . . . . . . . . 13 |- ( s e. NN -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
310	309	ad2antrl 764	. . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
311	310	imp 445	. . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
312	241, 311	ffvelrnd 6360	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( b ` ( i - 1 ) ) e. B )
313	2, 3, 6, 4, 5, 25, 9, 8, 7	mat2pmatscmxcl 20545	. . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` ( i - 1 ) ) e. B /\ i e. NN0 ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) e. ( Base ` Y ) )
314	238, 239, 312, 229, 313	syl22anc 1327	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) e. ( Base ` Y ) )
315		eqid 2622	. . . . . . . . 9 |- ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
316		eqid 2622	. . . . . . . . 9 |- ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
317	25, 255, 296, 224, 314, 252, 315, 316	gsummptfidmsub 18350	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
318	275, 293, 317	3eqtr4d 2666	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
319	318	oveq2d 6666	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) )
320	223	adantr 481	. . . . . . . . . 10 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. Grp )
321	25, 255	grpsubcl 17495	. . . . . . . . . 10 |- ( ( Y e. Grp /\ ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) e. ( Base ` Y ) /\ ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) ) -> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
322	320, 314, 252, 321	syl3anc 1326	. . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
323	322	ralrimiva 2966	. . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 1 ... s ) ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
324	25, 34, 224, 323	gsummptcl 18366	. . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) e. ( Base ` Y ) )
325	25, 26	cmncom 18209	. . . . . . 7 |- ( ( Y e. CMnd /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) e. ( Base ` Y ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
326	34, 70, 324, 325	syl3anc 1326	. . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
327	257, 319, 326	3eqtrd 2660	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
328	327	oveq1d 6665	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
329	25, 26	mndcl 17301	. . . . . 6 |- ( ( Y e. Mnd /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) )
330	57, 70, 217, 329	syl3anc 1326	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) )
331	25, 26, 255, 296, 330, 254, 173	ablsubsub4 18224	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
332	25, 26, 255	grpaddsubass 17505	. . . . 5 |- ( ( Y e. Grp /\ ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) ) ) -> ( ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
333	223, 324, 70, 173, 332	syl13anc 1328	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
334	328, 331, 333	3eqtr3d 2664	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
335	6, 2, 3, 4, 5	mat2pmatbas 20531	. . . . . . . . 9 |- ( ( N e. Fin /\ R e. Ring /\ ( b ` ( i - 1 ) ) e. B ) -> ( T ` ( b ` ( i - 1 ) ) ) e. ( Base ` Y ) )
336	238, 239, 312, 335	syl3anc 1326	. . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` ( b ` ( i - 1 ) ) ) e. ( Base ` Y ) )
337	25, 9, 137, 138, 255, 225, 235, 336, 251	lmodsubdi 18920	. . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
338	337	eqcomd 2628	. . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
339	338	mpteq2dva 4744	. . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
340	339	oveq2d 6666	. . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
341	340	oveq1d 6665	. . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
342	220, 334, 341	3eqtrd 2660	. 2 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsumg ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
343	16, 194, 342	3eqtrd 2660	1 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   _Vcvv 3200   C_ wss 3574   {csn 4177   |-> cmpt 4729   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   - cmin 10266   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326  ..^cfzo 12465   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   gsum_g cgsu 16101   Mndcmnd 17294   Grpcgrp 17422   -gcsg 17424  ._gcmg 17540  CMndccmn 18193   Abelcabl 18194  mulGrpcmgp 18489   1rcur 18501   Ringcrg 18547   CRingccrg 18548   LModclmod 18863  var₁cv1 19546  Poly₁cpl1 19547   Mat cmat 20213   matToPolyMat cmat2pmat 20509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-ot 4186  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-subrg 18778  df-lmod 18865  df-lss 18933  df-sra 19172  df-rgmod 19173  df-assa 19312  df-ascl 19314  df-psr 19356  df-mvr 19357  df-mpl 19358  df-opsr 19360  df-psr1 19550  df-vr1 19551  df-ply1 19552  df-dsmm 20076  df-frlm 20091  df-mamu 20190  df-mat 20214  df-mat2pmat 20512

This theorem is referenced by:  cpmadugsumfi  20682