Metamath Proof Explorer

Theorem decpmatid

Description: The matrix consisting of the coefficients in the polynomial entries of the identity matrix is an identity or a zero matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

Ref Expression
Hypotheses decpmatid.p 
|- P = ( Poly1 ` R )
decpmatid.c 
|- C = ( N Mat P )
decpmatid.i 
|- I = ( 1r ` C )
decpmatid.a 
|- A = ( N Mat R )
decpmatid.0 
|- .0. = ( 0g ` A )
decpmatid.1 
|- .1. = ( 1r ` A )
Assertion decpmatid 
|- ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( I decompPMat K ) = if ( K = 0 , .1. , .0. ) )

Proof

Step Hyp Ref Expression
1 decpmatid.p 
 |-  P = ( Poly1 ` R )
2 decpmatid.c 
 |-  C = ( N Mat P )
3 decpmatid.i 
 |-  I = ( 1r ` C )
4 decpmatid.a 
 |-  A = ( N Mat R )
5 decpmatid.0 
 |-  .0. = ( 0g ` A )
6 decpmatid.1 
 |-  .1. = ( 1r ` A )
7 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
8 7 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> C e. Ring )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 9 3 ringidcl 
 |-  ( C e. Ring -> I e. ( Base ` C ) )
11 8 10 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> I e. ( Base ` C ) )
12 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> K e. NN0 )
13 2 9 decpmatval 
 |-  ( ( I e. ( Base ` C ) /\ K e. NN0 ) -> ( I decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i I j ) ) ` K ) ) )
14 11 12 13 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( I decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i I j ) ) ` K ) ) )
15 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
16 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
17 simp11 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> N e. Fin )
18 simp12 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
19 simp2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
20 simp3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
21 1 2 15 16 17 18 19 20 3 pmat1ovd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( i I j ) = if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) )
22 21 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( coe1 ` ( i I j ) ) = ( coe1 ` if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) )
23 22 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i I j ) ) ` K ) = ( ( coe1 ` if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) ` K ) )
24 fvif 
 |-  ( coe1 ` if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) = if ( i = j , ( coe1 ` ( 1r ` P ) ) , ( coe1 ` ( 0g ` P ) ) )
25 24 fveq1i 
 |-  ( ( coe1 ` if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) ` K ) = ( if ( i = j , ( coe1 ` ( 1r ` P ) ) , ( coe1 ` ( 0g ` P ) ) ) ` K )
26 iffv 
 |-  ( if ( i = j , ( coe1 ` ( 1r ` P ) ) , ( coe1 ` ( 0g ` P ) ) ) ` K ) = if ( i = j , ( ( coe1 ` ( 1r ` P ) ) ` K ) , ( ( coe1 ` ( 0g ` P ) ) ` K ) )
27 25 26 eqtri 
 |-  ( ( coe1 ` if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) ` K ) = if ( i = j , ( ( coe1 ` ( 1r ` P ) ) ` K ) , ( ( coe1 ` ( 0g ` P ) ) ` K ) )
28 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
29 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
30 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
31 1 28 29 30 ply1idvr1 
 |-  ( R e. Ring -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( 1r ` P ) )
32 31 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( 1r ` P ) )
33 32 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 1r ` P ) = ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
34 33 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( coe1 ` ( 1r ` P ) ) = ( coe1 ` ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
35 34 fveq1d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( coe1 ` ( 1r ` P ) ) ` K ) = ( ( coe1 ` ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` K ) )
36 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
37 36 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> P e. LMod )
38 0nn0 
 |-  0 e. NN0
39 eqid 
 |-  ( Base ` P ) = ( Base ` P )
