Metamath Proof Explorer

Theorem pm2mpmhmlem1

Description: Lemma 1 for pm2mpmhm . (Contributed by AV, 21-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p 
|- P = ( Poly1 ` R )
pm2mpfo.c 
|- C = ( N Mat P )
pm2mpfo.b 
|- B = ( Base ` C )
pm2mpfo.m 
|- .* = ( .s ` Q )
pm2mpfo.e 
|- .^ = ( .g ` ( mulGrp ` Q ) )
pm2mpfo.x 
|- X = ( var1 ` A )
pm2mpfo.a 
|- A = ( N Mat R )
pm2mpfo.q 
|- Q = ( Poly1 ` A )
pm2mpfo.l 
|- L = ( Base ` Q )
pm2mpfo.t 
|- T = ( N pMatToMatPoly R )
Assertion pm2mpmhmlem1 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( l e. NN0 |-> ( ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) ) ) .* ( l .^ X ) ) ) finSupp ( 0g ` Q ) )

Proof

Step Hyp Ref Expression
1 pm2mpfo.p 
 |-  P = ( Poly1 ` R )
2 pm2mpfo.c 
 |-  C = ( N Mat P )
3 pm2mpfo.b 
 |-  B = ( Base ` C )
4 pm2mpfo.m 
 |-  .* = ( .s ` Q )
5 pm2mpfo.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 pm2mpfo.x 
 |-  X = ( var1 ` A )
7 pm2mpfo.a 
 |-  A = ( N Mat R )
8 pm2mpfo.q 
 |-  Q = ( Poly1 ` A )
9 pm2mpfo.l 
 |-  L = ( Base ` Q )
10 pm2mpfo.t 
 |-  T = ( N pMatToMatPoly R )
11 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( 0g ` Q ) e. _V )
12 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 ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) ) ) .* ( l .^ X ) ) e. _V )
13 oveq2 
 |-  ( l = n -> ( 0 ... l ) = ( 0 ... n ) )
14 oveq1 
 |-  ( l = n -> ( l - k ) = ( n - k ) )
15 14 oveq2d 
 |-  ( l = n -> ( y decompPMat ( l - k ) ) = ( y decompPMat ( n - k ) ) )
16 15 oveq2d 
 |-  ( l = n -> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) = ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) )
17 13 16 mpteq12dv 
 |-  ( l = n -> ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) ) = ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) )
18 17 oveq2d 
 |-  ( l = n -> ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) ) ) = ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) )
19 oveq1 
 |-  ( l = n -> ( l .^ X ) = ( n .^ X ) )
20 18 19 oveq12d 
 |-  ( l = n -> ( ( A gsum ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) ) ) .* ( l .^ X ) ) = ( ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) )
21 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> N e. Fin )
22 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> R e. Ring )
23 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
24 23 anim1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( C e. Ring /\ ( x e. B /\ y e. B ) ) )
25 3anass 
 |-  ( ( C e. Ring /\ x e. B /\ y e. B ) <-> ( C e. Ring /\ ( x e. B /\ y e. B ) ) )
26 24 25 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( C e. Ring /\ x e. B /\ y e. B ) )
27 eqid 
 |-  ( .r ` C ) = ( .r ` C )
28 3 27 ringcl 
 |-  ( ( C e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` C ) y ) e. B )
29 26 28 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` C ) y ) e. B )
30 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
31 1 2 3 30 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 ) ) )
32 21 22 29 31 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 ) ) )
33 fvoveq1 
 |-  ( a = i -> ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) = ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) )
34 33 fveq1d 
 |-  ( a = i -> ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) )
