Metamath Proof Explorer

Theorem pm2mpmhmlem1

Description: Lemma 1 for pm2mpmhm . (Contributed by AV, 21-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pm2mpfo.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpfo.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pm2mpfo.m ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
pm2mpfo.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
pm2mpfo.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
pm2mpfo.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpfo.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
pm2mpfo.l ⊢ 𝐿 = ( Base ‘ 𝑄 )
pm2mpfo.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion pm2mpmhmlem1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑙 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ∗ ( 𝑙 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 pm2mpfo.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pm2mpfo.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pm2mpfo.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pm2mpfo.m ⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5 pm2mpfo.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6 pm2mpfo.x ⊢ 𝑋 = ( var1 ‘ 𝐴 )
7 pm2mpfo.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8 pm2mpfo.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9 pm2mpfo.l ⊢ 𝐿 = ( Base ‘ 𝑄 )
10 pm2mpfo.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
11 fvexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 0g ‘ 𝑄 ) ∈ V )
12 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ∗ ( 𝑙 ↑ 𝑋 ) ) ∈ V )
13 oveq2 ⊢ ( 𝑙 = 𝑛 → ( 0 ... 𝑙 ) = ( 0 ... 𝑛 ) )
14 oveq1 ⊢ ( 𝑙 = 𝑛 → ( 𝑙 − 𝑘 ) = ( 𝑛 − 𝑘 ) )
15 14 oveq2d ⊢ ( 𝑙 = 𝑛 → ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) = ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) )
16 15 oveq2d ⊢ ( 𝑙 = 𝑛 → ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) = ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) )
17 13 16 mpteq12dv ⊢ ( 𝑙 = 𝑛 → ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) )
18 17 oveq2d ⊢ ( 𝑙 = 𝑛 → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
19 oveq1 ⊢ ( 𝑙 = 𝑛 → ( 𝑙 ↑ 𝑋 ) = ( 𝑛 ↑ 𝑋 ) )
20 18 19 oveq12d ⊢ ( 𝑙 = 𝑛 → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ∗ ( 𝑙 ↑ 𝑋 ) ) = ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
21 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
22 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
23 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
24 23 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
25 3anass ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝐶 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
26 24 25 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
27 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
28 3 27 ringcl ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 )
29 26 28 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 )
30 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
31 1 2 3 30 pmatcoe1fsupp ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
32 21 22 29 31 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
33 fvoveq1 ⊢ ( 𝑎 = 𝑖 → ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) = ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) )
34 33 fveq1d ⊢ ( 𝑎 = 𝑖 → ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) )
35 34 eqeq1d ⊢ ( 𝑎 = 𝑖 → ( ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
36 oveq2 ⊢ ( 𝑏 = 𝑗 → ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) = ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) )
37 36 fveq2d ⊢ ( 𝑏 = 𝑗 → ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) = ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) )
38 37 fveq1d ⊢ ( 𝑏 = 𝑗 → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) )
39 38 eqeq1d ⊢ ( 𝑏 = 𝑗 → ( ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
40 35 39 rspc2va ⊢ ( ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) )
41 40 expcom ⊢ ( ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
42 41 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
43 42 3impib ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) )
44 43 mpoeq3dva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
45 7 30 mat0op ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
46 45 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
47 7 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
48 8 ply1sca ⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
49 47 48 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
50 49 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
51 50 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
52 44 46 51 3eqtr2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
53 52 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
54 8 ply1lmod ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
55 47 54 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
56 55 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑄 ∈ LMod )
57 47 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐴 ∈ Ring )
58 eqid ⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
59 8 6 58 5 9 ply1moncl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ 𝐿 )
60 57 59 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ 𝐿 )
61 eqid ⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
62 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) )
63 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
64 9 61 4 62 63 lmod0vs ⊢ ( ( 𝑄 ∈ LMod ∧ ( 𝑛 ↑ 𝑋 ) ∈ 𝐿 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
65 56 60 64 syl2an2r ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
66 65 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
67 53 66 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
68 67 ex ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) )
69 68 imim2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
70 69 ralimdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
71 70 reximdv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
72 32 71 mpd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) )
73 2 3 decpmatval ⊢ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) )
74 29 73 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) )
75 74 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
76 75 eqeq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ↔ ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) )
77 76 imbi2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ↔ ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
78 77 ralbidva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
79 78 rexbidv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
80 72 79 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) )
81 1 2 3 7 decpmatmul ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
82 81 ad4ant234 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
83 82 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) )
84 83 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
85 84 eqeq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ↔ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) )
86 85 imbi2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ↔ ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
87 86 ralbidva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
88 87 rexbidv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) ) )
89 80 88 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) ∗ ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) ) )
90 11 12 20 89 mptnn0fsuppd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑙 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ∗ ( 𝑙 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )