Metamath Proof Explorer

Theorem smadiadet

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 Mat R )
smadiadet.b 
|- B = ( Base ` A )
smadiadet.r 
|- R e. CRing
smadiadet.d 
|- D = ( N maDet R )
smadiadet.h 
|- E = ( ( N \ { K } ) maDet R )
Assertion smadiadet 
|- ( ( M e. B /\ K e. N ) -> ( E ` ( K ( ( N subMat R ) ` M ) K ) ) = ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) )

Proof

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