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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
smadiadet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
smadiadet.r ⊢ 𝑅 ∈ CRing
smadiadet.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
smadiadet.h ⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
Assertion smadiadet ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 smadiadet.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 smadiadet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 smadiadet.r ⊢ 𝑅 ∈ CRing
4 smadiadet.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
5 smadiadet.h ⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
6 eqid ⊢ ( 𝑁 subMat 𝑅 ) = ( 𝑁 subMat 𝑅 )
7 1 6 2 submaval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
8 7 3anidm23 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
9 8 fveq2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐸 ‘ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
10 eqid ⊢ ( 𝑁 minMatR1 𝑅 ) = ( 𝑁 minMatR1 𝑅 )
11 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 1 2 10 11 12 minmar1val ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
14 13 3anidm23 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
15 14 fveq2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
16 1 2 3 12 11 marep01ma ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 )
17 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
18 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
19 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
20 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
22 4 1 2 17 18 19 20 21 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
23 3 16 22 sylancr ⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
24 23 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
27 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
28 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
29 3 27 28 mp2b ⊢ 𝑅 ∈ CMnd
30 29 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
31 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
32 31 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
33 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
34 33 17 symgbasfi ⊢ ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
35 32 34 syl ⊢ ( 𝑀 ∈ 𝐵 → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
36 35 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
37 1 2 3 12 11 17 21 18 19 20 smadiadetlem1 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
38 disjdif ⊢ ( { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ∩ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ) = ∅
39 38 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ∩ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ) = ∅ )
40 ssrab2 ⊢ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
41 40 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
42 undif ⊢ ( { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ ( { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
43 41 42 sylib ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
44 43 eqcomd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ) )
45 25 26 30 36 37 39 44 gsummptfidmsplit ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ) )
46 eqid ⊢ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
47 eqid ⊢ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
48 1 2 3 12 11 17 21 18 19 20 46 47 smadiadetlem4 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
49 1 2 3 12 11 17 21 18 19 20 smadiadetlem2 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
50 48 49 oveq12d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ { 𝑞 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
51 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
52 3 27 51 mp2b ⊢ 𝑅 ∈ Mnd
53 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
54 32 53 syl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
55 54 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
56 eqid ⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
57 56 46 symgbasfi ⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin → ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∈ Fin )
58 55 57 syl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∈ Fin )
59 simpll ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → 𝑀 ∈ 𝐵 )
60 difssd ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
61 1 2 submabas ⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) )
62 59 60 61 syl2anc ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) )
63 simpr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
64 eqid ⊢ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) = ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 )
65 eqid ⊢ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) = ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) )
66 46 47 18 64 65 21 madetsmelbas2 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
67 3 62 63 66 mp3an2i ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
68 67 ralrimiva ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ∀ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
69 25 30 58 68 gsummptcl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
70 25 26 12 mndrid ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
71 52 69 70 sylancr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
72 difssd ⊢ ( 𝐾 ∈ 𝑁 → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
73 61 3 jctil ⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) → ( 𝑅 ∈ CRing ∧ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) ) )
74 72 73 sylan2 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 ∈ CRing ∧ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) ) )
75 5 64 65 46 18 47 20 21 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( ( 𝑁 ∖ { 𝐾 } ) Mat 𝑅 ) ) ) → ( 𝐸 ‘ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
76 74 75 syl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
77 71 76 eqtr4d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 𝐸 ‘ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
78 45 50 77 3eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝐸 ‘ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
79 15 24 78 3eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐸 ‘ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ) )
80 9 79 eqtr4d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) )