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

Theorem mdetleib2 21844
Description: Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
Hypotheses
Ref Expression
mdetfval.d 𝐷 = (𝑁 maDet 𝑅)
mdetfval.a 𝐴 = (𝑁 Mat 𝑅)
mdetfval.b 𝐵 = (Base‘𝐴)
mdetfval.p 𝑃 = (Base‘(SymGrp‘𝑁))
mdetfval.y 𝑌 = (ℤRHom‘𝑅)
mdetfval.s 𝑆 = (pmSgn‘𝑁)
mdetfval.t · = (.r𝑅)
mdetfval.u 𝑈 = (mulGrp‘𝑅)
Assertion
Ref Expression
mdetleib2 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐷𝑀) = (𝑅 Σg (𝑝𝑃 ↦ (((𝑌𝑆)‘𝑝) · (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥))))))))
Distinct variable groups:   𝑥,𝑝,𝑀   𝑁,𝑝,𝑥   𝑅,𝑝,𝑥   𝐵,𝑝,𝑥   𝑃,𝑝,𝑥   𝑆,𝑝   𝑈,𝑝   𝑌,𝑝   · ,𝑝
Allowed substitution hints:   𝐴(𝑥,𝑝)   𝐷(𝑥,𝑝)   𝑆(𝑥)   · (𝑥)   𝑈(𝑥)   𝑌(𝑥)

Proof of Theorem mdetleib2
Dummy variables 𝑦 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetfval.d . . . 4 𝐷 = (𝑁 maDet 𝑅)
2 mdetfval.a . . . 4 𝐴 = (𝑁 Mat 𝑅)
3 mdetfval.b . . . 4 𝐵 = (Base‘𝐴)
4 mdetfval.p . . . 4 𝑃 = (Base‘(SymGrp‘𝑁))
5 mdetfval.y . . . 4 𝑌 = (ℤRHom‘𝑅)
6 mdetfval.s . . . 4 𝑆 = (pmSgn‘𝑁)
7 mdetfval.t . . . 4 · = (.r𝑅)
8 mdetfval.u . . . 4 𝑈 = (mulGrp‘𝑅)
91, 2, 3, 4, 5, 6, 7, 8mdetleib 21843 . . 3 (𝑀𝐵 → (𝐷𝑀) = (𝑅 Σg (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))))))
109adantl 482 . 2 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐷𝑀) = (𝑅 Σg (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))))))
11 eqid 2736 . . 3 (Base‘𝑅) = (Base‘𝑅)
12 crngring 19891 . . . . 5 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
13 ringcmn 19916 . . . . 5 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
1412, 13syl 17 . . . 4 (𝑅 ∈ CRing → 𝑅 ∈ CMnd)
1514adantr 481 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ CMnd)
162, 3matrcl 21666 . . . . . 6 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
1716adantl 482 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
1817simpld 495 . . . 4 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑁 ∈ Fin)
19 eqid 2736 . . . . 5 (SymGrp‘𝑁) = (SymGrp‘𝑁)
2019, 4symgbasfi 19083 . . . 4 (𝑁 ∈ Fin → 𝑃 ∈ Fin)
2118, 20syl 17 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑃 ∈ Fin)
2212ad2antrr 723 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → 𝑅 ∈ Ring)
235, 6coeq12i 5806 . . . . . . . . 9 (𝑌𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))
24 zrhpsgnmhm 20896 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2523, 24eqeltrid 2841 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑌𝑆) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2612, 18, 25syl2an2r 682 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑌𝑆) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
27 eqid 2736 . . . . . . . . 9 (mulGrp‘𝑅) = (mulGrp‘𝑅)
2827, 11mgpbas 19822 . . . . . . . 8 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
294, 28mhmf 18533 . . . . . . 7 ((𝑌𝑆) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (𝑌𝑆):𝑃⟶(Base‘𝑅))
3026, 29syl 17 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑌𝑆):𝑃⟶(Base‘𝑅))
3130ffvelcdmda 7018 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → ((𝑌𝑆)‘𝑞) ∈ (Base‘𝑅))
328, 11mgpbas 19822 . . . . . 6 (Base‘𝑅) = (Base‘𝑈)
338crngmgp 19887 . . . . . . 7 (𝑅 ∈ CRing → 𝑈 ∈ CMnd)
3433ad2antrr 723 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → 𝑈 ∈ CMnd)
3518adantr 481 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → 𝑁 ∈ Fin)
36 simpr 485 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀𝐵)
372, 11, 3matbas2i 21678 . . . . . . . . . 10 (𝑀𝐵𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
38 elmapi 8709 . . . . . . . . . 10 (𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3936, 37, 383syl 18 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
4039ad2antrr 723 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) ∧ 𝑦𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
4119, 4symgbasf1o 19079 . . . . . . . . . . 11 (𝑞𝑃𝑞:𝑁1-1-onto𝑁)
4241adantl 482 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → 𝑞:𝑁1-1-onto𝑁)
43 f1of 6768 . . . . . . . . . 10 (𝑞:𝑁1-1-onto𝑁𝑞:𝑁𝑁)
4442, 43syl 17 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → 𝑞:𝑁𝑁)
4544ffvelcdmda 7018 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) ∧ 𝑦𝑁) → (𝑞𝑦) ∈ 𝑁)
46 simpr 485 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) ∧ 𝑦𝑁) → 𝑦𝑁)
4740, 45, 46fovcdmd 7507 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) ∧ 𝑦𝑁) → ((𝑞𝑦)𝑀𝑦) ∈ (Base‘𝑅))
4847ralrimiva 3139 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → ∀𝑦𝑁 ((𝑞𝑦)𝑀𝑦) ∈ (Base‘𝑅))
4932, 34, 35, 48gsummptcl 19664 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))) ∈ (Base‘𝑅))
5011, 7ringcl 19896 . . . . 5 ((𝑅 ∈ Ring ∧ ((𝑌𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))) ∈ (Base‘𝑅)) → (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))) ∈ (Base‘𝑅))
5122, 31, 49, 50syl3anc 1370 . . . 4 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑞𝑃) → (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))) ∈ (Base‘𝑅))
5251ralrimiva 3139 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → ∀𝑞𝑃 (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))) ∈ (Base‘𝑅))
53 eqid 2736 . . 3 (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))) = (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))))
54 eqid 2736 . . . 4 (invg‘(SymGrp‘𝑁)) = (invg‘(SymGrp‘𝑁))
5519symggrp 19105 . . . . 5 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
5618, 55syl 17 . . . 4 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (SymGrp‘𝑁) ∈ Grp)
574, 54, 56grpinvf1o 18742 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (invg‘(SymGrp‘𝑁)):𝑃1-1-onto𝑃)
5811, 15, 21, 52, 53, 57gsummptfif1o 19665 . 2 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑅 Σg (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))))) = (𝑅 Σg ((𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))) ∘ (invg‘(SymGrp‘𝑁)))))
59 f1of 6768 . . . . . . 7 ((invg‘(SymGrp‘𝑁)):𝑃1-1-onto𝑃 → (invg‘(SymGrp‘𝑁)):𝑃𝑃)
6057, 59syl 17 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (invg‘(SymGrp‘𝑁)):𝑃𝑃)
6160ffvelcdmda 7018 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((invg‘(SymGrp‘𝑁))‘𝑝) ∈ 𝑃)
6260feqmptd 6894 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (invg‘(SymGrp‘𝑁)) = (𝑝𝑃 ↦ ((invg‘(SymGrp‘𝑁))‘𝑝)))
63 eqidd 2737 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))) = (𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))))
64 fveq2 6826 . . . . . 6 (𝑞 = ((invg‘(SymGrp‘𝑁))‘𝑝) → ((𝑌𝑆)‘𝑞) = ((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)))
65 fveq1 6825 . . . . . . . . 9 (𝑞 = ((invg‘(SymGrp‘𝑁))‘𝑝) → (𝑞𝑦) = (((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦))
6665oveq1d 7353 . . . . . . . 8 (𝑞 = ((invg‘(SymGrp‘𝑁))‘𝑝) → ((𝑞𝑦)𝑀𝑦) = ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))
6766mpteq2dv 5195 . . . . . . 7 (𝑞 = ((invg‘(SymGrp‘𝑁))‘𝑝) → (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)) = (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))
6867oveq2d 7354 . . . . . 6 (𝑞 = ((invg‘(SymGrp‘𝑁))‘𝑝) → (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))) = (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))))
6964, 68oveq12d 7356 . . . . 5 (𝑞 = ((invg‘(SymGrp‘𝑁))‘𝑝) → (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦)))) = (((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))))
7061, 62, 63, 69fmptco 7058 . . . 4 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))) ∘ (invg‘(SymGrp‘𝑁))) = (𝑝𝑃 ↦ (((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))))))
7119, 4, 54symginv 19107 . . . . . . . . 9 (𝑝𝑃 → ((invg‘(SymGrp‘𝑁))‘𝑝) = 𝑝)
7271adantl 482 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((invg‘(SymGrp‘𝑁))‘𝑝) = 𝑝)
7372fveq2d 6830 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) = ((𝑌𝑆)‘𝑝))
7412ad2antrr 723 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑅 ∈ Ring)
7518adantr 481 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑁 ∈ Fin)
76 simpr 485 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑝𝑃)
774, 5, 6zrhpsgninv 20897 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝𝑃) → ((𝑌𝑆)‘𝑝) = ((𝑌𝑆)‘𝑝))
7874, 75, 76, 77syl3anc 1370 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((𝑌𝑆)‘𝑝) = ((𝑌𝑆)‘𝑝))
7973, 78eqtrd 2776 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) = ((𝑌𝑆)‘𝑝))
80 eqid 2736 . . . . . . . 8 (Base‘𝑈) = (Base‘𝑈)
8133ad2antrr 723 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑈 ∈ CMnd)
8239ad2antrr 723 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
8371ad2antlr 724 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → ((invg‘(SymGrp‘𝑁))‘𝑝) = 𝑝)
8483fveq1d 6828 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → (((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦) = (𝑝𝑦))
8519, 4symgbasf1o 19079 . . . . . . . . . . . . . . 15 (𝑝𝑃𝑝:𝑁1-1-onto𝑁)
8685adantl 482 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑝:𝑁1-1-onto𝑁)
87 f1ocnv 6780 . . . . . . . . . . . . . 14 (𝑝:𝑁1-1-onto𝑁𝑝:𝑁1-1-onto𝑁)
88 f1of 6768 . . . . . . . . . . . . . 14 (𝑝:𝑁1-1-onto𝑁𝑝:𝑁𝑁)
8986, 87, 883syl 18 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑝:𝑁𝑁)
9089ffvelcdmda 7018 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → (𝑝𝑦) ∈ 𝑁)
9184, 90eqeltrd 2837 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → (((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦) ∈ 𝑁)
92 simpr 485 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → 𝑦𝑁)
9382, 91, 92fovcdmd 7507 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) ∈ (Base‘𝑅))
9493, 32eleqtrdi 2847 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑦𝑁) → ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) ∈ (Base‘𝑈))
9594ralrimiva 3139 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ∀𝑦𝑁 ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) ∈ (Base‘𝑈))
96 eqid 2736 . . . . . . . 8 (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) = (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))
9780, 81, 75, 95, 96, 86gsummptfif1o 19665 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))) = (𝑈 Σg ((𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝)))
98 f1of 6768 . . . . . . . . . . . 12 (𝑝:𝑁1-1-onto𝑁𝑝:𝑁𝑁)
9986, 98syl 17 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑝:𝑁𝑁)
10099ffvelcdmda 7018 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑥𝑁) → (𝑝𝑥) ∈ 𝑁)
10199feqmptd 6894 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → 𝑝 = (𝑥𝑁 ↦ (𝑝𝑥)))
102 eqidd 2737 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) = (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))
103 fveq2 6826 . . . . . . . . . . 11 (𝑦 = (𝑝𝑥) → (((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦) = (((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥)))
104 id 22 . . . . . . . . . . 11 (𝑦 = (𝑝𝑥) → 𝑦 = (𝑝𝑥))
105103, 104oveq12d 7356 . . . . . . . . . 10 (𝑦 = (𝑝𝑥) → ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) = ((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥))𝑀(𝑝𝑥)))
106100, 101, 102, 105fmptco 7058 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝) = (𝑥𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥))𝑀(𝑝𝑥))))
10771ad2antlr 724 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑥𝑁) → ((invg‘(SymGrp‘𝑁))‘𝑝) = 𝑝)
108107fveq1d 6828 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑥𝑁) → (((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥)) = (𝑝‘(𝑝𝑥)))
109 f1ocnvfv1 7205 . . . . . . . . . . . . 13 ((𝑝:𝑁1-1-onto𝑁𝑥𝑁) → (𝑝‘(𝑝𝑥)) = 𝑥)
11086, 109sylan 580 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑥𝑁) → (𝑝‘(𝑝𝑥)) = 𝑥)
111108, 110eqtrd 2776 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑥𝑁) → (((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥)) = 𝑥)
112111oveq1d 7353 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) ∧ 𝑥𝑁) → ((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥))𝑀(𝑝𝑥)) = (𝑥𝑀(𝑝𝑥)))
113112mpteq2dva 5193 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → (𝑥𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝𝑥))𝑀(𝑝𝑥))) = (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥))))
114106, 113eqtrd 2776 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → ((𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝) = (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥))))
115114oveq2d 7354 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → (𝑈 Σg ((𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝)) = (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥)))))
11697, 115eqtrd 2776 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))) = (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥)))))
11779, 116oveq12d 7356 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑝𝑃) → (((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))) = (((𝑌𝑆)‘𝑝) · (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥))))))
118117mpteq2dva 5193 . . . 4 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑝𝑃 ↦ (((𝑌𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦𝑁 ↦ ((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))))) = (𝑝𝑃 ↦ (((𝑌𝑆)‘𝑝) · (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥)))))))
11970, 118eqtrd 2776 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))) ∘ (invg‘(SymGrp‘𝑁))) = (𝑝𝑃 ↦ (((𝑌𝑆)‘𝑝) · (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥)))))))
120119oveq2d 7354 . 2 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑅 Σg ((𝑞𝑃 ↦ (((𝑌𝑆)‘𝑞) · (𝑈 Σg (𝑦𝑁 ↦ ((𝑞𝑦)𝑀𝑦))))) ∘ (invg‘(SymGrp‘𝑁)))) = (𝑅 Σg (𝑝𝑃 ↦ (((𝑌𝑆)‘𝑝) · (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥))))))))
12110, 58, 1203eqtrd 2780 1 ((𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝐷𝑀) = (𝑅 Σg (𝑝𝑃 ↦ (((𝑌𝑆)‘𝑝) · (𝑈 Σg (𝑥𝑁 ↦ (𝑥𝑀(𝑝𝑥))))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  Vcvv 3441  cmpt 5176   × cxp 5619  ccnv 5620  ccom 5625  wf 6476  1-1-ontowf1o 6479  cfv 6480  (class class class)co 7338  m cmap 8687  Fincfn 8805  Basecbs 17010  .rcmulr 17061   Σg cgsu 17249   MndHom cmhm 18526  Grpcgrp 18674  invgcminusg 18675  SymGrpcsymg 19071  pmSgncpsgn 19194  CMndccmn 19482  mulGrpcmgp 19816  Ringcrg 19879  CRingccrg 19880  ℤRHomczrh 20808   Mat cmat 21661   maDet cmdat 21840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-addf 11052  ax-mulf 11053
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-xor 1509  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-ot 4583  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-1st 7900  df-2nd 7901  df-supp 8049  df-tpos 8113  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-2o 8369  df-er 8570  df-map 8689  df-pm 8690  df-ixp 8758  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fsupp 9228  df-sup 9300  df-oi 9368  df-card 9797  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-xnn0 12408  df-z 12422  df-dec 12540  df-uz 12685  df-rp 12833  df-fz 13342  df-fzo 13485  df-seq 13824  df-exp 13885  df-hash 14147  df-word 14319  df-lsw 14367  df-concat 14375  df-s1 14401  df-substr 14453  df-pfx 14483  df-splice 14562  df-reverse 14571  df-s2 14661  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-0g 17250  df-gsum 17251  df-prds 17256  df-pws 17258  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-mhm 18528  df-submnd 18529  df-efmnd 18605  df-grp 18677  df-minusg 18678  df-mulg 18798  df-subg 18849  df-ghm 18929  df-gim 18972  df-cntz 19020  df-oppg 19047  df-symg 19072  df-pmtr 19147  df-psgn 19196  df-cmn 19484  df-abl 19485  df-mgp 19817  df-ur 19834  df-ring 19881  df-cring 19882  df-oppr 19958  df-dvdsr 19979  df-unit 19980  df-invr 20010  df-dvr 20021  df-rnghom 20055  df-drng 20096  df-subrg 20128  df-sra 20541  df-rgmod 20542  df-cnfld 20705  df-zring 20778  df-zrh 20812  df-dsmm 21046  df-frlm 21061  df-mat 21662  df-mdet 21841
This theorem is referenced by:  mdetrlin  21858  mdetrsca  21859  mdettpos  21867  smadiadet  21926
  Copyright terms: Public domain W3C validator