m2cpminv0

Description: The inverse matrix transformation applied to the zero polynomial matrix results in the zero of the matrices over the base ring of the polynomials. (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	m2cpminv0.a	$⊢ A = N Mat R$
	m2cpminv0.i	$⊢ I = N cPolyMatToMat R$
	m2cpminv0.p	$⊢ P = {Poly}_{1} (R)$
	m2cpminv0.c	$⊢ C = N Mat P$
	m2cpminv0.0	$⊢ \underset{˙}{0} = 0_{A}$
	m2cpminv0.z	$⊢ Z = 0_{C}$
Assertion	m2cpminv0	$⊢ (N \in Fin \land R \in Ring) \to I (Z) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		m2cpminv0.a	$⊢ A = N Mat R$
2		m2cpminv0.i	$⊢ I = N cPolyMatToMat R$
3		m2cpminv0.p	$⊢ P = {Poly}_{1} (R)$
4		m2cpminv0.c	$⊢ C = N Mat P$
5		m2cpminv0.0	$⊢ \underset{˙}{0} = 0_{A}$
6		m2cpminv0.z	$⊢ Z = 0_{C}$
7		eqid	$⊢ N matToPolyMat R = N matToPolyMat R$
8	1	fveq2i	$⊢ 0_{A} = 0_{(N Mat R)}$
9	5 8	eqtri	$⊢ \underset{˙}{0} = 0_{(N Mat R)}$
10	4	fveq2i	$⊢ 0_{C} = 0_{(N Mat P)}$
11	6 10	eqtri	$⊢ Z = 0_{(N Mat P)}$
12	7 3 9 11	0mat2pmat	$⊢ (R \in Ring \land N \in Fin) \to (N matToPolyMat R) (\underset{˙}{0}) = Z$
13	12	ancoms	$⊢ (N \in Fin \land R \in Ring) \to (N matToPolyMat R) (\underset{˙}{0}) = Z$
14	13	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to Z = (N matToPolyMat R) (\underset{˙}{0})$
15	14	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to I (Z) = I ((N matToPolyMat R) (\underset{˙}{0}))$
16	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
17		eqid	$⊢ {Base}_{A} = {Base}_{A}$
18	17 5	ring0cl	$⊢ A \in Ring \to \underset{˙}{0} \in {Base}_{A}$
19	16 18	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} \in {Base}_{A}$
20	2 1 17 7	m2cpminvid	$⊢ (N \in Fin \land R \in Ring \land \underset{˙}{0} \in {Base}_{A}) \to I ((N matToPolyMat R) (\underset{˙}{0})) = \underset{˙}{0}$
21	19 20	mpd3an3	$⊢ (N \in Fin \land R \in Ring) \to I ((N matToPolyMat R) (\underset{˙}{0})) = \underset{˙}{0}$
22	15 21	eqtrd	$⊢ (N \in Fin \land R \in Ring) \to I (Z) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem m2cpminv0

Proof