Metamath Proof Explorer

Theorem pmatcollpw3fi1lem2

Description: Lemma 2 for pmatcollpw3fi1 . (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p ⊢ P = Poly 1 ⁡ R
pmatcollpw.c ⊢ C = N Mat P
pmatcollpw.b ⊢ B = Base C
pmatcollpw.m ⊢ ∗ ˙ = ⋅ C
pmatcollpw.e ⊢ × ˙ = ⋅ mulGrp P
pmatcollpw.x ⊢ X = var 1 ⁡ R
pmatcollpw.t ⊢ T = N matToPolyMat R
pmatcollpw3.a ⊢ A = N Mat R
pmatcollpw3.d ⊢ D = Base A
Assertion pmatcollpw3fi1lem2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ f ∈ D 0 M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ f ⁡ n → ∃ s ∈ ℕ ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n

Proof

Step Hyp Ref Expression
1 pmatcollpw.p ⊢ P = Poly 1 ⁡ R
2 pmatcollpw.c ⊢ C = N Mat P
3 pmatcollpw.b ⊢ B = Base C
4 pmatcollpw.m ⊢ ∗ ˙ = ⋅ C
5 pmatcollpw.e ⊢ × ˙ = ⋅ mulGrp P
6 pmatcollpw.x ⊢ X = var 1 ⁡ R
7 pmatcollpw.t ⊢ T = N matToPolyMat R
8 pmatcollpw3.a ⊢ A = N Mat R
9 pmatcollpw3.d ⊢ D = Base A
10 fveq1 ⊢ f = g → f ⁡ n = g ⁡ n
11 10 fveq2d ⊢ f = g → T ⁡ f ⁡ n = T ⁡ g ⁡ n
12 11 oveq2d ⊢ f = g → n × ˙ X ∗ ˙ T ⁡ f ⁡ n = n × ˙ X ∗ ˙ T ⁡ g ⁡ n
13 12 mpteq2dv ⊢ f = g → n ∈ 0 ⟼ n × ˙ X ∗ ˙ T ⁡ f ⁡ n = n ∈ 0 ⟼ n × ˙ X ∗ ˙ T ⁡ g ⁡ n
14 13 oveq2d ⊢ f = g → ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ f ⁡ n = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n
15 14 eqeq2d ⊢ f = g → M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n
16 15 cbvrexvw ⊢ ∃ f ∈ D 0 M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ ∃ g ∈ D 0 M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n
17 crngring ⊢ R ∈ CRing → R ∈ Ring
18 17 anim2i ⊢ N ∈ Fin ∧ R ∈ CRing → N ∈ Fin ∧ R ∈ Ring
19 18 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → N ∈ Fin ∧ R ∈ Ring
20 19 ad2antrr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → N ∈ Fin ∧ R ∈ Ring
21 simplr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → g ∈ D 0
22 simpr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n
23 eqid ⊢ 0 A = 0 A
24 eqid ⊢ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A
25 1 2 3 4 5 6 7 8 9 23 24 pmatcollpw3fi1lem1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
26 20 21 22 25 syl3anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
27 1nn ⊢ 1 ∈ ℕ
28 27 a1i ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n ∧ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n → 1 ∈ ℕ
29 oveq2 ⊢ s = 1 → 0 … s = 0 … 1
30 29 oveq2d ⊢ s = 1 → D 0 … s = D 0 … 1
31 29 mpteq1d ⊢ s = 1 → n ∈ 0 … s ⟼ n × ˙ X ∗ ˙ T ⁡ f ⁡ n = n ∈ 0 … 1 ⟼ n × ˙ X ∗ ˙ T ⁡ f ⁡ n
32 31 oveq2d ⊢ s = 1 → ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n
33 32 eqeq2d ⊢ s = 1 → M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n
34 30 33 rexeqbidv ⊢ s = 1 → ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ ∃ f ∈ D 0 … 1 M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n
35 34 adantl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n ∧ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n ∧ s = 1 → ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ ∃ f ∈ D 0 … 1 M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n
36 elmapi ⊢ g ∈ D 0 → g : 0 ⟶ D
37 c0ex ⊢ 0 ∈ V
38 37 snid ⊢ 0 ∈ 0
39 38 a1i ⊢ l ∈ 0 … 1 → 0 ∈ 0
40 ffvelrn ⊢ g : 0 ⟶ D ∧ 0 ∈ 0 → g ⁡ 0 ∈ D
41 39 40 sylan2 ⊢ g : 0 ⟶ D ∧ l ∈ 0 … 1 → g ⁡ 0 ∈ D
42 41 ex ⊢ g : 0 ⟶ D → l ∈ 0 … 1 → g ⁡ 0 ∈ D
43 36 42 syl ⊢ g ∈ D 0 → l ∈ 0 … 1 → g ⁡ 0 ∈ D
44 43 adantl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 → l ∈ 0 … 1 → g ⁡ 0 ∈ D
45 44 imp ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ l ∈ 0 … 1 → g ⁡ 0 ∈ D
46 8 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
47 17 46 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → A ∈ Ring
48 47 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → A ∈ Ring
49 9 23 ring0cl ⊢ A ∈ Ring → 0 A ∈ D
50 48 49 syl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → 0 A ∈ D
51 50 ad2antrr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ l ∈ 0 … 1 → 0 A ∈ D
52 45 51 ifcld ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ l ∈ 0 … 1 → if l = 0 g ⁡ 0 0 A ∈ D
53 52 fmpttd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 → l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A : 0 … 1 ⟶ D
54 9 fvexi ⊢ D ∈ V
55 ovex ⊢ 0 … 1 ∈ V
56 54 55 pm3.2i ⊢ D ∈ V ∧ 0 … 1 ∈ V
57 elmapg ⊢ D ∈ V ∧ 0 … 1 ∈ V → l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ∈ D 0 … 1 ↔ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A : 0 … 1 ⟶ D
58 56 57 mp1i ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 → l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ∈ D 0 … 1 ↔ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A : 0 … 1 ⟶ D
59 53 58 mpbird ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 → l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ∈ D 0 … 1
60 59 adantr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ∈ D 0 … 1
61 fveq1 ⊢ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → f ⁡ n = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
62 61 fveq2d ⊢ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → T ⁡ f ⁡ n = T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
63 62 oveq2d ⊢ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → n × ˙ X ∗ ˙ T ⁡ f ⁡ n = n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
64 63 mpteq2dv ⊢ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → n ∈ 0 … 1 ⟼ n × ˙ X ∗ ˙ T ⁡ f ⁡ n = n ∈ 0 … 1 ⟼ n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
65 64 oveq2d ⊢ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
66 65 eqeq2d ⊢ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
67 66 adantl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n ∧ f = l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A → M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n ↔ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n
68 60 67 rspcedv ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n → ∃ f ∈ D 0 … 1 M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n
69 68 imp ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n ∧ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n → ∃ f ∈ D 0 … 1 M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ f ⁡ n
70 28 35 69 rspcedvd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n ∧ M = ∑ C n = 0 1 n × ˙ X ∗ ˙ T ⁡ l ∈ 0 … 1 ⟼ if l = 0 g ⁡ 0 0 A ⁡ n → ∃ s ∈ ℕ ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n
71 26 70 mpdan ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ g ∈ D 0 ∧ M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → ∃ s ∈ ℕ ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n
72 71 rexlimdva2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ g ∈ D 0 M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ g ⁡ n → ∃ s ∈ ℕ ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n
73 16 72 syl5bi ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ f ∈ D 0 M = ∑ C n ∈ 0 n × ˙ X ∗ ˙ T ⁡ f ⁡ n → ∃ s ∈ ℕ ∃ f ∈ D 0 … s M = ∑ C n = 0 s n × ˙ X ∗ ˙ T ⁡ f ⁡ n