Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smadiadet Structured version   Visualization version   GIF version

 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.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables 𝑖 𝑗 𝑛 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smadiadet.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
2 eqid 2610 . . . . 5 (𝑁 subMat 𝑅) = (𝑁 subMat 𝑅)
41, 2, 3submaval 20206 . . . 4 ((𝑀𝐵𝐾𝑁𝐾𝑁) → (𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)))
543anidm23 1377 . . 3 ((𝑀𝐵𝐾𝑁) → (𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)))
65fveq2d 6107 . 2 ((𝑀𝐵𝐾𝑁) → (𝐸‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)) = (𝐸‘(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))))
7 eqid 2610 . . . . . 6 (𝑁 minMatR1 𝑅) = (𝑁 minMatR1 𝑅)
8 eqid 2610 . . . . . 6 (1r𝑅) = (1r𝑅)
9 eqid 2610 . . . . . 6 (0g𝑅) = (0g𝑅)
101, 3, 7, 8, 9minmar1val 20273 . . . . 5 ((𝑀𝐵𝐾𝑁𝐾𝑁) → (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) = (𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗))))
11103anidm23 1377 . . . 4 ((𝑀𝐵𝐾𝑁) → (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) = (𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗))))
1211fveq2d 6107 . . 3 ((𝑀𝐵𝐾𝑁) → (𝐷‘(𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾)) = (𝐷‘(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))))
141, 3, 13, 9, 8marep01ma 20285 . . . . 5 (𝑀𝐵 → (𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗))) ∈ 𝐵)
16 eqid 2610 . . . . . 6 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
17 eqid 2610 . . . . . 6 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
18 eqid 2610 . . . . . 6 (pmSgn‘𝑁) = (pmSgn‘𝑁)
19 eqid 2610 . . . . . 6 (.r𝑅) = (.r𝑅)
20 eqid 2610 . . . . . 6 (mulGrp‘𝑅) = (mulGrp‘𝑅)
2115, 1, 3, 16, 17, 18, 19, 20mdetleib2 20213 . . . . 5 ((𝑅 ∈ CRing ∧ (𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗))) ∈ 𝐵) → (𝐷‘(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛))))))))
2213, 14, 21sylancr 694 . . . 4 (𝑀𝐵 → (𝐷‘(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛))))))))
2322adantr 480 . . 3 ((𝑀𝐵𝐾𝑁) → (𝐷‘(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛))))))))
24 eqid 2610 . . . . 5 (Base‘𝑅) = (Base‘𝑅)
25 eqid 2610 . . . . 5 (+g𝑅) = (+g𝑅)
26 crngring 18381 . . . . . . 7 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
27 ringcmn 18404 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
2813, 26, 27mp2b 10 . . . . . 6 𝑅 ∈ CMnd
2928a1i 11 . . . . 5 ((𝑀𝐵𝐾𝑁) → 𝑅 ∈ CMnd)
301, 3matrcl 20037 . . . . . . . 8 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
3130simpld 474 . . . . . . 7 (𝑀𝐵𝑁 ∈ Fin)
32 eqid 2610 . . . . . . . 8 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3332, 16symgbasfi 17629 . . . . . . 7 (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
3431, 33syl 17 . . . . . 6 (𝑀𝐵 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
3534adantr 480 . . . . 5 ((𝑀𝐵𝐾𝑁) → (Base‘(SymGrp‘𝑁)) ∈ Fin)
361, 3, 13, 9, 8, 16, 20, 17, 18, 19smadiadetlem1 20287 . . . . 5 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛))))) ∈ (Base‘𝑅))
37 disjdif 3992 . . . . . 6 ({𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ∩ ((Base‘(SymGrp‘𝑁)) ∖ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾})) = ∅
3837a1i 11 . . . . 5 ((𝑀𝐵𝐾𝑁) → ({𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ∩ ((Base‘(SymGrp‘𝑁)) ∖ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾})) = ∅)
39 ssrab2 3650 . . . . . . . 8 {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ⊆ (Base‘(SymGrp‘𝑁))
4039a1i 11 . . . . . . 7 ((𝑀𝐵𝐾𝑁) → {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ⊆ (Base‘(SymGrp‘𝑁)))
41 undif 4001 . . . . . . 7 ({𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ⊆ (Base‘(SymGrp‘𝑁)) ↔ ({𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ∪ ((Base‘(SymGrp‘𝑁)) ∖ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾})) = (Base‘(SymGrp‘𝑁)))
4240, 41sylib 207 . . . . . 6 ((𝑀𝐵𝐾𝑁) → ({𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ∪ ((Base‘(SymGrp‘𝑁)) ∖ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾})) = (Base‘(SymGrp‘𝑁)))
4342eqcomd 2616 . . . . 5 ((𝑀𝐵𝐾𝑁) → (Base‘(SymGrp‘𝑁)) = ({𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ∪ ((Base‘(SymGrp‘𝑁)) ∖ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾})))
4424, 25, 29, 35, 36, 38, 43gsummptfidmsplit 18153 . . . 4 ((𝑀𝐵𝐾𝑁) → (𝑅 Σ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𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛)))))))))
45 eqid 2610 . . . . . 6 (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))
46 eqid 2610 . . . . . 6 (pmSgn‘(𝑁 ∖ {𝐾})) = (pmSgn‘(𝑁 ∖ {𝐾}))
471, 3, 13, 9, 8, 16, 20, 17, 18, 19, 45, 46smadiadetlem4 20294 . . . . 5 ((𝑀𝐵𝐾𝑁) → (𝑅 Σg (𝑝 ∈ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛))))))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))))))
481, 3, 13, 9, 8, 16, 20, 17, 18, 19smadiadetlem2 20289 . . . . 5 ((𝑀𝐵𝐾𝑁) → (𝑅 Σg (𝑝 ∈ ((Base‘(SymGrp‘𝑁)) ∖ {𝑞 ∈ (Base‘(SymGrp‘𝑁)) ∣ (𝑞𝐾) = 𝐾}) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r𝑅), (0g𝑅)), (𝑖𝑀𝑗)))(𝑝𝑛))))))) = (0g𝑅))
4947, 48oveq12d 6567 . . . 4 ((𝑀𝐵𝐾𝑁) → ((𝑅 Σ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𝑅)))
50 ringmnd 18379 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
5113, 26, 50mp2b 10 . . . . . 6 𝑅 ∈ Mnd
52 diffi 8077 . . . . . . . . . 10 (𝑁 ∈ Fin → (𝑁 ∖ {𝐾}) ∈ Fin)
5331, 52syl 17 . . . . . . . . 9 (𝑀𝐵 → (𝑁 ∖ {𝐾}) ∈ Fin)
5453adantr 480 . . . . . . . 8 ((𝑀𝐵𝐾𝑁) → (𝑁 ∖ {𝐾}) ∈ Fin)
55 eqid 2610 . . . . . . . . 9 (SymGrp‘(𝑁 ∖ {𝐾})) = (SymGrp‘(𝑁 ∖ {𝐾}))
5655, 45symgbasfi 17629 . . . . . . . 8 ((𝑁 ∖ {𝐾}) ∈ Fin → (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ∈ Fin)
5754, 56syl 17 . . . . . . 7 ((𝑀𝐵𝐾𝑁) → (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ∈ Fin)
5813a1i 11 . . . . . . . . 9 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → 𝑅 ∈ CRing)
59 simpll 786 . . . . . . . . . 10 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → 𝑀𝐵)
60 difssd 3700 . . . . . . . . . 10 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → (𝑁 ∖ {𝐾}) ⊆ 𝑁)
611, 3submabas 20203 . . . . . . . . . 10 ((𝑀𝐵 ∧ (𝑁 ∖ {𝐾}) ⊆ 𝑁) → (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅)))
6259, 60, 61syl2anc 691 . . . . . . . . 9 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅)))
63 simpr 476 . . . . . . . . 9 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))))
64 eqid 2610 . . . . . . . . . 10 ((𝑁 ∖ {𝐾}) Mat 𝑅) = ((𝑁 ∖ {𝐾}) Mat 𝑅)
65 eqid 2610 . . . . . . . . . 10 (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅)) = (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅))
6645, 46, 17, 64, 65, 20madetsmelbas2 20090 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅)) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))) ∈ (Base‘𝑅))
6758, 62, 63, 66syl3anc 1318 . . . . . . . 8 (((𝑀𝐵𝐾𝑁) ∧ 𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))) ∈ (Base‘𝑅))
6867ralrimiva 2949 . . . . . . 7 ((𝑀𝐵𝐾𝑁) → ∀𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))) ∈ (Base‘𝑅))
6924, 29, 57, 68gsummptcl 18189 . . . . . 6 ((𝑀𝐵𝐾𝑁) → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))))) ∈ (Base‘𝑅))
7024, 25, 9mndrid 17135 . . . . . 6 ((𝑅 ∈ 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 (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))))))
7151, 69, 70sylancr 694 . . . . 5 ((𝑀𝐵𝐾𝑁) → ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛)))))))(+g𝑅)(0g𝑅)) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘(𝑁 ∖ {𝐾})))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝𝑛))))))))
72 difssd 3700 . . . . . . 7 (𝐾𝑁 → (𝑁 ∖ {𝐾}) ⊆ 𝑁)
7361, 13jctil 558 . . . . . . 7 ((𝑀𝐵 ∧ (𝑁 ∖ {𝐾}) ⊆ 𝑁) → (𝑅 ∈ CRing ∧ (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅))))
7472, 73sylan2 490 . . . . . 6 ((𝑀𝐵𝐾𝑁) → (𝑅 ∈ CRing ∧ (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅))))