40 1 28 29 30 39 ply1moncl 
 |-  ( ( R e. Ring /\ 0 e. NN0 ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
41 38 40 mpan2 
 |-  ( R e. Ring -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
42 41 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
43 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
44 eqid 
 |-  ( .s ` P ) = ( .s ` P )
45 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
46 39 43 44 45 lmodvs1 
 |-  ( ( P e. LMod /\ ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
47 37 42 46 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
48 47 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
49 48 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( coe1 ` ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( coe1 ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
50 49 fveq1d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( coe1 ` ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` K ) = ( ( coe1 ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` K ) )
51 simp2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> R e. Ring )
52 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
53 52 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> R = ( Scalar ` P ) )
54 53 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( Scalar ` P ) = R )
55 54 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 1r ` ( Scalar ` P ) ) = ( 1r ` R ) )
56 eqid 
 |-  ( Base ` R ) = ( Base ` R )
57 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
58 56 57 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
59 58 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 1r ` R ) e. ( Base ` R ) )
60 55 59 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 1r ` ( Scalar ` P ) ) e. ( Base ` R ) )
61 38 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> 0 e. NN0 )
62 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
63 62 56 1 28 44 29 30 coe1tm 
 |-  ( ( R e. Ring /\ ( 1r ` ( Scalar ` P ) ) e. ( Base ` R ) /\ 0 e. NN0 ) -> ( coe1 ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) ) )
64 51 60 61 63 syl3anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( coe1 ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) ) )
65 eqeq1 
 |-  ( k = K -> ( k = 0 <-> K = 0 ) )
66 65 ifbid 
 |-  ( k = K -> if ( k = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) = if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) )
67 66 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ k = K ) -> if ( k = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) = if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) )
68 fvex 
 |-  ( 1r ` ( Scalar ` P ) ) e. _V
69 fvex 
 |-  ( 0g ` R ) e. _V
70 68 69 ifex 
 |-  if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) e. _V
71 70 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) e. _V )
72 64 67 12 71 fvmptd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( coe1 ` ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` K ) = if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) )
73 35 50 72 3eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( coe1 ` ( 1r ` P ) ) ` K ) = if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) )
74 1 15 62 coe1z 
 |-  ( R e. Ring -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
75 74 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
76 75 fveq1d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( coe1 ` ( 0g ` P ) ) ` K ) = ( ( NN0 X. { ( 0g ` R ) } ) ` K ) )
77 69 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( 0g ` R ) e. _V )
78 fvconst2g 
 |-  ( ( ( 0g ` R ) e. _V /\ K e. NN0 ) -> ( ( NN0 X. { ( 0g ` R ) } ) ` K ) = ( 0g ` R ) )
79 77 12 78 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( NN0 X. { ( 0g ` R ) } ) ` K ) = ( 0g ` R ) )
80 76 79 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( ( coe1 ` ( 0g ` P ) ) ` K ) = ( 0g ` R ) )
81 73 80 ifeq12d 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> if ( i = j , ( ( coe1 ` ( 1r ` P ) ) ` K ) , ( ( coe1 ` ( 0g ` P ) ) ` K ) ) = if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
82 81 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> if ( i = j , ( ( coe1 ` ( 1r ` P ) ) ` K ) , ( ( coe1 ` ( 0g ` P ) ) ` K ) ) = if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
83 27 82 syl5eq 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) ` K ) = if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
84 23 83 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i I j ) ) ` K ) = if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
85 84 mpoeq3dva 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i I j ) ) ` K ) ) = ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) )
86 53 adantl 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> R = ( Scalar ` P ) )
87 86 eqcomd 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( Scalar ` P ) = R )
88 87 fveq2d 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( 1r ` ( Scalar ` P ) ) = ( 1r ` R ) )
89 88 ifeq1d 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> if ( i = j , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
90 89 mpoeq3dv 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
91 iftrue 
 |-  ( K = 0 -> if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) = ( 1r ` ( Scalar ` P ) ) )
92 91 ifeq1d 
 |-  ( K = 0 -> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) )
93 92 adantr 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) )
94 93 mpoeq3dv 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) ) )
95 4 57 62 mat1 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
96 6 95 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
97 96 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> .1. = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
98 97 adantl 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> .1. = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
99 90 94 98 3eqtr4d 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = .1. )
100 iftrue 
 |-  ( K = 0 -> if ( K = 0 , .1. , .0. ) = .1. )
101 100 eqcomd 
 |-  ( K = 0 -> .1. = if ( K = 0 , .1. , .0. ) )
102 101 adantr 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> .1. = if ( K = 0 , .1. , .0. ) )
103 99 102 eqtrd 
 |-  ( ( K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( K = 0 , .1. , .0. ) )
104 ifid 
 |-  if ( i = j , ( 0g ` R ) , ( 0g ` R ) ) = ( 0g ` R )
105 104 a1i 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> if ( i = j , ( 0g ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
106 105 mpoeq3dv 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , ( 0g ` R ) , ( 0g ` R ) ) ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
107 iffalse 
 |-  ( -. K = 0 -> if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) = ( 0g ` R ) )
108 107 adantr 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) = ( 0g ` R ) )
109 108 ifeq1d 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) = if ( i = j , ( 0g ` R ) , ( 0g ` R ) ) )
110 109 mpoeq3dv 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = ( i e. N , j e. N |-> if ( i = j , ( 0g ` R ) , ( 0g ` R ) ) ) )
111 3simpa 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( N e. Fin /\ R e. Ring ) )
112 111 adantl 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( N e. Fin /\ R e. Ring ) )
113 4 62 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
114 5 113 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. = ( i e. N , j e. N |-> ( 0g ` R ) ) )
115 112 114 syl 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> .0. = ( i e. N , j e. N |-> ( 0g ` R ) ) )
116 106 110 115 3eqtr4d 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = .0. )
117 iffalse 
 |-  ( -. K = 0 -> if ( K = 0 , .1. , .0. ) = .0. )
118 117 eqcomd 
 |-  ( -. K = 0 -> .0. = if ( K = 0 , .1. , .0. ) )
119 118 adantr 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> .0. = if ( K = 0 , .1. , .0. ) )
120 116 119 eqtrd 
 |-  ( ( -. K = 0 /\ ( N e. Fin /\ R e. Ring /\ K e. NN0 ) ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( K = 0 , .1. , .0. ) )
121 103 120 pm2.61ian 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( i e. N , j e. N |-> if ( i = j , if ( K = 0 , ( 1r ` ( Scalar ` P ) ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( K = 0 , .1. , .0. ) )
122 14 85 121 3eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( I decompPMat K ) = if ( K = 0 , .1. , .0. ) )