Metamath Proof Explorer

Theorem monmatcollpw

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid (but requires R to be commutative!). (Contributed by AV, 11-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses monmatcollpw.p 
|- P = ( Poly1 ` R )
monmatcollpw.c 
|- C = ( N Mat P )
monmatcollpw.a 
|- A = ( N Mat R )
monmatcollpw.k 
|- K = ( Base ` A )
monmatcollpw.0 
|- .0. = ( 0g ` A )
monmatcollpw.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
monmatcollpw.x 
|- X = ( var1 ` R )
monmatcollpw.m 
|- .x. = ( .s ` C )
monmatcollpw.t 
|- T = ( N matToPolyMat R )
Assertion monmatcollpw 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( ( L .^ X ) .x. ( T ` M ) ) decompPMat I ) = if ( I = L , M , .0. ) )

Proof

Step Hyp Ref Expression
1 monmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 monmatcollpw.c 
 |-  C = ( N Mat P )
3 monmatcollpw.a 
 |-  A = ( N Mat R )
4 monmatcollpw.k 
 |-  K = ( Base ` A )
5 monmatcollpw.0 
 |-  .0. = ( 0g ` A )
6 monmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
7 monmatcollpw.x 
 |-  X = ( var1 ` R )
8 monmatcollpw.m 
 |-  .x. = ( .s ` C )
9 monmatcollpw.t 
 |-  T = ( N matToPolyMat R )
10 simpll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> N e. Fin )
11 crngring 
 |-  ( R e. CRing -> R e. Ring )
12 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
13 11 12 syl 
 |-  ( R e. CRing -> P e. Ring )
14 13 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> P e. Ring )
15 11 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
16 simp2 
 |-  ( ( M e. K /\ L e. NN0 /\ I e. NN0 ) -> L e. NN0 )
17 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
18 eqid 
 |-  ( Base ` P ) = ( Base ` P )
19 1 7 17 6 18 ply1moncl 
 |-  ( ( R e. Ring /\ L e. NN0 ) -> ( L .^ X ) e. ( Base ` P ) )
20 15 16 19 syl2an 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( L .^ X ) e. ( Base ` P ) )
21 11 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
22 simp1 
 |-  ( ( M e. K /\ L e. NN0 /\ I e. NN0 ) -> M e. K )
23 21 22 anim12i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ M e. K ) )
24 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) <-> ( ( N e. Fin /\ R e. Ring ) /\ M e. K ) )
25 23 24 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( N e. Fin /\ R e. Ring /\ M e. K ) )
26 9 3 4 1 2 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( T ` M ) e. ( Base ` C ) )
27 25 26 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( T ` M ) e. ( Base ` C ) )
28 20 27 jca 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( L .^ X ) e. ( Base ` P ) /\ ( T ` M ) e. ( Base ` C ) ) )
29 eqid 
 |-  ( Base ` C ) = ( Base ` C )
30 18 2 29 8 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( L .^ X ) e. ( Base ` P ) /\ ( T ` M ) e. ( Base ` C ) ) ) -> ( ( L .^ X ) .x. ( T ` M ) ) e. ( Base ` C ) )
31 10 14 28 30 syl21anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( L .^ X ) .x. ( T ` M ) ) e. ( Base ` C ) )
32 simpr3 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> I e. NN0 )
33 2 29 decpmatval 
 |-  ( ( ( ( L .^ X ) .x. ( T ` M ) ) e. ( Base ` C ) /\ I e. NN0 ) -> ( ( ( L .^ X ) .x. ( T ` M ) ) decompPMat I ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) ) ` I ) ) )
34 31 32 33 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( ( L .^ X ) .x. ( T ` M ) ) decompPMat I ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) ) ` I ) ) )
35 14 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> P e. Ring )
36 28 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( L .^ X ) e. ( Base ` P ) /\ ( T ` M ) e. ( Base ` C ) ) )
37 3simpc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( i e. N /\ j e. N ) )
38 eqid 
 |-  ( .r ` P ) = ( .r ` P )
39 2 29 18 8 38 matvscacell 
 |-  ( ( P e. Ring /\ ( ( L .^ X ) e. ( Base ` P ) /\ ( T ` M ) e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) = ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) )
40 35 36 37 39 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) = ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) )
41 40 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( coe1 ` ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) ) = ( coe1 ` ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) ) )
42 41 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) ) ` I ) = ( ( coe1 ` ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) ) ` I ) )
43 22 anim2i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( N e. Fin /\ R e. CRing ) /\ M e. K ) )
44 df-3an 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. K ) <-> ( ( N e. Fin /\ R e. CRing ) /\ M e. K ) )
45 43 44 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( N e. Fin /\ R e. CRing /\ M e. K ) )
46 45 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( N e. Fin /\ R e. CRing /\ M e. K ) )
47 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
48 9 3 4 1 47 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` M ) j ) = ( ( algSc ` P ) ` ( i M j ) ) )
49 46 37 48 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( i ( T ` M ) j ) = ( ( algSc ` P ) ` ( i M j ) ) )
50 49 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) = ( ( L .^ X ) ( .r ` P ) ( ( algSc ` P ) ` ( i M j ) ) ) )
51 1 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
52 51 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> P e. AssAlg )
53 52 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> P e. AssAlg )
54 eqid 
 |-  ( Base ` R ) = ( Base ` R )
55 eqid 
 |-  ( Base ` A ) = ( Base ` A )
56 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> i e. N )
57 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> j e. N )
58 4 eleq2i 
 |-  ( M e. K <-> M e. ( Base ` A ) )
