Metamath Proof Explorer

Theorem pmatcollpw2lem

Description: Lemma for pmatcollpw2 . (Contributed by AV, 3-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses pmatcollpw1.p 
|- P = ( Poly1 ` R )
pmatcollpw1.c 
|- C = ( N Mat P )
pmatcollpw1.b 
|- B = ( Base ` C )
pmatcollpw1.m 
|- .X. = ( .s ` P )
pmatcollpw1.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw1.x 
|- X = ( var1 ` R )
Assertion pmatcollpw2lem 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) finSupp ( 0g ` C ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw1.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw1.c 
 |-  C = ( N Mat P )
3 pmatcollpw1.b 
 |-  B = ( Base ` C )
4 pmatcollpw1.m 
 |-  .X. = ( .s ` P )
5 pmatcollpw1.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw1.x 
 |-  X = ( var1 ` R )
7 simp1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> N e. Fin )
8 mpoexga 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) e. _V )
9 7 7 8 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) e. _V )
10 9 ralrimivw 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A. n e. NN0 ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) e. _V )
11 eqid 
 |-  ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) = ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) )
12 11 fnmpt 
 |-  ( A. n e. NN0 ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) e. _V -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) Fn NN0 )
13 10 12 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) Fn NN0 )
14 nn0ex 
 |-  NN0 e. _V
15 14 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> NN0 e. _V )
16 fvexd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( 0g ` C ) e. _V )
17 suppvalfn 
 |-  ( ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) Fn NN0 /\ NN0 e. _V /\ ( 0g ` C ) e. _V ) -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) supp ( 0g ` C ) ) = { x e. NN0 | ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) } )
18 13 15 16 17 syl3anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) supp ( 0g ` C ) ) = { x e. NN0 | ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) } )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 1 2 3 19 pmatcoe1fsupp 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) )
21 oveq1 
 |-  ( ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) -> ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( ( 0g ` R ) .X. ( x .^ X ) ) )
22 4 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .X. = ( .s ` P ) )
23 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
24 23 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> R = ( Scalar ` P ) )
25 24 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
26 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( x .^ X ) = ( x .^ X ) )
27 22 25 26 oveq123d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( 0g ` R ) .X. ( x .^ X ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( x .^ X ) ) )
28 27 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( ( 0g ` R ) .X. ( x .^ X ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( x .^ X ) ) )
29 24 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( Scalar ` P ) = R )
30 29 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( Scalar ` P ) = R )
31 30 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( 0g ` ( Scalar ` P ) ) = ( 0g ` R ) )
32 31 oveq1d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( x .^ X ) ) = ( ( 0g ` R ) ( .s ` P ) ( x .^ X ) ) )
33 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> R e. Ring )
34 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
35 eqid 
 |-  ( Base ` P ) = ( Base ` P )
36 1 6 34 5 35 ply1moncl 
 |-  ( ( R e. Ring /\ x e. NN0 ) -> ( x .^ X ) e. ( Base ` P ) )
37 36 3ad2antl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( x .^ X ) e. ( Base ` P ) )
38 33 37 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( R e. Ring /\ ( x .^ X ) e. ( Base ` P ) ) )
39 38 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) -> ( R e. Ring /\ ( x .^ X ) e. ( Base ` P ) ) )
40 39 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( R e. Ring /\ ( x .^ X ) e. ( Base ` P ) ) )
41 eqid 
 |-  ( .s ` P ) = ( .s ` P )
42 1 35 41 19 ply10s0 
 |-  ( ( R e. Ring /\ ( x .^ X ) e. ( Base ` P ) ) -> ( ( 0g ` R ) ( .s ` P ) ( x .^ X ) ) = ( 0g ` P ) )
43 40 42 syl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( ( 0g ` R ) ( .s ` P ) ( x .^ X ) ) = ( 0g ` P ) )
44 28 32 43 3eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( ( 0g ` R ) .X. ( x .^ X ) ) = ( 0g ` P ) )
45 21 44 sylan9eqr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) /\ ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) -> ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) )
46 45 ex 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ i e. N ) /\ j e. N ) -> ( ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) -> ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
47 46 anasss 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) -> ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
48 47 ralimdvva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
49 48 imim2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( y < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) -> ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
50 49 ralimdva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) -> A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
51 50 reximdv 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) -> E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
52 20 51 mpd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
53 simpl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> M e. B )
54 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> x e. NN0 )
55 33 53 54 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( R e. Ring /\ M e. B /\ x e. NN0 ) )
56 1 2 3 decpmate 
 |-  ( ( ( R e. Ring /\ M e. B /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( M decompPMat x ) j ) = ( ( coe1 ` ( i M j ) ) ` x ) )
57 55 56 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( M decompPMat x ) j ) = ( ( coe1 ` ( i M j ) ) ` x ) )
58 57 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) )
59 58 eqeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) <-> ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
60 59 2ralbidva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) <-> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
61 60 imbi2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( y < x -> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) <-> ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
62 61 ralbidva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) <-> A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
63 62 rexbidv 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) <-> E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( ( coe1 ` ( i M j ) ) ` x ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
64 52 63 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
65 eqid 
 |-  N = N
66 65 biantrur 
 |-  ( A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) <-> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
67 65 biantrur 
 |-  ( A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) <-> ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
68 67 bicomi 
 |-  ( ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) <-> A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) )
