Metamath Proof Explorer

Theorem decpmatmulsumfsupp

Description: Lemma 0 for pm2mpmhm . (Contributed by AV, 21-Oct-2019)

Ref Expression
Hypotheses decpmatmul.p 
|- P = ( Poly1 ` R )
decpmatmul.c 
|- C = ( N Mat P )
decpmatmul.b 
|- B = ( Base ` C )
decpmatmul.a 
|- A = ( N Mat R )
decpmatmulsumfsupp.m 
|- .x. = ( .r ` A )
decpmatmulsumfsupp.0 
|- .0. = ( 0g ` A )
Assertion decpmatmulsumfsupp 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( l e. NN0 |-> ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) ) ) ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 decpmatmul.p 
 |-  P = ( Poly1 ` R )
2 decpmatmul.c 
 |-  C = ( N Mat P )
3 decpmatmul.b 
 |-  B = ( Base ` C )
4 decpmatmul.a 
 |-  A = ( N Mat R )
5 decpmatmulsumfsupp.m 
 |-  .x. = ( .r ` A )
6 decpmatmulsumfsupp.0 
 |-  .0. = ( 0g ` A )
7 6 fvexi 
 |-  .0. e. _V
8 7 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> .0. e. _V )
9 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ l e. NN0 ) -> ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) ) ) e. _V )
10 oveq2 
 |-  ( l = n -> ( 0 ... l ) = ( 0 ... n ) )
11 oveq1 
 |-  ( l = n -> ( l - k ) = ( n - k ) )
12 11 oveq2d 
 |-  ( l = n -> ( y decompPMat ( l - k ) ) = ( y decompPMat ( n - k ) ) )
13 12 oveq2d 
 |-  ( l = n -> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) = ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) )
14 10 13 mpteq12dv 
 |-  ( l = n -> ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) ) = ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) )
15 14 oveq2d 
 |-  ( l = n -> ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) ) ) = ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) )
16 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> N e. Fin )
17 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> R e. Ring )
18 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
19 18 anim1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( C e. Ring /\ ( x e. B /\ y e. B ) ) )
20 3anass 
 |-  ( ( C e. Ring /\ x e. B /\ y e. B ) <-> ( C e. Ring /\ ( x e. B /\ y e. B ) ) )
21 19 20 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( C e. Ring /\ x e. B /\ y e. B ) )
22 eqid 
 |-  ( .r ` C ) = ( .r ` C )
23 3 22 ringcl 
 |-  ( ( C e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` C ) y ) e. B )
24 21 23 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` C ) y ) e. B )
25 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
26 1 2 3 25 pmatcoe1fsupp 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( .r ` C ) y ) e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) )
27 16 17 24 26 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) )
28 fvoveq1 
 |-  ( a = i -> ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) = ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) )
29 28 fveq1d 
 |-  ( a = i -> ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) )
30 29 eqeq1d 
 |-  ( a = i -> ( ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) )
31 oveq2 
 |-  ( b = j -> ( i ( x ( .r ` C ) y ) b ) = ( i ( x ( .r ` C ) y ) j ) )
32 31 fveq2d 
 |-  ( b = j -> ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) = ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) )
33 32 fveq1d 
 |-  ( b = j -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) = ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) )
34 33 eqeq1d 
 |-  ( b = j -> ( ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) = ( 0g ` R ) ) )
35 30 34 rspc2va 
 |-  ( ( ( i e. N /\ j e. N ) /\ A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) = ( 0g ` R ) )
36 35 expcom 
 |-  ( A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) -> ( ( i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) = ( 0g ` R ) ) )
37 36 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> ( ( i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) = ( 0g ` R ) ) )
38 37 3impib 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) = ( 0g ` R ) )
39 38 mpoeq3dva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
40 4 25 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
41 6 40 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. = ( i e. N , j e. N |-> ( 0g ` R ) ) )
42 41 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> .0. = ( i e. N , j e. N |-> ( 0g ` R ) ) )
43 39 42 eqtr4d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) /\ A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. )
44 43 ex 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) )
45 44 imim2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( s < n -> A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) ) )
46 45 ralimdva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A. n e. NN0 ( s < n -> A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> A. n e. NN0 ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) ) )
47 46 reximdv 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( E. s e. NN0 A. n e. NN0 ( s < n -> A. a e. N A. b e. N ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) ) )
48 27 47 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) )
49 5 oveqi 
 |-  ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) = ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) )
50 49 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) = ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) )
51 50 mpteq2dv 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) = ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) )
52 51 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) )
53 1 2 3 4 decpmatmul 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) /\ n e. NN0 ) -> ( ( x ( .r ` C ) y ) decompPMat n ) = ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) )
54 53 ad4ant234 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( x ( .r ` C ) y ) decompPMat n ) = ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) )
55 2 3 decpmatval 
 |-  ( ( ( x ( .r ` C ) y ) e. B /\ n e. NN0 ) -> ( ( x ( .r ` C ) y ) decompPMat n ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) )
56 24 55 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( x ( .r ` C ) y ) decompPMat n ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) )
57 52 54 56 3eqtr2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) )
58 57 eqeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = .0. <-> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) )
59 58 imbi2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( s < n -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = .0. ) <-> ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) ) )
60 59 ralbidva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A. n e. NN0 ( s < n -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = .0. ) <-> A. n e. NN0 ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) ) )
61 60 rexbidv 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( E. s e. NN0 A. n e. NN0 ( s < n -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = .0. ) <-> E. s e. NN0 A. n e. NN0 ( s < n -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) = .0. ) ) )
62 48 61 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( n - k ) ) ) ) ) = .0. ) )
63 8 9 15 62 mptnn0fsuppd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( l e. NN0 |-> ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) ) ) ) finSupp .0. )