Metamath Proof Explorer

Theorem pmatcollpw3fi1lem2

Description: Lemma 2 for pmatcollpw3fi1 . (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p 
|- P = ( Poly1 ` R )
pmatcollpw.c 
|- C = ( N Mat P )
pmatcollpw.b 
|- B = ( Base ` C )
pmatcollpw.m 
|- .* = ( .s ` C )
pmatcollpw.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw.x 
|- X = ( var1 ` R )
pmatcollpw.t 
|- T = ( N matToPolyMat R )
pmatcollpw3.a 
|- A = ( N Mat R )
pmatcollpw3.d 
|- D = ( Base ` A )
Assertion pmatcollpw3fi1lem2 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw.c 
 |-  C = ( N Mat P )
3 pmatcollpw.b 
 |-  B = ( Base ` C )
4 pmatcollpw.m 
 |-  .* = ( .s ` C )
5 pmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw.x 
 |-  X = ( var1 ` R )
7 pmatcollpw.t 
 |-  T = ( N matToPolyMat R )
8 pmatcollpw3.a 
 |-  A = ( N Mat R )
9 pmatcollpw3.d 
 |-  D = ( Base ` A )
10 fveq1 
 |-  ( f = g -> ( f ` n ) = ( g ` n ) )
11 10 fveq2d 
 |-  ( f = g -> ( T ` ( f ` n ) ) = ( T ` ( g ` n ) ) )
12 11 oveq2d 
 |-  ( f = g -> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) = ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) )
13 12 mpteq2dv 
 |-  ( f = g -> ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) = ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) )
14 13 oveq2d 
 |-  ( f = g -> ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) )
15 14 eqeq2d 
 |-  ( f = g -> ( M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) )
16 15 cbvrexvw 
 |-  ( E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> E. g e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) )
17 crngring 
 |-  ( R e. CRing -> R e. Ring )
18 17 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
19 18 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
20 19 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> ( N e. Fin /\ R e. Ring ) )
21 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> g e. ( D ^m { 0 } ) )
22 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) )
23 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
24 eqid 
 |-  ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) )
25 1 2 3 4 5 6 7 8 9 23 24 pmatcollpw3fi1lem1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ g e. ( D ^m { 0 } ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) )
26 20 21 22 25 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) )
27 1nn 
 |-  1 e. NN
28 27 a1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) /\ M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) ) -> 1 e. NN )
29 oveq2 
 |-  ( s = 1 -> ( 0 ... s ) = ( 0 ... 1 ) )
30 29 oveq2d 
 |-  ( s = 1 -> ( D ^m ( 0 ... s ) ) = ( D ^m ( 0 ... 1 ) ) )
31 29 mpteq1d 
 |-  ( s = 1 -> ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) = ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) )
32 31 oveq2d 
 |-  ( s = 1 -> ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
33 32 eqeq2d 
 |-  ( s = 1 -> ( M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
34 30 33 rexeqbidv 
 |-  ( s = 1 -> ( E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> E. f e. ( D ^m ( 0 ... 1 ) ) M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
35 34 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) /\ M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) ) /\ s = 1 ) -> ( E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> E. f e. ( D ^m ( 0 ... 1 ) ) M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
36 elmapi 
 |-  ( g e. ( D ^m { 0 } ) -> g : { 0 } --> D )
37 c0ex 
 |-  0 e. _V
38 37 snid 
 |-  0 e. { 0 }
39 38 a1i 
 |-  ( l e. ( 0 ... 1 ) -> 0 e. { 0 } )
40 ffvelcdm 
 |-  ( ( g : { 0 } --> D /\ 0 e. { 0 } ) -> ( g ` 0 ) e. D )
41 39 40 sylan2 
 |-  ( ( g : { 0 } --> D /\ l e. ( 0 ... 1 ) ) -> ( g ` 0 ) e. D )
42 41 ex 
 |-  ( g : { 0 } --> D -> ( l e. ( 0 ... 1 ) -> ( g ` 0 ) e. D ) )
43 36 42 syl 
 |-  ( g e. ( D ^m { 0 } ) -> ( l e. ( 0 ... 1 ) -> ( g ` 0 ) e. D ) )
44 43 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) -> ( l e. ( 0 ... 1 ) -> ( g ` 0 ) e. D ) )
45 44 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ l e. ( 0 ... 1 ) ) -> ( g ` 0 ) e. D )
46 8 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
47 17 46 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
48 47 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> A e. Ring )
49 9 23 ring0cl 
 |-  ( A e. Ring -> ( 0g ` A ) e. D )
50 48 49 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0g ` A ) e. D )
51 50 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ l e. ( 0 ... 1 ) ) -> ( 0g ` A ) e. D )
52 45 51 ifcld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ l e. ( 0 ... 1 ) ) -> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) e. D )
53 52 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) -> ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) : ( 0 ... 1 ) --> D )
54 9 fvexi 
 |-  D e. _V
55 ovex 
 |-  ( 0 ... 1 ) e. _V
56 54 55 pm3.2i 
 |-  ( D e. _V /\ ( 0 ... 1 ) e. _V )
57 elmapg 
 |-  ( ( D e. _V /\ ( 0 ... 1 ) e. _V ) -> ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) e. ( D ^m ( 0 ... 1 ) ) <-> ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) : ( 0 ... 1 ) --> D ) )
58 56 57 mp1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) -> ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) e. ( D ^m ( 0 ... 1 ) ) <-> ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) : ( 0 ... 1 ) --> D ) )
59 53 58 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) -> ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) e. ( D ^m ( 0 ... 1 ) ) )
60 59 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) e. ( D ^m ( 0 ... 1 ) ) )
61 fveq1 
 |-  ( f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) -> ( f ` n ) = ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) )
62 61 fveq2d 
 |-  ( f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) -> ( T ` ( f ` n ) ) = ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) )
63 62 oveq2d 
 |-  ( f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) -> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) = ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) )
64 63 mpteq2dv 
 |-  ( f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) -> ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) = ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) )
65 64 oveq2d 
 |-  ( f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) -> ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) )
66 65 eqeq2d 
 |-  ( f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) -> ( M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) ) )
67 66 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) /\ f = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ) -> ( M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) ) )
68 60 67 rspcedv 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> ( M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) -> E. f e. ( D ^m ( 0 ... 1 ) ) M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
69 68 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) /\ M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) ) -> E. f e. ( D ^m ( 0 ... 1 ) ) M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
70 28 35 69 rspcedvd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) /\ M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( g ` 0 ) , ( 0g ` A ) ) ) ` n ) ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
71 26 70 mpdan 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ g e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
72 71 rexlimdva2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. g e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( g ` n ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
73 16 72 biimtrid 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )