Theorem cpmidpmatlem2

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

	Ref	Expression
Hypotheses	cpmidgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmidgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmidgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmidgsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmidgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cpmidgsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	cpmidgsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmidgsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmidgsum.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
	cpmidgsum.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cpmidgsum.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
	cpmidgsum.h	⊢ 𝐻 = ( 𝐾 · 1 )
	cpmidgsumm2pm.o	⊢ 𝑂 = ( 1r ‘ 𝐴 )
	cpmidgsumm2pm.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	cpmidgsumm2pm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cpmidpmat.g	⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
Assertion	cpmidpmatlem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ ( 𝐵 ↑m ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmidgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmidgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cpmidgsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		cpmidgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
6		cpmidgsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7		cpmidgsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
8		cpmidgsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
9		cpmidgsum.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
10		cpmidgsum.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
11		cpmidgsum.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
12		cpmidgsum.h	⊢ 𝐻 = ( 𝐾 · 1 )
13		cpmidgsumm2pm.o	⊢ 𝑂 = ( 1r ‘ 𝐴 )
14		cpmidgsumm2pm.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15		cpmidgsumm2pm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
16		cpmidpmat.g	⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
17		simpl1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ Fin )
18		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
19	18	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
20	19	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
21		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
22	10 1 2 3 21	chpmatply1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
23	11 22	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
24		eqid	⊢ ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐾 )
25		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26	24 21 3 25	coe1fvalcl	⊢ ( ( 𝐾 ∈ ( Base ‘ 𝑃 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
27	23 26	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
28	18	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
29	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
30	2 13	ringidcl	⊢ ( 𝐴 ∈ Ring → 𝑂 ∈ 𝐵 )
31	28 29 30	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑂 ∈ 𝐵 )
32	31	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑂 ∈ 𝐵 )
33	32	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑂 ∈ 𝐵 )
34	25 1 2 14	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑂 ∈ 𝐵 ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ∈ 𝐵 )
35	17 20 27 33 34	syl22anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ∈ 𝐵 )
36	35 16	fmptd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐺 : ℕ0 ⟶ 𝐵 )
37	2	fvexi	⊢ 𝐵 ∈ V
38		nn0ex	⊢ ℕ0 ∈ V
39	37 38	pm3.2i	⊢ ( 𝐵 ∈ V ∧ ℕ0 ∈ V )
40		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ℕ0 ∈ V ) → ( 𝐺 ∈ ( 𝐵 ↑m ℕ0 ) ↔ 𝐺 : ℕ0 ⟶ 𝐵 ) )
41	39 40	mp1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 ∈ ( 𝐵 ↑m ℕ0 ) ↔ 𝐺 : ℕ0 ⟶ 𝐵 ) )
42	36 41	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ ( 𝐵 ↑m ℕ0 ) )