cpmadumatpolylem1

Description: Lemma 1 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	cpmadumatpolylem1	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( U o. G ) e. ( B ^m NN0 ) )

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		simp1	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> N e. Fin )
23		crngring	\|- ( R e. CRing -> R e. Ring )
24	23	3ad2ant2	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
25	22 24	jca	\|- ( ( 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	1 2 10 21	cpm2mf	\|- ( ( N e. Fin /\ R e. Ring ) -> U : S --> B )
28	26 27	syl	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> U : S --> B )
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		fco	\|- ( ( U : S --> B /\ G : NN0 --> S ) -> ( U o. G ) : NN0 --> B )
33	28 31 32	syl2anc	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( U o. G ) : NN0 --> B )
34	2	fvexi	\|- B e. _V
35		nn0ex	\|- NN0 e. _V
36	34 35	pm3.2i	\|- ( B e. _V /\ NN0 e. _V )
37		elmapg	\|- ( ( B e. _V /\ NN0 e. _V ) -> ( ( U o. G ) e. ( B ^m NN0 ) <-> ( U o. G ) : NN0 --> B ) )
38	36 37	mp1i	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( U o. G ) e. ( B ^m NN0 ) <-> ( U o. G ) : NN0 --> B ) )
39	33 38	mpbird	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( U o. G ) e. ( B ^m NN0 ) )

Metamath Proof Explorer

Theorem cpmadumatpolylem1

Proof