59 58 biimpi 
 |-  ( M e. K -> M e. ( Base ` A ) )
60 59 3ad2ant1 
 |-  ( ( M e. K /\ L e. NN0 /\ I e. NN0 ) -> M e. ( Base ` A ) )
61 60 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> M e. ( Base ` A ) )
62 61 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> M e. ( Base ` A ) )
63 3 54 55 56 57 62 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` R ) )
64 1 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
65 64 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` P ) )
66 65 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` P ) = R )
67 66 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
68 67 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
69 68 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
70 63 69 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` ( Scalar ` P ) ) )
71 20 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( L .^ X ) e. ( Base ` P ) )
72 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
73 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
74 eqid 
 |-  ( .s ` P ) = ( .s ` P )
75 47 72 73 18 38 74 asclmul2 
 |-  ( ( P e. AssAlg /\ ( i M j ) e. ( Base ` ( Scalar ` P ) ) /\ ( L .^ X ) e. ( Base ` P ) ) -> ( ( L .^ X ) ( .r ` P ) ( ( algSc ` P ) ` ( i M j ) ) ) = ( ( i M j ) ( .s ` P ) ( L .^ X ) ) )
76 53 70 71 75 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( L .^ X ) ( .r ` P ) ( ( algSc ` P ) ` ( i M j ) ) ) = ( ( i M j ) ( .s ` P ) ( L .^ X ) ) )
77 50 76 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) = ( ( i M j ) ( .s ` P ) ( L .^ X ) ) )
78 77 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( coe1 ` ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) ) = ( coe1 ` ( ( i M j ) ( .s ` P ) ( L .^ X ) ) ) )
79 78 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( ( L .^ X ) ( .r ` P ) ( i ( T ` M ) j ) ) ) ` I ) = ( ( coe1 ` ( ( i M j ) ( .s ` P ) ( L .^ X ) ) ) ` I ) )
80 11 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> R e. Ring )
81 80 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> R e. Ring )
82 simp1r2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> L e. NN0 )
83 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
84 83 54 1 7 74 17 6 coe1tm 
 |-  ( ( R e. Ring /\ ( i M j ) e. ( Base ` R ) /\ L e. NN0 ) -> ( coe1 ` ( ( i M j ) ( .s ` P ) ( L .^ X ) ) ) = ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) )
85 81 63 82 84 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( coe1 ` ( ( i M j ) ( .s ` P ) ( L .^ X ) ) ) = ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) )
86 85 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( ( i M j ) ( .s ` P ) ( L .^ X ) ) ) ` I ) = ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) )
87 42 79 86 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) ) ` I ) = ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) )
88 87 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i ( ( L .^ X ) .x. ( T ` M ) ) j ) ) ` I ) ) = ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) )
89 21 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( N e. Fin /\ R e. Ring ) )
90 89 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( N e. Fin /\ R e. Ring ) )
91 3 83 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( z e. N , w e. N |-> ( 0g ` R ) ) )
92 90 91 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( 0g ` A ) = ( z e. N , w e. N |-> ( 0g ` R ) ) )
93 5 92 syl5eq 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> .0. = ( z e. N , w e. N |-> ( 0g ` R ) ) )
94 eqidd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) /\ ( z = x /\ w = y ) ) -> ( 0g ` R ) = ( 0g ` R ) )
95 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> x e. N )
96 simprr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> y e. N )
97 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( 0g ` R ) e. _V )
98 93 94 95 96 97 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( x .0. y ) = ( 0g ` R ) )
99 98 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( 0g ` R ) = ( x .0. y ) )
100 99 ifeq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> if ( I = L , ( x M y ) , ( 0g ` R ) ) = if ( I = L , ( x M y ) , ( x .0. y ) ) )
101 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) = ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) )
102 oveq12 
 |-  ( ( i = x /\ j = y ) -> ( i M j ) = ( x M y ) )
103 102 ifeq1d 
 |-  ( ( i = x /\ j = y ) -> if ( l = L , ( i M j ) , ( 0g ` R ) ) = if ( l = L , ( x M y ) , ( 0g ` R ) ) )
104 103 mpteq2dv 
 |-  ( ( i = x /\ j = y ) -> ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) = ( l e. NN0 |-> if ( l = L , ( x M y ) , ( 0g ` R ) ) ) )
