Metamath Proof Explorer

Theorem cpmidpmatlem3

Description: Lemma 3 for cpmidpmat . (Contributed by AV, 14-Nov-2019) (Proof shortened by AV, 7-Dec-2019)

Ref Expression
Hypotheses cpmidgsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cpmidgsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cpmidgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmidgsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cpmidgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
cpmidgsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
cpmidgsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
cpmidgsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
cpmidgsum.u ⊢ 𝑈 = ( algSc ‘ 𝑃 )
cpmidgsum.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
cpmidgsum.k ⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
cpmidgsum.h ⊢ 𝐻 = ( 𝐾 · 1 )
cpmidgsumm2pm.o ⊢ 𝑂 = ( 1r ‘ 𝐴 )
cpmidgsumm2pm.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
cpmidgsumm2pm.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cpmidpmat.g ⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
Assertion cpmidpmatlem3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐺 finSupp ( 0g ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cpmidgsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpmidgsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cpmidgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cpmidgsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cpmidgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 cpmidgsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7 cpmidgsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
8 cpmidgsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
9 cpmidgsum.u ⊢ 𝑈 = ( algSc ‘ 𝑃 )
10 cpmidgsum.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
11 cpmidgsum.k ⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
12 cpmidgsum.h ⊢ 𝐻 = ( 𝐾 · 1 )
13 cpmidgsumm2pm.o ⊢ 𝑂 = ( 1r ‘ 𝐴 )
14 cpmidgsumm2pm.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15 cpmidgsumm2pm.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
16 cpmidpmat.g ⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) )
17 fvexd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ 𝐴 ) ∈ V )
18 ovexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ∈ V )
19 fveq2 ⊢ ( 𝑘 = 𝑙 → ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) )
20 19 oveq1d ⊢ ( 𝑘 = 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) )
21 fvexd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ 𝑅 ) ∈ V )
22 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
23 10 1 2 3 22 chpmatply1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
24 11 23 eqeltrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
25 eqid ⊢ ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐾 )
26 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 25 22 3 26 coe1fvalcl ⊢ ( ( 𝐾 ∈ ( Base ‘ 𝑃 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
28 24 27 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
29 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
30 29 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
31 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
32 3 22 31 mptcoe1fsupp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) finSupp ( 0g ‘ 𝑅 ) )
33 30 24 32 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) finSupp ( 0g ‘ 𝑅 ) )
34 21 28 33 mptnn0fsuppr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑙 ∈ ℕ0 ( 𝑠 < 𝑙 → ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
35 csbfv ⊢ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 )
36 35 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) → ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) )
37 36 eqeq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) → ( ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) )
38 37 biimpa ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) )
39 1 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
40 39 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
41 40 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
42 41 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
43 38 42 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
44 43 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∗ 𝑂 ) )
45 1 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
46 29 45 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ LMod )
47 46 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ LMod )
48 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
49 29 48 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
50 2 13 ringidcl ⊢ ( 𝐴 ∈ Ring → 𝑂 ∈ 𝐵 )
51 49 50 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑂 ∈ 𝐵 )
52 51 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑂 ∈ 𝐵 )
53 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
54 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) )
55 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
56 2 53 14 54 55 lmod0vs ⊢ ( ( 𝐴 ∈ LMod ∧ 𝑂 ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) )
57 47 52 56 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) )
58 57 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) )
59 44 58 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) ∧ ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) )
60 59 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) → ( ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) ) )
61 60 imim2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑠 < 𝑙 → ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑠 < 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) ) ) )
62 61 ralimdva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑙 ∈ ℕ0 ( 𝑠 < 𝑙 → ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑙 ∈ ℕ0 ( 𝑠 < 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) ) ) )
63 62 reximdv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑙 ∈ ℕ0 ( 𝑠 < 𝑙 → ⦋ 𝑙 / 𝑛 ⦌ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑙 ∈ ℕ0 ( 𝑠 < 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) ) ) )
64 34 63 mpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑙 ∈ ℕ0 ( 𝑠 < 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 𝑂 ) = ( 0g ‘ 𝐴 ) ) )
65 17 18 20 64 mptnn0fsuppd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑘 ) ∗ 𝑂 ) ) finSupp ( 0g ‘ 𝐴 ) )
66 16 65 eqbrtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐺 finSupp ( 0g ‘ 𝐴 ) )