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	eqtrid	⊢ ( ( ( 𝑁 ∈ 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	eqtrid	⊢ ( ( 𝑁 ∈ 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	eqtrid	⊢ ( ( 𝑁 ∈ 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 ) )