cpm2mf

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

	Ref	Expression
Hypotheses	cpm2mf.a	$⊢ A = N Mat R$
	cpm2mf.k	$⊢ K = {Base}_{A}$
	cpm2mf.s	$⊢ S = N ConstPolyMat R$
	cpm2mf.i	$⊢ I = N cPolyMatToMat R$
Assertion	cpm2mf	$⊢ (N \in Fin \land R \in Ring) \to I : S ⟶ K$

Proof

Step	Hyp	Ref	Expression
1		cpm2mf.a	$⊢ A = N Mat R$
2		cpm2mf.k	$⊢ K = {Base}_{A}$
3		cpm2mf.s	$⊢ S = N ConstPolyMat R$
4		cpm2mf.i	$⊢ I = N cPolyMatToMat R$
5	4 3	cpm2mfval	$⊢ (N \in Fin \land R \in Ring) \to I = (m \in S ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)))$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		simpll	$⊢ ((N \in Fin \land R \in Ring) \land m \in S) \to N \in Fin$
8		simplr	$⊢ ((N \in Fin \land R \in Ring) \land m \in S) \to R \in Ring$
9		eqid	$⊢ N Mat {Poly}_{1} (R) = N Mat {Poly}_{1} (R)$
10		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
11		eqid	$⊢ {Base}_{(N Mat {Poly}_{1} (R))} = {Base}_{(N Mat {Poly}_{1} (R))}$
12		simp2	$⊢ (((N \in Fin \land R \in Ring) \land m \in S) \land x \in N \land y \in N) \to x \in N$
13		simp3	$⊢ (((N \in Fin \land R \in Ring) \land m \in S) \land x \in N \land y \in N) \to y \in N$
14		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
15	3 14 9 11	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land m \in S) \to m \in {Base}_{(N Mat {Poly}_{1} (R))}$
16	15	3expa	$⊢ ((N \in Fin \land R \in Ring) \land m \in S) \to m \in {Base}_{(N Mat {Poly}_{1} (R))}$
17	16	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land m \in S) \land x \in N \land y \in N) \to m \in {Base}_{(N Mat {Poly}_{1} (R))}$
18	9 10 11 12 13 17	matecld	$⊢ (((N \in Fin \land R \in Ring) \land m \in S) \land x \in N \land y \in N) \to x m y \in {Base}_{{Poly}_{1} (R)}$
19		0nn0	$⊢ 0 \in ℕ_{0}$
20		eqid	$⊢ {coe}_{1} (x m y) = {coe}_{1} (x m y)$
21	20 10 14 6	coe1fvalcl	$⊢ (x m y \in {Base}_{{Poly}_{1} (R)} \land 0 \in ℕ_{0}) \to {coe}_{1} (x m y) (0) \in {Base}_{R}$
22	18 19 21	sylancl	$⊢ (((N \in Fin \land R \in Ring) \land m \in S) \land x \in N \land y \in N) \to {coe}_{1} (x m y) (0) \in {Base}_{R}$
23	1 6 2 7 8 22	matbas2d	$⊢ ((N \in Fin \land R \in Ring) \land m \in S) \to (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)) \in K$
24	5 23	fmpt3d	$⊢ (N \in Fin \land R \in Ring) \to I : S ⟶ K$

Metamath Proof Explorer

Theorem cpm2mf

Proof