Metamath Proof Explorer

Theorem mptcoe1matfsupp

Description: The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019) (Proof shortened by AV, 23-Dec-2019)

Ref Expression
Hypotheses mptcoe1matfsupp.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mptcoe1matfsupp.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
mptcoe1matfsupp.l ⊢ 𝐿 = ( Base ‘ 𝑄 )
Assertion mptcoe1matfsupp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) ) finSupp ( 0g ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mptcoe1matfsupp.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mptcoe1matfsupp.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3 mptcoe1matfsupp.l ⊢ 𝐿 = ( Base ‘ 𝑄 )
4 fvexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
7 simp2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
8 7 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐼 ∈ 𝑁 )
9 simp3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
10 9 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐽 ∈ 𝑁 )
11 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑂 ∈ 𝐿 )
12 11 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝑂 ∈ 𝐿 )
13 eqid ⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
14 13 3 2 6 coe1fvalcl ⊢ ( ( 𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
15 12 14 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
16 1 5 6 8 10 15 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
17 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
18 13 3 2 17 6 coe1fsupp ⊢ ( 𝑂 ∈ 𝐿 → ( coe1 ‘ 𝑂 ) ∈ { 𝑐 ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∣ 𝑐 finSupp ( 0g ‘ 𝐴 ) } )
19 elrabi ⊢ ( ( coe1 ‘ 𝑂 ) ∈ { 𝑐 ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∣ 𝑐 finSupp ( 0g ‘ 𝐴 ) } → ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) )
20 12 18 19 3syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) )
21 fvex ⊢ ( 0g ‘ 𝐴 ) ∈ V
22 20 21 jctir ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∧ ( 0g ‘ 𝐴 ) ∈ V ) )
23 13 3 2 17 coe1sfi ⊢ ( 𝑂 ∈ 𝐿 → ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) )
24 12 23 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) )
25 fsuppmapnn0ub ⊢ ( ( ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∧ ( 0g ‘ 𝐴 ) ∈ V ) → ( ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
26 22 24 25 sylc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) )
27 csbov ⊢ ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 𝐼 ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 )
28 csbfv ⊢ ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 )
29 28 oveqi ⊢ ( 𝐼 ⦋ 𝑥 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝐽 )
30 27 29 eqtri ⊢ ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝐽 )
31 30 a1i ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝐽 ) )
32 oveq ⊢ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝐽 ) = ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) )
33 32 adantl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝐽 ) = ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) )
34 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
35 1 34 mat0op ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
36 35 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
37 36 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
38 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
39 37 38 7 9 4 ovmpod ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) = ( 0g ‘ 𝑅 ) )
40 39 ad4antr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) = ( 0g ‘ 𝑅 ) )
41 31 33 40 3eqtrd ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 0g ‘ 𝑅 ) )
42 41 exp31 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑠 < 𝑥 → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 0g ‘ 𝑅 ) ) ) )
43 42 a2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 0g ‘ 𝑅 ) ) ) )
44 43 ralimdva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 0g ‘ 𝑅 ) ) ) )
45 44 reximdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 0g ‘ 𝑅 ) ) ) )
46 26 45 mpd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) = ( 0g ‘ 𝑅 ) ) )
47 4 16 46 mptnn0fsupp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) ) finSupp ( 0g ‘ 𝑅 ) )