# Metamath Proof Explorer

## Theorem maduf

Description: Creating the adjunct of matrices is a function from the set of matrices into the set of matrices. (Contributed by Stefan O'Rear, 11-Jul-2018)

Ref Expression
Hypotheses maduf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
maduf.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
maduf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion maduf ${⊢}{R}\in \mathrm{CRing}\to {J}:{B}⟶{B}$

### Proof

Step Hyp Ref Expression
1 maduf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 maduf.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
3 maduf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
5 1 3 matrcl ${⊢}{m}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
6 5 adantl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
7 6 simpld ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to {N}\in \mathrm{Fin}$
8 simpl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to {R}\in \mathrm{CRing}$
9 eqid ${⊢}{N}\mathrm{maDet}{R}={N}\mathrm{maDet}{R}$
10 9 1 3 4 mdetf ${⊢}{R}\in \mathrm{CRing}\to \left({N}\mathrm{maDet}{R}\right):{B}⟶{\mathrm{Base}}_{{R}}$
11 10 adantr ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \left({N}\mathrm{maDet}{R}\right):{B}⟶{\mathrm{Base}}_{{R}}$
12 11 3ad2ant1 ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({N}\mathrm{maDet}{R}\right):{B}⟶{\mathrm{Base}}_{{R}}$
13 7 3ad2ant1 ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {N}\in \mathrm{Fin}$
14 simp1l ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{CRing}$
15 simp11l ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {R}\in \mathrm{CRing}$
16 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
17 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
18 4 17 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {\mathrm{Base}}_{{R}}$
19 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
20 4 19 ring0cl ${⊢}{R}\in \mathrm{Ring}\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
21 18 20 ifcld ${⊢}{R}\in \mathrm{Ring}\to if\left({l}={i},{1}_{{R}},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
22 15 16 21 3syl ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to if\left({l}={i},{1}_{{R}},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
23 simp2 ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {k}\in {N}$
24 simp3 ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {l}\in {N}$
25 simp11r ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {m}\in {B}$
26 1 4 3 23 24 25 matecld ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {k}{m}{l}\in {\mathrm{Base}}_{{R}}$
27 22 26 ifcld ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to if\left({k}={j},if\left({l}={i},{1}_{{R}},{0}_{{R}}\right),{k}{m}{l}\right)\in {\mathrm{Base}}_{{R}}$
28 1 4 3 13 14 27 matbas2d ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\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)\in {B}$
29 12 28 ffvelrnd ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\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)\in {\mathrm{Base}}_{{R}}$
30 1 4 3 7 8 29 matbas2d ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\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)\in {B}$
31 1 9 2 3 17 19 madufval ${⊢}{J}=\left({m}\in {B}⟼\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)$
32 30 31 fmptd ${⊢}{R}\in \mathrm{CRing}\to {J}:{B}⟶{B}$