Theorem m2cpminvid

Description: The inverse transformation applied to the transformation of a matrix over a ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019) (Revised by AV, 13-Dec-2019)

	Ref	Expression
Hypotheses	m2cpminvid.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
	m2cpminvid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpminvid.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
	m2cpminvid.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	m2cpminvid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑀 ) ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		m2cpminvid.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
2		m2cpminvid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		m2cpminvid.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
4		m2cpminvid.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
5		eqid	⊢ ( 𝑁 ConstPolyMat 𝑅 ) = ( 𝑁 ConstPolyMat 𝑅 )
6	5 4 2 3	m2cpm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( 𝑁 ConstPolyMat 𝑅 ) )
7	1 5	cpm2mval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( 𝑁 ConstPolyMat 𝑅 ) ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑀 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) ) ‘ 0 ) ) )
8	6 7	syld3an3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑀 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) ) ‘ 0 ) ) )
9		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
10		eqid	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
11	4 2 3 9 10	mat2pmatvalel	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 𝑀 𝑦 ) ) )
12	11	3impb	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 𝑀 𝑦 ) ) )
13	12	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( coe1 ‘ ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) ) = ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 𝑀 𝑦 ) ) ) )
14	13	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 𝑀 𝑦 ) ) ) ‘ 0 ) )
15		simp12	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ Ring )
16		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17		simp2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
18		simp3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
19		simp13	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑀 ∈ 𝐾 )
20	2 16 3 17 18 19	matecld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
21	9 10 16	ply1sclid	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 𝑀 𝑦 ) = ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 𝑀 𝑦 ) ) ) ‘ 0 ) )
22	15 20 21	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑀 𝑦 ) = ( ( coe1 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 𝑀 𝑦 ) ) ) ‘ 0 ) )
23	14 22	eqtr4d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) ) ‘ 0 ) = ( 𝑥 𝑀 𝑦 ) )
24	23	mpoeq3dva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 ( 𝑇 ‘ 𝑀 ) 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) )
25		eqidd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) )
26		oveq12	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑖 𝑀 𝑗 ) )
27	26	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑖 𝑀 𝑗 ) )
28		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
29		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
30		ovexd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ V )
31	25 27 28 29 30	ovmpod	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
32	31	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
33		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → 𝑁 ∈ Fin )
34		simp2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → 𝑅 ∈ Ring )
35	2 16 3 33 34 20	matbas2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) ∈ 𝐾 )
36		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → 𝑀 ∈ 𝐾 )
37	2 3	eqmat	⊢ ( ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) ∈ 𝐾 ∧ 𝑀 ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) = 𝑀 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) 𝑗 ) = ( 𝑖 𝑀 𝑗 ) ) )
38	35 36 37	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) = 𝑀 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) 𝑗 ) = ( 𝑖 𝑀 𝑗 ) ) )
39	32 38	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑥 𝑀 𝑦 ) ) = 𝑀 )
40	8 24 39	3eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑀 ) ) = 𝑀 )