cpmidpmatlem3

Description: Lemma 3 for cpmidpmat . (Contributed by AV, 14-Nov-2019) (Proof shortened by AV, 7-Dec-2019)

	Ref	Expression
Hypotheses	cpmidgsum.a	$⊢ A = N Mat R$
	cpmidgsum.b	$⊢ B = {Base}_{A}$
	cpmidgsum.p	$⊢ P = {Poly}_{1} (R)$
	cpmidgsum.y	$⊢ Y = N Mat P$
	cpmidgsum.x	$⊢ X = {var}_{1} (R)$
	cpmidgsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	cpmidgsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmidgsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
	cpmidgsum.u	$⊢ U = algSc (P)$
	cpmidgsum.c	$⊢ C = N CharPlyMat R$
	cpmidgsum.k	$⊢ K = C (M)$
	cpmidgsum.h	$⊢ H = K \underset{˙}{\cdot} \underset{˙}{1}$
	cpmidgsumm2pm.o	$⊢ O = 1_{A}$
	cpmidgsumm2pm.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	cpmidgsumm2pm.t	$⊢ T = N matToPolyMat R$
	cpmidpmat.g	$⊢ G = (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{*} O)$
Assertion	cpmidpmatlem3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {finSupp}_{0_{A}} (G)$

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	$⊢ A = N Mat R$
2		cpmidgsum.b	$⊢ B = {Base}_{A}$
3		cpmidgsum.p	$⊢ P = {Poly}_{1} (R)$
4		cpmidgsum.y	$⊢ Y = N Mat P$
5		cpmidgsum.x	$⊢ X = {var}_{1} (R)$
6		cpmidgsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
7		cpmidgsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
8		cpmidgsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
9		cpmidgsum.u	$⊢ U = algSc (P)$
10		cpmidgsum.c	$⊢ C = N CharPlyMat R$
11		cpmidgsum.k	$⊢ K = C (M)$
12		cpmidgsum.h	$⊢ H = K \underset{˙}{\cdot} \underset{˙}{1}$
13		cpmidgsumm2pm.o	$⊢ O = 1_{A}$
14		cpmidgsumm2pm.m	$⊢ \underset{˙}{*} = \cdot_{A}$
15		cpmidgsumm2pm.t	$⊢ T = N matToPolyMat R$
16		cpmidpmat.g	$⊢ G = (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{*} O)$
17		fvexd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0_{A} \in V$
18		ovexd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in ℕ_{0}) \to {coe}_{1} (K) (k) \underset{˙}{*} O \in V$
19		fveq2	$⊢ k = l \to {coe}_{1} (K) (k) = {coe}_{1} (K) (l)$
20	19	oveq1d	$⊢ k = l \to {coe}_{1} (K) (k) \underset{˙}{} O = {coe}_{1} (K) (l) \underset{˙}{} O$
21		fvexd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0_{R} \in V$
22		eqid	$⊢ {Base}_{P} = {Base}_{P}$
23	10 1 2 3 22	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in {Base}_{P}$
24	11 23	eqeltrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K \in {Base}_{P}$
25		eqid	$⊢ {coe}_{1} (K) = {coe}_{1} (K)$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27	25 22 3 26	coe1fvalcl	$⊢ (K \in {Base}_{P} \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \in {Base}_{R}$
28	24 27	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \in {Base}_{R}$
29		crngring	$⊢ R \in CRing \to R \in Ring$
30	29	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
31		eqid	$⊢ 0_{R} = 0_{R}$
32	3 22 31	mptcoe1fsupp	$⊢ (R \in Ring \land K \in {Base}_{P}) \to {finSupp}_{0_{R}} ((n \in ℕ_{0} ⟼ {coe}_{1} (K) (n)))$
33	30 24 32	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {finSupp}_{0_{R}} ((n \in ℕ_{0} ⟼ {coe}_{1} (K) (n)))$
34	21 28 33	mptnn0fsuppr	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ_{0} \forall l \in ℕ_{0} (s < l \to ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R})$
35		csbfv	$⊢ ⦋ l / n ⦌ {coe}_{1} (K) (n) = {coe}_{1} (K) (l)$
36	35	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \to ⦋ l / n ⦌ {coe}_{1} (K) (n) = {coe}_{1} (K) (l)$
37	36	eqeq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \to (⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R} \leftrightarrow {coe}_{1} (K) (l) = 0_{R})$
38	37	biimpa	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to {coe}_{1} (K) (l) = 0_{R}$
39	1	matsca2	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (A)$
40	39	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R = Scalar (A)$
41	40	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to R = Scalar (A)$
42	41	fveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to 0_{R} = 0_{Scalar (A)}$
43	38 42	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to {coe}_{1} (K) (l) = 0_{Scalar (A)}$
44	43	oveq1d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to {coe}_{1} (K) (l) \underset{˙}{} O = 0_{Scalar (A)} \underset{˙}{} O$
45	1	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
46	29 45	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in LMod$
47	46	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in LMod$
48	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
49	29 48	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
50	2 13	ringidcl	$⊢ A \in Ring \to O \in B$
51	49 50	syl	$⊢ (N \in Fin \land R \in CRing) \to O \in B$
52	51	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to O \in B$
53		eqid	$⊢ Scalar (A) = Scalar (A)$
54		eqid	$⊢ 0_{Scalar (A)} = 0_{Scalar (A)}$
55		eqid	$⊢ 0_{A} = 0_{A}$
56	2 53 14 54 55	lmod0vs	$⊢ (A \in LMod \land O \in B) \to 0_{Scalar (A)} \underset{˙}{*} O = 0_{A}$
57	47 52 56	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0_{Scalar (A)} \underset{˙}{*} O = 0_{A}$
58	57	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to 0_{Scalar (A)} \underset{˙}{*} O = 0_{A}$
59	44 58	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \land ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to {coe}_{1} (K) (l) \underset{˙}{*} O = 0_{A}$
60	59	ex	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \to (⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R} \to {coe}_{1} (K) (l) \underset{˙}{*} O = 0_{A})$
61	60	imim2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land l \in ℕ_{0}) \to ((s < l \to ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to (s < l \to {coe}_{1} (K) (l) \underset{˙}{*} O = 0_{A}))$
62	61	ralimdva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\forall l \in ℕ_{0} (s < l \to ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to \forall l \in ℕ_{0} (s < l \to {coe}_{1} (K) (l) \underset{˙}{*} O = 0_{A}))$
63	62	reximdv	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists s \in ℕ_{0} \forall l \in ℕ_{0} (s < l \to ⦋ l / n ⦌ {coe}_{1} (K) (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall l \in ℕ_{0} (s < l \to {coe}_{1} (K) (l) \underset{˙}{*} O = 0_{A}))$
64	34 63	mpd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ_{0} \forall l \in ℕ_{0} (s < l \to {coe}_{1} (K) (l) \underset{˙}{*} O = 0_{A})$
65	17 18 20 64	mptnn0fsuppd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{*} O))$
66	16 65	eqbrtrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {finSupp}_{0_{A}} (G)$

Metamath Proof Explorer

Theorem cpmidpmatlem3

Proof