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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
decpmatid.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
decpmatid.i ⊢ 𝐼 = ( 1r ‘ 𝐶 )
decpmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
decpmatid.0 ⊢ 0 = ( 0g ‘ 𝐴 )
decpmatid.1 ⊢ 1 = ( 1r ‘ 𝐴 )
Assertion decpmatid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 decompPMat 𝐾 ) = if ( 𝐾 = 0 , 1 , 0 ) )

Proof

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