cpmidpmatlem2

Description: Lemma 2 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	cpmidpmatlem2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to G \in (B^{ℕ_{0}})$

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		simpl1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in ℕ_{0}) \to N \in Fin$
18		crngring	$⊢ R \in CRing \to R \in Ring$
19	18	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
20	19	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in ℕ_{0}) \to R \in Ring$
21		eqid	$⊢ {Base}_{P} = {Base}_{P}$
22	10 1 2 3 21	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in {Base}_{P}$
23	11 22	eqeltrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K \in {Base}_{P}$
24		eqid	$⊢ {coe}_{1} (K) = {coe}_{1} (K)$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26	24 21 3 25	coe1fvalcl	$⊢ (K \in {Base}_{P} \land k \in ℕ_{0}) \to {coe}_{1} (K) (k) \in {Base}_{R}$
27	23 26	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in ℕ_{0}) \to {coe}_{1} (K) (k) \in {Base}_{R}$
28	18	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
29	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
30	2 13	ringidcl	$⊢ A \in Ring \to O \in B$
31	28 29 30	3syl	$⊢ (N \in Fin \land R \in CRing) \to O \in B$
32	31	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to O \in B$
33	32	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in ℕ_{0}) \to O \in B$
34	25 1 2 14	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land ({coe}_{1} (K) (k) \in {Base}_{R} \land O \in B)) \to {coe}_{1} (K) (k) \underset{˙}{*} O \in B$
35	17 20 27 33 34	syl22anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in ℕ_{0}) \to {coe}_{1} (K) (k) \underset{˙}{*} O \in B$
36	35 16	fmptd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to G : ℕ_{0} ⟶ B$
37	2	fvexi	$⊢ B \in V$
38		nn0ex	$⊢ ℕ_{0} \in V$
39	37 38	pm3.2i	$⊢ (B \in V \land ℕ_{0} \in V)$
40		elmapg	$⊢ (B \in V \land ℕ_{0} \in V) \to (G \in (B^{ℕ_{0}}) \leftrightarrow G : ℕ_{0} ⟶ B)$
41	39 40	mp1i	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (G \in (B^{ℕ_{0}}) \leftrightarrow G : ℕ_{0} ⟶ B)$
42	36 41	mpbird	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to G \in (B^{ℕ_{0}})$

Metamath Proof Explorer

Theorem cpmidpmatlem2

Proof