cpmadumatpolylem2

Description: Lemma 2 for cpmadumatpoly . (Contributed by AV, 20-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	cpmadumatpoly.a	\|- A = ( N Mat R )
	cpmadumatpoly.b	\|- B = ( Base ` A )
	cpmadumatpoly.p	\|- P = ( Poly1 ` R )
	cpmadumatpoly.y	\|- Y = ( N Mat P )
	cpmadumatpoly.t	\|- T = ( N matToPolyMat R )
	cpmadumatpoly.r	\|- .X. = ( .r ` Y )
	cpmadumatpoly.m0	\|- .- = ( -g ` Y )
	cpmadumatpoly.0	\|- .0. = ( 0g ` Y )
	cpmadumatpoly.g	\|- G = ( n e. NN0 \|-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
	cpmadumatpoly.s	\|- S = ( N ConstPolyMat R )
	cpmadumatpoly.m1	\|- .x. = ( .s ` Y )
	cpmadumatpoly.1	\|- .1. = ( 1r ` Y )
	cpmadumatpoly.z	\|- Z = ( var1 ` R )
	cpmadumatpoly.d	\|- D = ( ( Z .x. .1. ) .- ( T ` M ) )
	cpmadumatpoly.j	\|- J = ( N maAdju P )
	cpmadumatpoly.w	\|- W = ( Base ` Y )
	cpmadumatpoly.q	\|- Q = ( Poly1 ` A )
	cpmadumatpoly.x	\|- X = ( var1 ` A )
	cpmadumatpoly.m2	\|- .* = ( .s ` Q )
	cpmadumatpoly.e	\|- .^ = ( .g ` ( mulGrp ` Q ) )
	cpmadumatpoly.u	\|- U = ( N cPolyMatToMat R )
Assertion	cpmadumatpolylem2	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( U o. G ) finSupp ( 0g ` A ) )

Proof

Step	Hyp	Ref	Expression
1		cpmadumatpoly.a	\|- A = ( N Mat R )
2		cpmadumatpoly.b	\|- B = ( Base ` A )
3		cpmadumatpoly.p	\|- P = ( Poly1 ` R )
4		cpmadumatpoly.y	\|- Y = ( N Mat P )
5		cpmadumatpoly.t	\|- T = ( N matToPolyMat R )
6		cpmadumatpoly.r	\|- .X. = ( .r ` Y )
7		cpmadumatpoly.m0	\|- .- = ( -g ` Y )
8		cpmadumatpoly.0	\|- .0. = ( 0g ` Y )
9		cpmadumatpoly.g	\|- G = ( n e. NN0 \|-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
10		cpmadumatpoly.s	\|- S = ( N ConstPolyMat R )
11		cpmadumatpoly.m1	\|- .x. = ( .s ` Y )
12		cpmadumatpoly.1	\|- .1. = ( 1r ` Y )
13		cpmadumatpoly.z	\|- Z = ( var1 ` R )
14		cpmadumatpoly.d	\|- D = ( ( Z .x. .1. ) .- ( T ` M ) )
15		cpmadumatpoly.j	\|- J = ( N maAdju P )
16		cpmadumatpoly.w	\|- W = ( Base ` Y )
17		cpmadumatpoly.q	\|- Q = ( Poly1 ` A )
18		cpmadumatpoly.x	\|- X = ( var1 ` A )
19		cpmadumatpoly.m2	\|- .* = ( .s ` Q )
20		cpmadumatpoly.e	\|- .^ = ( .g ` ( mulGrp ` Q ) )
21		cpmadumatpoly.u	\|- U = ( N cPolyMatToMat R )
22		fvexd	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0g ` A ) e. _V )
23		crngring	\|- ( R e. CRing -> R e. Ring )
24	23	anim2i	\|- ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
25	24	3adant3	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
26	25	ad2antrr	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( N e. Fin /\ R e. Ring ) )
27	10 3 4	0elcpmat	\|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` Y ) e. S )
28	26 27	syl	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0g ` Y ) e. S )
29	1 2 3 4 6 7 8 5 9 10	chfacfisfcpmat	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> S )
30	23 29	syl3anl2	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> S )
31	30	anassrs	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> G : NN0 --> S )
32	1 2 10 21	cpm2mf	\|- ( ( N e. Fin /\ R e. Ring ) -> U : S --> B )
33	26 32	syl	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> U : S --> B )
34		ssidd	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> S C_ S )
35		nn0ex	\|- NN0 e. _V
36	35	a1i	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> NN0 e. _V )
37	10	ovexi	\|- S e. _V
38	37	a1i	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> S e. _V )
39	1 2 3 4 6 7 8 5 9	chfacffsupp	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G finSupp ( 0g ` Y ) )
40	39	anassrs	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> G finSupp ( 0g ` Y ) )
41		eqid	\|- ( 0g ` A ) = ( 0g ` A )
42		eqid	\|- ( 0g ` Y ) = ( 0g ` Y )
43	1 21 3 4 41 42	m2cpminv0	\|- ( ( N e. Fin /\ R e. Ring ) -> ( U ` ( 0g ` Y ) ) = ( 0g ` A ) )
44	23 43	sylan2	\|- ( ( N e. Fin /\ R e. CRing ) -> ( U ` ( 0g ` Y ) ) = ( 0g ` A ) )
45	44	3adant3	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( U ` ( 0g ` Y ) ) = ( 0g ` A ) )
46	45	ad2antrr	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( U ` ( 0g ` Y ) ) = ( 0g ` A ) )
47	22 28 31 33 34 36 38 40 46	fsuppcor	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( U o. G ) finSupp ( 0g ` A ) )

Metamath Proof Explorer

Theorem cpmadumatpolylem2

Proof