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