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 eqtrid
 |-  ( ( 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. )