# Metamath Proof Explorer

Description: First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
madufval.d ${⊢}{D}={N}\mathrm{maDet}{R}$
madufval.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
madufval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$

### Proof

Step Hyp Ref Expression
1 madufval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 madufval.d ${⊢}{D}={N}\mathrm{maDet}{R}$
3 madufval.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
4 madufval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
7 fvoveq1 ${⊢}{n}={N}\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{r}\right)}$
8 id ${⊢}{n}={N}\to {n}={N}$
9 oveq1 ${⊢}{n}={N}\to {n}\mathrm{maDet}{r}={N}\mathrm{maDet}{r}$
10 eqidd ${⊢}{n}={N}\to if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)=if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)$
11 8 8 10 mpoeq123dv ${⊢}{n}={N}\to \left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)=\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)$
12 9 11 fveq12d ${⊢}{n}={N}\to \left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)=\left({N}\mathrm{maDet}{r}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)$
13 8 8 12 mpoeq123dv ${⊢}{n}={N}\to \left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)=\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{r}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)$
14 7 13 mpteq12dv ${⊢}{n}={N}\to \left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)=\left({m}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{r}\right)}⟼\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{r}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)$
15 oveq2 ${⊢}{r}={R}\to {N}\mathrm{Mat}{r}={N}\mathrm{Mat}{R}$
16 15 fveq2d ${⊢}{r}={R}\to {\mathrm{Base}}_{\left({N}\mathrm{Mat}{r}\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}$
17 oveq2 ${⊢}{r}={R}\to {N}\mathrm{maDet}{r}={N}\mathrm{maDet}{R}$
18 fveq2 ${⊢}{r}={R}\to {1}_{{r}}={1}_{{R}}$
19 fveq2 ${⊢}{r}={R}\to {0}_{{r}}={0}_{{R}}$
20 18 19 ifeq12d ${⊢}{r}={R}\to if\left({l}={i},{1}_{{r}},{0}_{{r}}\right)=if\left({l}={i},{1}_{{R}},{0}_{{R}}\right)$
21 20 ifeq1d ${⊢}{r}={R}\to if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)=if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)$
22 21 mpoeq3dv ${⊢}{r}={R}\to \left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)=\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\right)$
23 17 22 fveq12d ${⊢}{r}={R}\to \left({N}\mathrm{maDet}{r}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)=\left({N}\mathrm{maDet}{R}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\right)\right)$
24 23 mpoeq3dv ${⊢}{r}={R}\to \left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{r}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)=\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{R}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\right)\right)\right)$
25 16 24 mpteq12dv ${⊢}{r}={R}\to \left({m}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{r}\right)}⟼\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{r}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)=\left({m}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}⟼\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{R}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\right)\right)\right)\right)$
26 df-madu ${⊢}\mathrm{maAdju}=\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)\right)$
27 fvex ${⊢}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}\in \mathrm{V}$
28 27 mptex ${⊢}\left({m}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}⟼\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{R}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\right)\right)\right)\right)\in \mathrm{V}$
29 14 25 26 28 ovmpo ${⊢}\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {N}\mathrm{maAdju}{R}=\left({m}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}⟼\left({i}\in {N},{j}\in {N}⟼\left({N}\mathrm{maDet}{R}\right)\left(\left({k}\in {N},{l}\in {N}⟼if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\right)\right)\right)\right)$
30 1 fveq2i ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}$
31 4 30 eqtri ${⊢}{B}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}$
32 5 a1i
33 6 a1i
34 32 33 ifeq12d
35 34 ifeq1d
36 35 mpoeq3ia
37 2 36 fveq12i
38 37 a1i
39 38 mpoeq3ia
40 31 39 mpteq12i
41 29 40 syl6eqr
42 26 reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{maAdju}$
43 42 ovprc ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {N}\mathrm{maAdju}{R}=\varnothing$
44 df-mat ${⊢}\mathrm{Mat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({r}\mathrm{freeLMod}\left({n}×{n}\right)\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{r}\mathrm{maMul}⟨{n},{n},{n}⟩⟩\right)$
45 44 reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{Mat}$
46 45 ovprc ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {N}\mathrm{Mat}{R}=\varnothing$
47 1 46 syl5eq ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {A}=\varnothing$
48 47 fveq2d ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{A}}={\mathrm{Base}}_{\varnothing }$
49 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
50 48 4 49 3eqtr4g ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}=\varnothing$
51 50 mpteq1d
52 mpt0
53 51 52 syl6eq
54 43 53 eqtr4d
55 41 54 pm2.61i
56 3 55 eqtri