105 104 fveq1d 
 |-  ( ( i = x /\ j = y ) -> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) = ( ( l e. NN0 |-> if ( l = L , ( x M y ) , ( 0g ` R ) ) ) ` I ) )
106 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( l e. NN0 |-> if ( l = L , ( x M y ) , ( 0g ` R ) ) ) = ( l e. NN0 |-> if ( l = L , ( x M y ) , ( 0g ` R ) ) ) )
107 eqeq1 
 |-  ( l = I -> ( l = L <-> I = L ) )
108 107 ifbid 
 |-  ( l = I -> if ( l = L , ( x M y ) , ( 0g ` R ) ) = if ( I = L , ( x M y ) , ( 0g ` R ) ) )
109 108 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) /\ l = I ) -> if ( l = L , ( x M y ) , ( 0g ` R ) ) = if ( I = L , ( x M y ) , ( 0g ` R ) ) )
110 32 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> I e. NN0 )
111 ovex 
 |-  ( x M y ) e. _V
112 fvex 
 |-  ( 0g ` R ) e. _V
113 111 112 ifex 
 |-  if ( I = L , ( x M y ) , ( 0g ` R ) ) e. _V
114 113 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> if ( I = L , ( x M y ) , ( 0g ` R ) ) e. _V )
115 106 109 110 114 fvmptd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( ( l e. NN0 |-> if ( l = L , ( x M y ) , ( 0g ` R ) ) ) ` I ) = if ( I = L , ( x M y ) , ( 0g ` R ) ) )
116 105 115 sylan9eqr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) /\ ( i = x /\ j = y ) ) -> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) = if ( I = L , ( x M y ) , ( 0g ` R ) ) )
117 101 116 95 96 114 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( x ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) y ) = if ( I = L , ( x M y ) , ( 0g ` R ) ) )
118 ifov 
 |-  ( x if ( I = L , M , .0. ) y ) = if ( I = L , ( x M y ) , ( x .0. y ) )
119 118 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( x if ( I = L , M , .0. ) y ) = if ( I = L , ( x M y ) , ( x .0. y ) ) )
120 100 117 119 3eqtr4d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ ( x e. N /\ y e. N ) ) -> ( x ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) y ) = ( x if ( I = L , M , .0. ) y ) )
121 120 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) y ) = ( x if ( I = L , M , .0. ) y ) )
122 simplr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> R e. CRing )
123 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) = ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) )
124 107 ifbid 
 |-  ( l = I -> if ( l = L , ( i M j ) , ( 0g ` R ) ) = if ( I = L , ( i M j ) , ( 0g ` R ) ) )
125 124 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) /\ l = I ) -> if ( l = L , ( i M j ) , ( 0g ` R ) ) = if ( I = L , ( i M j ) , ( 0g ` R ) ) )
126 32 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> I e. NN0 )
127 54 83 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
128 15 127 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( 0g ` R ) e. ( Base ` R ) )
129 128 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( 0g ` R ) e. ( Base ` R ) )
130 129 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( 0g ` R ) e. ( Base ` R ) )
131 63 130 ifcld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> if ( I = L , ( i M j ) , ( 0g ` R ) ) e. ( Base ` R ) )
132 123 125 126 131 fvmptd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) = if ( I = L , ( i M j ) , ( 0g ` R ) ) )
133 132 131 eqeltrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) /\ i e. N /\ j e. N ) -> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) e. ( Base ` R ) )
134 3 54 4 10 122 133 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) e. K )
135 61 58 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> M e. K )
136 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
137 4 5 ring0cl 
 |-  ( A e. Ring -> .0. e. K )
138 21 136 137 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> .0. e. K )
139 138 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> .0. e. K )
140 135 139 ifcld 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> if ( I = L , M , .0. ) e. K )
141 3 4 eqmat 
 |-  ( ( ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) e. K /\ if ( I = L , M , .0. ) e. K ) -> ( ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) = if ( I = L , M , .0. ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) y ) = ( x if ( I = L , M , .0. ) y ) ) )
142 134 140 141 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) = if ( I = L , M , .0. ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) y ) = ( x if ( I = L , M , .0. ) y ) ) )
143 121 142 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( i e. N , j e. N |-> ( ( l e. NN0 |-> if ( l = L , ( i M j ) , ( 0g ` R ) ) ) ` I ) ) = if ( I = L , M , .0. ) )
144 34 88 143 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( ( L .^ X ) .x. ( T ` M ) ) decompPMat I ) = if ( I = L , M , .0. ) )