Theorem cpmadumatpolylem1

Description: Lemma 1 for cpmadumatpoly . (Contributed by AV, 20-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	cpmadumatpoly.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmadumatpoly.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmadumatpoly.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmadumatpoly.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmadumatpoly.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cpmadumatpoly.r	⊢ × = ( .r ‘ 𝑌 )
	cpmadumatpoly.m0	⊢ − = ( -g ‘ 𝑌 )
	cpmadumatpoly.0	⊢ 0 = ( 0g ‘ 𝑌 )
	cpmadumatpoly.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
	cpmadumatpoly.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	cpmadumatpoly.m1	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmadumatpoly.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmadumatpoly.z	⊢ 𝑍 = ( var1 ‘ 𝑅 )
	cpmadumatpoly.d	⊢ 𝐷 = ( ( 𝑍 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
	cpmadumatpoly.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
	cpmadumatpoly.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
	cpmadumatpoly.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	cpmadumatpoly.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	cpmadumatpoly.m2	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	cpmadumatpoly.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	cpmadumatpoly.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
Assertion	cpmadumatpolylem1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		cpmadumatpoly.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmadumatpoly.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmadumatpoly.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cpmadumatpoly.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		cpmadumatpoly.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6		cpmadumatpoly.r	⊢ × = ( .r ‘ 𝑌 )
7		cpmadumatpoly.m0	⊢ − = ( -g ‘ 𝑌 )
8		cpmadumatpoly.0	⊢ 0 = ( 0g ‘ 𝑌 )
9		cpmadumatpoly.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10		cpmadumatpoly.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
11		cpmadumatpoly.m1	⊢ · = ( ·𝑠 ‘ 𝑌 )
12		cpmadumatpoly.1	⊢ 1 = ( 1r ‘ 𝑌 )
13		cpmadumatpoly.z	⊢ 𝑍 = ( var1 ‘ 𝑅 )
14		cpmadumatpoly.d	⊢ 𝐷 = ( ( 𝑍 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
15		cpmadumatpoly.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
16		cpmadumatpoly.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
17		cpmadumatpoly.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
18		cpmadumatpoly.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
19		cpmadumatpoly.m2	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
20		cpmadumatpoly.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
21		cpmadumatpoly.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
22		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
23		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
24	23	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
25	22 24	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
26	25	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
27	1 2 10 21	cpm2mf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑈 : 𝑆 ⟶ 𝐵 )
28	26 27	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑈 : 𝑆 ⟶ 𝐵 )
29	1 2 3 4 6 7 8 5 9 10	chfacfisfcpmat	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )
30	23 29	syl3anl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )
31	30	anassrs	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )
32		fco	⊢ ( ( 𝑈 : 𝑆 ⟶ 𝐵 ∧ 𝐺 : ℕ0 ⟶ 𝑆 ) → ( 𝑈 ∘ 𝐺 ) : ℕ0 ⟶ 𝐵 )
33	28 31 32	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) : ℕ0 ⟶ 𝐵 )
34	2	fvexi	⊢ 𝐵 ∈ V
35		nn0ex	⊢ ℕ0 ∈ V
36	34 35	pm3.2i	⊢ ( 𝐵 ∈ V ∧ ℕ0 ∈ V )
37		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ℕ0 ∈ V ) → ( ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑈 ∘ 𝐺 ) : ℕ0 ⟶ 𝐵 ) )
38	36 37	mp1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑈 ∘ 𝐺 ) : ℕ0 ⟶ 𝐵 ) )
39	33 38	mpbird	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) )