# 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}\mathrm{Mat}{R}$
chmatcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
chmatcl.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
chmatcl.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
chmatcl.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
chmatcl.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
chmatcl.s
chmatcl.m
chmatcl.1
chmatcl.h
chmatval.s
chmatval.0
Assertion chmatval

### Proof

Step Hyp Ref Expression
1 chmatcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 chmatcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 chmatcl.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
4 chmatcl.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
5 chmatcl.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
6 chmatcl.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
7 chmatcl.s
8 chmatcl.m
9 chmatcl.1
10 chmatcl.h
11 chmatval.s
12 chmatval.0
13 10 oveqi
14 3 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
15 14 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {P}\in \mathrm{Ring}$
16 15 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {P}\in \mathrm{Ring}$
17 14 anim2i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)$
18 17 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)$
19 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
20 5 3 19 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {X}\in {\mathrm{Base}}_{{P}}$
21 20 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {X}\in {\mathrm{Base}}_{{P}}$
22 3 4 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Y}\in \mathrm{Ring}$
23 22 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {Y}\in \mathrm{Ring}$
24 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
25 24 9 ringidcl
26 23 25 syl
27 19 4 24 8 matvscl
28 18 21 26 27 syl12anc
30 6 1 2 3 4 mat2pmatbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {T}\left({M}\right)\in {\mathrm{Base}}_{{Y}}$
31 30 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {T}\left({M}\right)\in {\mathrm{Base}}_{{Y}}$
32 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to \left({I}\in {N}\wedge {J}\in {N}\right)$
33 4 24 7 11 matsubgcell
34 16 29 31 32 33 syl121anc
35 13 34 syl5eq
36 9 a1i
37 36 oveq2d
38 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}\in \mathrm{Fin}$
39 14 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {P}\in \mathrm{Ring}$
40 20 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {X}\in {\mathrm{Base}}_{{P}}$
41 38 39 40 3jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\wedge {X}\in {\mathrm{Base}}_{{P}}\right)$
42 41 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\wedge {X}\in {\mathrm{Base}}_{{P}}\right)$
43 42 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\wedge {X}\in {\mathrm{Base}}_{{P}}\right)$
44 4 19 8 12 matsc
45 43 44 syl
46 37 45 eqtrd
47 eqeq12 ${⊢}\left({i}={I}\wedge {j}={J}\right)\to \left({i}={j}↔{I}={J}\right)$
48 47 ifbid
50 simprl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\in {N}$
51 simpr ${⊢}\left({I}\in {N}\wedge {J}\in {N}\right)\to {J}\in {N}$
52 51 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {J}\in {N}$
53 5 fvexi ${⊢}{X}\in \mathrm{V}$