69 68 ralbii 
 |-  ( A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) <-> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) )
70 66 69 bitr3i 
 |-  ( ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) <-> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) )
71 70 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) <-> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) )
72 71 imbi2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( y < x -> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) ) <-> ( y < x -> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
73 72 rexralbidv 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( E. y e. NN0 A. x e. NN0 ( y < x -> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) ) <-> E. y e. NN0 A. x e. NN0 ( y < x -> A. i e. N A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) )
74 64 73 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) ) )
75 mpoeq123 
 |-  ( ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) )
76 75 imim2i 
 |-  ( ( y < x -> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) ) -> ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) )
77 76 ralimi 
 |-  ( A. x e. NN0 ( y < x -> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) ) -> A. x e. NN0 ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) )
78 77 reximi 
 |-  ( E. y e. NN0 A. x e. NN0 ( y < x -> ( N = N /\ A. i e. N ( N = N /\ A. j e. N ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) = ( 0g ` P ) ) ) ) -> E. y e. NN0 A. x e. NN0 ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) )
79 74 78 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) )
80 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) = ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) )
81 oveq2 
 |-  ( n = x -> ( M decompPMat n ) = ( M decompPMat x ) )
82 81 oveqd 
 |-  ( n = x -> ( i ( M decompPMat n ) j ) = ( i ( M decompPMat x ) j ) )
83 oveq1 
 |-  ( n = x -> ( n .^ X ) = ( x .^ X ) )
84 82 83 oveq12d 
 |-  ( n = x -> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) = ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) )
85 84 mpoeq3dv 
 |-  ( n = x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) = ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) )
86 85 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ n = x ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) = ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) )
87 id 
 |-  ( N e. Fin -> N e. Fin )
88 87 ancri 
 |-  ( N e. Fin -> ( N e. Fin /\ N e. Fin ) )
89 88 3ad2ant1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ N e. Fin ) )
90 89 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( N e. Fin /\ N e. Fin ) )
91 mpoexga 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) e. _V )
92 90 91 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) e. _V )
93 80 86 54 92 fvmptd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) )
94 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
95 94 anim2i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring ) )
96 95 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )
97 96 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( N e. Fin /\ P e. Ring ) )
98 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
99 2 98 mat0op 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( 0g ` C ) = ( i e. N , j e. N |-> ( 0g ` P ) ) )
100 97 99 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( 0g ` C ) = ( i e. N , j e. N |-> ( 0g ` P ) ) )
101 93 100 eqeq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) <-> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) )
102 101 imbi2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) <-> ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) ) )
103 102 ralbidva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( A. x e. NN0 ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) <-> A. x e. NN0 ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) ) )
104 103 rexbidv 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( E. y e. NN0 A. x e. NN0 ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) <-> E. y e. NN0 A. x e. NN0 ( y < x -> ( i e. N , j e. N |-> ( ( i ( M decompPMat x ) j ) .X. ( x .^ X ) ) ) = ( i e. N , j e. N |-> ( 0g ` P ) ) ) ) )
105 79 104 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) )
106 nne 
 |-  ( -. ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) <-> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) )
107 106 imbi2i 
 |-  ( ( y < x -> -. ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) ) <-> ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) )
108 107 ralbii 
 |-  ( A. x e. NN0 ( y < x -> -. ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) ) <-> A. x e. NN0 ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) )
109 108 rexbii 
 |-  ( E. y e. NN0 A. x e. NN0 ( y < x -> -. ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) ) <-> E. y e. NN0 A. x e. NN0 ( y < x -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) = ( 0g ` C ) ) )
110 105 109 sylibr 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. y e. NN0 A. x e. NN0 ( y < x -> -. ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) ) )
111 rabssnn0fi 
 |-  ( { x e. NN0 | ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) } e. Fin <-> E. y e. NN0 A. x e. NN0 ( y < x -> -. ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) ) )
112 110 111 sylibr 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> { x e. NN0 | ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ` x ) =/= ( 0g ` C ) } e. Fin )
113 18 112 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) supp ( 0g ` C ) ) e. Fin )
114 funmpt 
 |-  Fun ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) )
115 14 mptex 
 |-  ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) e. _V
116 funisfsupp 
 |-  ( ( Fun ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) /\ ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) e. _V /\ ( 0g ` C ) e. _V ) -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) finSupp ( 0g ` C ) <-> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) supp ( 0g ` C ) ) e. Fin ) )
117 114 115 16 116 mp3an12i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) finSupp ( 0g ` C ) <-> ( ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) supp ( 0g ` C ) ) e. Fin ) )
118 113 117 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) finSupp ( 0g ` C ) )