Metamath Proof Explorer

Theorem decpmataa0

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is 0 for almost all powers. (Contributed by AV, 3-Nov-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmate.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
decpmate.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
decpmate.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
decpmatcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
decpmatfsupp.0 ⊢ 0 = ( 0g ‘ 𝐴 )
Assertion decpmataa0 ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝑀 decompPMat 𝑥 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 decpmate.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 decpmate.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 decpmate.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 decpmatcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
5 decpmatfsupp.0 ⊢ 0 = ( 0g ‘ 𝐴 )
6 2 3 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ V ) )
7 6 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
8 7 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
9 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
10 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
11 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
12 1 2 3 11 pmatcoe1fsupp ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
13 8 9 10 12 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
14 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
15 1 2 3 4 14 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑥 ) ∈ ( Base ‘ 𝐴 ) )
16 15 3expa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑥 ) ∈ ( Base ‘ 𝐴 ) )
17 8 9 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
18 4 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
19 14 5 ring0cl ⊢ ( 𝐴 ∈ Ring → 0 ∈ ( Base ‘ 𝐴 ) )
20 17 18 19 3syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 0 ∈ ( Base ‘ 𝐴 ) )
21 20 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 0 ∈ ( Base ‘ 𝐴 ) )
22 4 14 eqmat ⊢ ( ( ( 𝑀 decompPMat 𝑥 ) ∈ ( Base ‘ 𝐴 ) ∧ 0 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑀 decompPMat 𝑥 ) = 0 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( 𝑖 0 𝑗 ) ) )
23 16 21 22 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝑥 ) = 0 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( 𝑖 0 𝑗 ) ) )
24 df-3an ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) )
25 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) )
26 24 25 sylanbr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) )
27 17 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
28 27 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
29 4 11 mat0op ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
30 5 29 eqtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
31 28 30 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 0 = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
32 eqidd ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑎 = 𝑖 ∧ 𝑏 = 𝑗 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
33 simpl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
34 33 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
35 simpr ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
36 35 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
37 fvexd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
38 31 32 34 36 37 ovmpod ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 0 𝑗 ) = ( 0g ‘ 𝑅 ) )
39 26 38 eqeq12d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( 𝑖 0 𝑗 ) ↔ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
40 39 2ralbidva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( 𝑖 0 𝑗 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
41 23 40 bitrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝑥 ) = 0 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
42 41 imbi2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( 𝑀 decompPMat 𝑥 ) = 0 ) ↔ ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
43 42 ralbidva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝑀 decompPMat 𝑥 ) = 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
44 43 rexbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝑀 decompPMat 𝑥 ) = 0 ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
45 13 44 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( 𝑀 decompPMat 𝑥 ) = 0 ) )