Metamath Proof Explorer


Theorem chmatval

Description: The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019) (Proof shortened by AV, 10-Dec-2019)

Ref Expression
Hypotheses chmatcl.a A = N Mat R
chmatcl.b B = Base A
chmatcl.p P = Poly 1 R
chmatcl.y Y = N Mat P
chmatcl.x X = var 1 R
chmatcl.t T = N matToPolyMat R
chmatcl.s - ˙ = - Y
chmatcl.m · ˙ = Y
chmatcl.1 1 ˙ = 1 Y
chmatcl.h H = X · ˙ 1 ˙ - ˙ T M
chmatval.s ˙ = - P
chmatval.0 0 ˙ = 0 P
Assertion chmatval N Fin R Ring M B I N J N I H J = if I = J X ˙ I T M J 0 ˙ ˙ I T M J

Proof

Step Hyp Ref Expression
1 chmatcl.a A = N Mat R
2 chmatcl.b B = Base A
3 chmatcl.p P = Poly 1 R
4 chmatcl.y Y = N Mat P
5 chmatcl.x X = var 1 R
6 chmatcl.t T = N matToPolyMat R
7 chmatcl.s - ˙ = - Y
8 chmatcl.m · ˙ = Y
9 chmatcl.1 1 ˙ = 1 Y
10 chmatcl.h H = X · ˙ 1 ˙ - ˙ T M
11 chmatval.s ˙ = - P
12 chmatval.0 0 ˙ = 0 P
13 10 oveqi I H J = I X · ˙ 1 ˙ - ˙ T M J
14 3 ply1ring R Ring P Ring
15 14 3ad2ant2 N Fin R Ring M B P Ring
16 15 adantr N Fin R Ring M B I N J N P Ring
17 14 anim2i N Fin R Ring N Fin P Ring
18 17 3adant3 N Fin R Ring M B N Fin P Ring
19 eqid Base P = Base P
20 5 3 19 vr1cl R Ring X Base P
21 20 3ad2ant2 N Fin R Ring M B X Base P
22 3 4 pmatring N Fin R Ring Y Ring
23 22 3adant3 N Fin R Ring M B Y Ring
24 eqid Base Y = Base Y
25 24 9 ringidcl Y Ring 1 ˙ Base Y
26 23 25 syl N Fin R Ring M B 1 ˙ Base Y
27 19 4 24 8 matvscl N Fin P Ring X Base P 1 ˙ Base Y X · ˙ 1 ˙ Base Y
28 18 21 26 27 syl12anc N Fin R Ring M B X · ˙ 1 ˙ Base Y
29 28 adantr N Fin R Ring M B I N J N X · ˙ 1 ˙ Base Y
30 6 1 2 3 4 mat2pmatbas N Fin R Ring M B T M Base Y
31 30 adantr N Fin R Ring M B I N J N T M Base Y
32 simpr N Fin R Ring M B I N J N I N J N
33 4 24 7 11 matsubgcell P Ring X · ˙ 1 ˙ Base Y T M Base Y I N J N I X · ˙ 1 ˙ - ˙ T M J = I X · ˙ 1 ˙ J ˙ I T M J
34 16 29 31 32 33 syl121anc N Fin R Ring M B I N J N I X · ˙ 1 ˙ - ˙ T M J = I X · ˙ 1 ˙ J ˙ I T M J
35 13 34 syl5eq N Fin R Ring M B I N J N I H J = I X · ˙ 1 ˙ J ˙ I T M J
36 9 a1i N Fin R Ring M B I N J N 1 ˙ = 1 Y
37 36 oveq2d N Fin R Ring M B I N J N X · ˙ 1 ˙ = X · ˙ 1 Y
38 simpl N Fin R Ring N Fin
39 14 adantl N Fin R Ring P Ring
40 20 adantl N Fin R Ring X Base P
41 38 39 40 3jca N Fin R Ring N Fin P Ring X Base P
42 41 3adant3 N Fin R Ring M B N Fin P Ring X Base P
43 42 adantr N Fin R Ring M B I N J N N Fin P Ring X Base P
44 4 19 8 12 matsc N Fin P Ring X Base P X · ˙ 1 Y = i N , j N if i = j X 0 ˙
45 43 44 syl N Fin R Ring M B I N J N X · ˙ 1 Y = i N , j N if i = j X 0 ˙
46 37 45 eqtrd N Fin R Ring M B I N J N X · ˙ 1 ˙ = i N , j N if i = j X 0 ˙
47 eqeq12 i = I j = J i = j I = J
48 47 ifbid i = I j = J if i = j X 0 ˙ = if I = J X 0 ˙
49 48 adantl N Fin R Ring M B I N J N i = I j = J if i = j X 0 ˙ = if I = J X 0 ˙
50 simprl N Fin R Ring M B I N J N I N
51 simpr I N J N J N
52 51 adantl N Fin R Ring M B I N J N J N
53 5 fvexi X V
54 12 fvexi 0 ˙ V
55 53 54 ifex if I = J X 0 ˙ V
56 55 a1i N Fin R Ring M B I N J N if I = J X 0 ˙ V
57 46 49 50 52 56 ovmpod N Fin R Ring M B I N J N I X · ˙ 1 ˙ J = if I = J X 0 ˙
58 57 oveq1d N Fin R Ring M B I N J N I X · ˙ 1 ˙ J ˙ I T M J = if I = J X 0 ˙ ˙ I T M J
59 ovif if I = J X 0 ˙ ˙ I T M J = if I = J X ˙ I T M J 0 ˙ ˙ I T M J
60 58 59 syl6eq N Fin R Ring M B I N J N I X · ˙ 1 ˙ J ˙ I T M J = if I = J X ˙ I T M J 0 ˙ ˙ I T M J
61 35 60 eqtrd N Fin R Ring M B I N J N I H J = if I = J X ˙ I T M J 0 ˙ ˙ I T M J