Theorem pmatcollpw1lem1

Description: Lemma 1 for pmatcollpw1 . (Contributed by AV, 28-Sep-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw1.p	|- P = ( Poly1 ` R )
	pmatcollpw1.c	|- C = ( N Mat P )
	pmatcollpw1.b	|- B = ( Base ` C )
	pmatcollpw1.m	|- .X. = ( .s ` P )
	pmatcollpw1.e	|- .^ = ( .g ` ( mulGrp ` P ) )
	pmatcollpw1.x	|- X = ( var1 ` R )
Assertion	pmatcollpw1lem1	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( n e. NN0 |-> ( ( I ( M decompPMat n ) J ) .X. ( n .^ X ) ) ) finSupp ( 0g ` P ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw1.p	|- P = ( Poly1 ` R )
2		pmatcollpw1.c	|- C = ( N Mat P )
3		pmatcollpw1.b	|- B = ( Base ` C )
4		pmatcollpw1.m	|- .X. = ( .s ` P )
5		pmatcollpw1.e	|- .^ = ( .g ` ( mulGrp ` P ) )
6		pmatcollpw1.x	|- X = ( var1 ` R )
7		fvexd	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( 0g ` P ) e. _V )
8		ovexd	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ n e. NN0 ) -> ( ( I ( M decompPMat n ) J ) .X. ( n .^ X ) ) e. _V )
9		oveq2	|- ( n = x -> ( M decompPMat n ) = ( M decompPMat x ) )
10	9	oveqd	|- ( n = x -> ( I ( M decompPMat n ) J ) = ( I ( M decompPMat x ) J ) )
11		oveq1	|- ( n = x -> ( n .^ X ) = ( x .^ X ) )
12	10 11	oveq12d	|- ( n = x -> ( ( I ( M decompPMat n ) J ) .X. ( n .^ X ) ) = ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) )
13		eqid	|- ( Base ` P ) = ( Base ` P )
14		simp2	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> I e. N )
15		simp3	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> J e. N )
16		simp13	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> M e. B )
17	2 13 3 14 15 16	matecld	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( I M J ) e. ( Base ` P ) )
18		eqid	|- ( coe1 ` ( I M J ) ) = ( coe1 ` ( I M J ) )
19		eqid	|- ( 0g ` R ) = ( 0g ` R )
20	18 13 1 19	coe1ae0	|- ( ( I M J ) e. ( Base ` P ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) )
21	17 20	syl	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) )
22		simpl12	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> R e. Ring )
23	16	adantr	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> M e. B )
24		simpr	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> x e. NN0 )
25		3simpc	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( I e. N /\ J e. N ) )
26	25	adantr	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> ( I e. N /\ J e. N ) )
27	1 2 3	decpmate	|- ( ( ( R e. Ring /\ M e. B /\ x e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( I ( M decompPMat x ) J ) = ( ( coe1 ` ( I M J ) ) ` x ) )
28	22 23 24 26 27	syl31anc	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> ( I ( M decompPMat x ) J ) = ( ( coe1 ` ( I M J ) ) ` x ) )
29	28	adantr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) /\ ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( I ( M decompPMat x ) J ) = ( ( coe1 ` ( I M J ) ) ` x ) )
30		simpr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) /\ ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) )
31	29 30	eqtrd	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) /\ ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( I ( M decompPMat x ) J ) = ( 0g ` R ) )
32	31	oveq1d	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) /\ ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( ( 0g ` R ) .X. ( x .^ X ) ) )
33		eqid	|- ( mulGrp ` P ) = ( mulGrp ` P )
34	1 6 33 5 13	ply1moncl	|- ( ( R e. Ring /\ x e. NN0 ) -> ( x .^ X ) e. ( Base ` P ) )
35	22 24 34	syl2anc	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> ( x .^ X ) e. ( Base ` P ) )
36	1 13 4 19	ply10s0	|- ( ( R e. Ring /\ ( x .^ X ) e. ( Base ` P ) ) -> ( ( 0g ` R ) .X. ( x .^ X ) ) = ( 0g ` P ) )
37	22 35 36	syl2anc	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> ( ( 0g ` R ) .X. ( x .^ X ) ) = ( 0g ` P ) )
38	37	adantr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) /\ ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( ( 0g ` R ) .X. ( x .^ X ) ) = ( 0g ` P ) )
39	32 38	eqtrd	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) /\ ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( 0g ` P ) )
40	39	ex	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> ( ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
41	40	imim2d	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) /\ x e. NN0 ) -> ( ( s < x -> ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> ( s < x -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
42	41	ralimdva	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( A. x e. NN0 ( s < x -> ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> A. x e. NN0 ( s < x -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
43	42	reximdv	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` ( I M J ) ) ` x ) = ( 0g ` R ) ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
44	21 43	mpd	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( I ( M decompPMat x ) J ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
45	7 8 12 44	mptnn0fsuppd	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( n e. NN0 |-> ( ( I ( M decompPMat n ) J ) .X. ( n .^ X ) ) ) finSupp ( 0g ` P ) )