Theorem cpmadumatpolylem2

Description: Lemma 2 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	cpmadumatpolylem2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) finSupp ( 0g ‘ 𝐴 ) )

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		fvexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 0g ‘ 𝐴 ) ∈ V )
23		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
24	23	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
25	24	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
26	25	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
27	10 3 4	0elcpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝑌 ) ∈ 𝑆 )
28	26 27	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 0g ‘ 𝑌 ) ∈ 𝑆 )
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	1 2 10 21	cpm2mf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑈 : 𝑆 ⟶ 𝐵 )
33	26 32	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑈 : 𝑆 ⟶ 𝐵 )
34		ssidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑆 ⊆ 𝑆 )
35		nn0ex	⊢ ℕ0 ∈ V
36	35	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ℕ0 ∈ V )
37	10	ovexi	⊢ 𝑆 ∈ V
38	37	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑆 ∈ V )
39	1 2 3 4 6 7 8 5 9	chfacffsupp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 finSupp ( 0g ‘ 𝑌 ) )
40	39	anassrs	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝐺 finSupp ( 0g ‘ 𝑌 ) )
41		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
42		eqid	⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
43	1 21 3 4 41 42	m2cpminv0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑈 ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ 𝐴 ) )
44	23 43	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑈 ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ 𝐴 ) )
45	44	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ 𝐴 ) )
46	45	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ 𝐴 ) )
47	22 28 31 33 34 36 38 40 46	fsuppcor	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) finSupp ( 0g ‘ 𝐴 ) )