Metamath Proof Explorer

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 ‘ 𝐴 ) )