Theorem m2cpminv

Description: The inverse matrix transformation is a 1-1 function from the constant polynomial matrices onto the matrices over the base ring of the polynomials. (Contributed by AV, 27-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	m2cpminv.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpminv.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
	m2cpminv.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpminv.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
	m2cpminv.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	m2cpminv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼 : 𝑆 –1-1-onto→ 𝐾 ∧ ◡ 𝐼 = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		m2cpminv.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		m2cpminv.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
3		m2cpminv.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
4		m2cpminv.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
5		m2cpminv.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6	1 2 3 4	cpm2mf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆 ⟶ 𝐾 )
7	3 5 1 2	m2cpmf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 ⟶ 𝑆 )
8	3 4 5	m2cpminvid2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑠 ) ) = 𝑠 )
9	8	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑠 ) ) = 𝑠 )
10	9	ralrimiva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑠 ∈ 𝑆 ( 𝑇 ‘ ( 𝐼 ‘ 𝑠 ) ) = 𝑠 )
11	4 1 2 5	m2cpminvid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑘 ) ) = 𝑘 )
12	11	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑘 ) ) = 𝑘 )
13	12	ralrimiva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑘 ∈ 𝐾 ( 𝐼 ‘ ( 𝑇 ‘ 𝑘 ) ) = 𝑘 )
14	6 7 10 13	2fvidf1od	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆 –1-1-onto→ 𝐾 )
15	6 7 10 13	2fvidinvd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ◡ 𝐼 = 𝑇 )
16	14 15	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼 : 𝑆 –1-1-onto→ 𝐾 ∧ ◡ 𝐼 = 𝑇 ) )