Metamath Proof Explorer

Theorem cpmadugsum

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite sum. (Contributed by AV, 10-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a ⊢ A = N Mat R
cpmadugsum.b ⊢ B = Base A
cpmadugsum.p ⊢ P = Poly 1 ⁡ R
cpmadugsum.y ⊢ Y = N Mat P
cpmadugsum.t ⊢ T = N matToPolyMat R
cpmadugsum.x ⊢ X = var 1 ⁡ R
cpmadugsum.e ⊢ × ˙ = ⋅ mulGrp P
cpmadugsum.m ⊢ · ˙ = ⋅ Y
cpmadugsum.r ⊢ × ˙ = ⋅ Y
cpmadugsum.1 ⊢ 1 ˙ = 1 Y
cpmadugsum.g ⊢ + ˙ = + Y
cpmadugsum.s ⊢ - ˙ = - Y
cpmadugsum.i ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M
cpmadugsum.j ⊢ J = N maAdju P
cpmadugsum.0 ⊢ 0 ˙ = 0 Y
cpmadugsum.g2 ⊢ G = n ∈ ℕ 0 ⟼ if n = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if n = s + 1 T ⁡ b ⁡ s if s + 1 < n 0 ˙ T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n
Assertion cpmadugsum ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i

Proof

Step Hyp Ref Expression
1 cpmadugsum.a ⊢ A = N Mat R
2 cpmadugsum.b ⊢ B = Base A
3 cpmadugsum.p ⊢ P = Poly 1 ⁡ R
4 cpmadugsum.y ⊢ Y = N Mat P
5 cpmadugsum.t ⊢ T = N matToPolyMat R
6 cpmadugsum.x ⊢ X = var 1 ⁡ R
7 cpmadugsum.e ⊢ × ˙ = ⋅ mulGrp P
8 cpmadugsum.m ⊢ · ˙ = ⋅ Y
9 cpmadugsum.r ⊢ × ˙ = ⋅ Y
10 cpmadugsum.1 ⊢ 1 ˙ = 1 Y
11 cpmadugsum.g ⊢ + ˙ = + Y
12 cpmadugsum.s ⊢ - ˙ = - Y
13 cpmadugsum.i ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M
14 cpmadugsum.j ⊢ J = N maAdju P
15 cpmadugsum.0 ⊢ 0 ˙ = 0 Y
16 cpmadugsum.g2 ⊢ G = n ∈ ℕ 0 ⟼ if n = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if n = s + 1 T ⁡ b ⁡ s if s + 1 < n 0 ˙ T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cpmadugsumfi ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0
18 simpr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 → I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0
19 1 2 3 4 9 12 15 5 16 6 8 7 11 chfacfscmulgsum ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0
20 19 eqcomd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
21 20 adantr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 → ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
22 18 21 eqtrd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 → I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
23 22 ex ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 → I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
24 23 reximdvva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i = 1 s i × ˙ X · ˙ T ⁡ b ⁡ i − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ i + ˙ s + 1 × ˙ X · ˙ T ⁡ b ⁡ s - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
25 17 24 mpd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i