Metamath Proof Explorer


Theorem 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 ) )