# Metamath Proof Explorer

Description: The determinant of a submatrix of a square matrix obtained by removing a row and a column at the same index equals the determinant of the original matrix with the row replaced with 0's and a 1 at the diagonal position. (Contributed by AV, 31-Jan-2019) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses smadiadet.a ${⊢}{A}={N}\mathrm{Mat}{R}$
smadiadet.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
smadiadet.r ${⊢}{R}\in \mathrm{CRing}$
smadiadet.d ${⊢}{D}={N}\mathrm{maDet}{R}$
smadiadet.h ${⊢}{E}=\left({N}\setminus \left\{{K}\right\}\right)\mathrm{maDet}{R}$
Assertion smadiadet ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {E}\left({K}\left({N}\mathrm{subMat}{R}\right)\left({M}\right){K}\right)={D}\left({K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){K}\right)$

### Proof

Step Hyp Ref Expression
1 smadiadet.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 smadiadet.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 smadiadet.r ${⊢}{R}\in \mathrm{CRing}$
4 smadiadet.d ${⊢}{D}={N}\mathrm{maDet}{R}$
5 smadiadet.h ${⊢}{E}=\left({N}\setminus \left\{{K}\right\}\right)\mathrm{maDet}{R}$
6 eqid ${⊢}{N}\mathrm{subMat}{R}={N}\mathrm{subMat}{R}$
7 1 6 2 submaval ${⊢}\left({M}\in {B}\wedge {K}\in {N}\wedge {K}\in {N}\right)\to {K}\left({N}\mathrm{subMat}{R}\right)\left({M}\right){K}=\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)$
8 7 3anidm23 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {K}\left({N}\mathrm{subMat}{R}\right)\left({M}\right){K}=\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)$
9 8 fveq2d ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {E}\left({K}\left({N}\mathrm{subMat}{R}\right)\left({M}\right){K}\right)={E}\left(\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\right)$
10 eqid ${⊢}{N}\mathrm{minMatR1}{R}={N}\mathrm{minMatR1}{R}$
11 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
12 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
13 1 2 10 11 12 minmar1val ${⊢}\left({M}\in {B}\wedge {K}\in {N}\wedge {K}\in {N}\right)\to {K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){K}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)$
14 13 3anidm23 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){K}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)$
15 14 fveq2d ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {D}\left({K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){K}\right)={D}\left(\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\right)$
16 1 2 3 12 11 marep01ma ${⊢}{M}\in {B}\to \left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\in {B}$
17 eqid ${⊢}{\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
18 eqid ${⊢}\mathrm{ℤRHom}\left({R}\right)=\mathrm{ℤRHom}\left({R}\right)$
19 eqid ${⊢}\mathrm{pmSgn}\left({N}\right)=\mathrm{pmSgn}\left({N}\right)$
20 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
21 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
22 4 1 2 17 18 19 20 21 mdetleib2 ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\in {B}\right)\to {D}\left(\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)$
23 3 16 22 sylancr ${⊢}{M}\in {B}\to {D}\left(\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)$
24 23 adantr ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {D}\left(\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)$
25 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
26 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
27 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
28 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
29 3 27 28 mp2b ${⊢}{R}\in \mathrm{CMnd}$
30 29 a1i ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {R}\in \mathrm{CMnd}$
31 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
32 31 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
33 eqid ${⊢}\mathrm{SymGrp}\left({N}\right)=\mathrm{SymGrp}\left({N}\right)$
34 33 17 symgbasfi ${⊢}{N}\in \mathrm{Fin}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\in \mathrm{Fin}$
35 32 34 syl ${⊢}{M}\in {B}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\in \mathrm{Fin}$
36 35 adantr ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\in \mathrm{Fin}$
37 1 2 3 12 11 17 21 18 19 20 smadiadetlem1 ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\in {\mathrm{Base}}_{{R}}$
38 disjdif ${⊢}\left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\cap \left({\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\right)=\varnothing$
39 38 a1i ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\cap \left({\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\right)=\varnothing$
40 ssrab2 ${⊢}\left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\subseteq {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
41 40 a1i ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\subseteq {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
42 undif ${⊢}\left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\subseteq {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}↔\left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\cup \left({\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\right)={\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
43 41 42 sylib ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\cup \left({\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\right)={\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
44 43 eqcomd ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}=\left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\cup \left({\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}\right)$
45 25 26 30 36 37 39 44 gsummptfidmsplit ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)=\left(\underset{{p}\in \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)\right){+}_{{R}}\left(\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)\right)$
46 eqid ${⊢}{\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}$
47 eqid ${⊢}\mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)=\mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)$
48 1 2 3 12 11 17 21 18 19 20 46 47 smadiadetlem4 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \underset{{p}\in \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)$
49 1 2 3 12 11 17 21 18 19 20 smadiadetlem2 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)={0}_{{R}}$
50 48 49 oveq12d ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left(\underset{{p}\in \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)\right){+}_{{R}}\left(\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\setminus \left\{{q}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}|{q}\left({K}\right)={K}\right\}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)\right)=\left(\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)\right){+}_{{R}}{0}_{{R}}$
51 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
52 3 27 51 mp2b ${⊢}{R}\in \mathrm{Mnd}$
53 diffi ${⊢}{N}\in \mathrm{Fin}\to {N}\setminus \left\{{K}\right\}\in \mathrm{Fin}$
54 32 53 syl ${⊢}{M}\in {B}\to {N}\setminus \left\{{K}\right\}\in \mathrm{Fin}$
55 54 adantr ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {N}\setminus \left\{{K}\right\}\in \mathrm{Fin}$
56 eqid ${⊢}\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)=\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)$
57 56 46 symgbasfi ${⊢}{N}\setminus \left\{{K}\right\}\in \mathrm{Fin}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\in \mathrm{Fin}$
58 55 57 syl ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\in \mathrm{Fin}$
59 simpll ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\right)\to {M}\in {B}$
60 difssd ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\right)\to {N}\setminus \left\{{K}\right\}\subseteq {N}$
61 1 2 submabas ${⊢}\left({M}\in {B}\wedge {N}\setminus \left\{{K}\right\}\subseteq {N}\right)\to \left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\in {\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}$
62 59 60 61 syl2anc ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\right)\to \left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\in {\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}$
63 simpr ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\right)\to {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}$
64 eqid ${⊢}\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}=\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}$
65 eqid ${⊢}{\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}={\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}$
66 46 47 18 64 65 21 madetsmelbas2 ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\in {\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\in {\mathrm{Base}}_{{R}}$
67 3 62 63 66 mp3an2i ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\in {\mathrm{Base}}_{{R}}$
68 67 ralrimiva ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \forall {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\in {\mathrm{Base}}_{{R}}$
69 25 30 58 68 gsummptcl ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)\in {\mathrm{Base}}_{{R}}$
70 25 26 12 mndrid ${⊢}\left({R}\in \mathrm{Mnd}\wedge \underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)\in {\mathrm{Base}}_{{R}}\right)\to \left(\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)\right){+}_{{R}}{0}_{{R}}=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)$
71 52 69 70 sylancr ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left(\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)\right){+}_{{R}}{0}_{{R}}=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)$
72 difssd ${⊢}{K}\in {N}\to {N}\setminus \left\{{K}\right\}\subseteq {N}$
73 61 3 jctil ${⊢}\left({M}\in {B}\wedge {N}\setminus \left\{{K}\right\}\subseteq {N}\right)\to \left({R}\in \mathrm{CRing}\wedge \left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\in {\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}\right)$
74 72 73 sylan2 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left({R}\in \mathrm{CRing}\wedge \left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\in {\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}\right)$
75 5 64 65 46 18 47 20 21 mdetleib2 ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\in {\mathrm{Base}}_{\left(\left({N}\setminus \left\{{K}\right\}\right)\mathrm{Mat}{R}\right)}\right)\to {E}\left(\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)$
76 74 75 syl ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {E}\left(\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)$
77 71 76 eqtr4d ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \left(\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\setminus \left\{{K}\right\}\right)}}{{\sum }_{{R}}},\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\setminus \left\{{K}\right\}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}\setminus \left\{{K}\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right){p}\left({n}\right)\right)\right)\right)\right){+}_{{R}}{0}_{{R}}={E}\left(\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\right)$
78 45 50 77 3eqtrd ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to \underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{n}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({n}\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={K},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right){p}\left({n}\right)\right)\right)\right)={E}\left(\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\right)$
79 15 24 78 3eqtrd ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {D}\left({K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){K}\right)={E}\left(\left({i}\in \left({N}\setminus \left\{{K}\right\}\right),{j}\in \left({N}\setminus \left\{{K}\right\}\right)⟼{i}{M}{j}\right)\right)$
80 9 79 eqtr4d ${⊢}\left({M}\in {B}\wedge {K}\in {N}\right)\to {E}\left({K}\left({N}\mathrm{subMat}{R}\right)\left({M}\right){K}\right)={D}\left({K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){K}\right)$