35 34 eqeq1d 
 |-  ( a = i -> ( ( ( coe1 ` ( a ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) ) )
36 oveq2 
 |-  ( b = j -> ( i ( x ( .r ` C ) y ) b ) = ( i ( x ( .r ` C ) y ) j ) )
37 36 fveq2d 
 |-  ( b = j -> ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) = ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) )
38 37 fveq1d 
 |-  ( b = j -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) = ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) )
39 38 eqeq1d 
 |-  ( b = j -> ( ( ( coe1 ` ( i ( x ( .r ` C ) y ) b ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) = ( 0g ` R ) ) )
40 35 39 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 ) )
41 40 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 ) ) )
42 41 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 ) ) )
43 42 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 ) )
44 43 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 ) ) )
45 7 30 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
46 45 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 ) ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
47 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
48 8 ply1sca 
 |-  ( A e. Ring -> A = ( Scalar ` Q ) )
49 47 48 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A = ( Scalar ` Q ) )
50 49 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 ) ) -> A = ( Scalar ` Q ) )
51 50 fveq2d 
 |-  ( ( ( ( ( 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 ) ) -> ( 0g ` A ) = ( 0g ` ( Scalar ` Q ) ) )
52 44 46 51 3eqtr2d 
 |-  ( ( ( ( ( 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 ` ( Scalar ` Q ) ) )
53 52 oveq1d 
 |-  ( ( ( ( ( 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 ) ) .* ( n .^ X ) ) = ( ( 0g ` ( Scalar ` Q ) ) .* ( n .^ X ) ) )
54 8 ply1lmod 
 |-  ( A e. Ring -> Q e. LMod )
55 47 54 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
56 55 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> Q e. LMod )
57 47 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> A e. Ring )
58 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
59 8 6 58 5 9 ply1moncl 
 |-  ( ( A e. Ring /\ n e. NN0 ) -> ( n .^ X ) e. L )
60 57 59 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( n .^ X ) e. L )
61 eqid 
 |-  ( Scalar ` Q ) = ( Scalar ` Q )
62 eqid 
 |-  ( 0g ` ( Scalar ` Q ) ) = ( 0g ` ( Scalar ` Q ) )
63 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
64 9 61 4 62 63 lmod0vs 
 |-  ( ( Q e. LMod /\ ( n .^ X ) e. L ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( n .^ X ) ) = ( 0g ` Q ) )
65 56 60 64 syl2an2r 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( n .^ X ) ) = ( 0g ` Q ) )
66 65 adantr 
 |-  ( ( ( ( ( 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 ) ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( n .^ X ) ) = ( 0g ` Q ) )
67 53 66 eqtrd 
 |-  ( ( ( ( ( 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 ) ) .* ( n .^ X ) ) = ( 0g ` Q ) )
68 67 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 ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) )
69 68 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 ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
70 69 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 ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
71 70 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 ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
72 32 71 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 ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) )
73 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 ) ) )
74 29 73 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 ) ) )
75 74 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) .* ( n .^ X ) ) )
76 75 eqeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) <-> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) )
77 76 imbi2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) <-> ( s < n -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
78 77 ralbidva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A. n e. NN0 ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) <-> A. n e. NN0 ( s < n -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
79 78 rexbidv 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( E. s e. NN0 A. n e. NN0 ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) <-> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` n ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
80 72 79 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) )
81 1 2 3 7 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 ) ) ) ) ) )
82 81 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 ) ) ) ) ) )
83 82 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) = ( ( x ( .r ` C ) y ) decompPMat n ) )
84 83 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ n e. NN0 ) -> ( ( A gsum ( k e. ( 0 ... n ) |-> ( ( x decompPMat k ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) = ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) )
85 84 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 ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) = ( 0g ` Q ) <-> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) )
86 85 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 ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) <-> ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
87 86 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 ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) <-> A. n e. NN0 ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
88 87 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 ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) <-> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( ( x ( .r ` C ) y ) decompPMat n ) .* ( n .^ X ) ) = ( 0g ` Q ) ) ) )
89 80 88 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 ) ( .r ` A ) ( y decompPMat ( n - k ) ) ) ) ) .* ( n .^ X ) ) = ( 0g ` Q ) ) )
90 11 12 20 89 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 ) ( .r ` A ) ( y decompPMat ( l - k ) ) ) ) ) .* ( l .^ X ) ) ) finSupp ( 0g ` Q ) )