Theorem mat2pmat1

Description: The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
Assertion	mat2pmat1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
7		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
8		simpr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
9	2	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
10		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
11	3 10	ringidcl	⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
12	9 11	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
13	7 8 12	3jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) )
14		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
15	1 2 3 4 14	mat2pmatvalel	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ) )
16	13 15	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ) )
17		fvif	⊢ ( ( algSc ‘ 𝑃 ) ‘ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) )
18		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
20	4 14 18 19	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
21	20	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
22		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
23		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
24	4 14 22 23	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
25	24	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
26	21 25	ifeq12d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
27	17 26	eqtrid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
28	7	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
29	8	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
30		simpl	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
31	30	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
32		simpr	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
33	32	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
34	2 18 22 28 29 31 33 10	mat1ov	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
35	34	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
36	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
37	36	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑃 ∈ Ring )
38		eqid	⊢ ( 1r ‘ 𝐶 ) = ( 1r ‘ 𝐶 )
39	5 19 23 28 37 31 33 38	mat1ov	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 1r ‘ 𝐶 ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
40	27 35 39	3eqtr4d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ) = ( 𝑖 ( 1r ‘ 𝐶 ) 𝑗 ) )
41	16 40	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r ‘ 𝐶 ) 𝑗 ) )
42	41	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r ‘ 𝐶 ) 𝑗 ) )
43	1 2 3 4 5 6	mat2pmatbas0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐻 )
44	13 43	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐻 )
45	4 5	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
46	6 38	ringidcl	⊢ ( 𝐶 ∈ Ring → ( 1r ‘ 𝐶 ) ∈ 𝐻 )
47	45 46	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) ∈ 𝐻 )
48	5 6	eqmat	⊢ ( ( ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐻 ∧ ( 1r ‘ 𝐶 ) ∈ 𝐻 ) → ( ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r ‘ 𝐶 ) 𝑗 ) ) )
49	44 47 48	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r ‘ 𝐶 ) 𝑗 ) ) )
50	42 49	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) )