Step | Hyp | Ref
| 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‘𝑅) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 20393 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))))) |
10 | 9 | adantl 482 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))))) |
11 | | eqid 2622 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | | crngring 18558 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
13 | | ringcmn 18581 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd) |
15 | 14 | adantr 481 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ CMnd) |
16 | 2, 3 | matrcl 20218 |
. . . . . 6
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
17 | 16 | adantl 482 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
18 | 17 | simpld 475 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin) |
19 | | eqid 2622 |
. . . . 5
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
20 | 19, 4 | symgbasfi 17806 |
. . . 4
⊢ (𝑁 ∈ Fin → 𝑃 ∈ Fin) |
21 | 18, 20 | syl 17 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Fin) |
22 | 12 | ad2antrr 762 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → 𝑅 ∈ Ring) |
23 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
24 | 5, 6 | coeq12i 5285 |
. . . . . . . . 9
⊢ (𝑌 ∘ 𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) |
25 | | zrhpsgnmhm 19930 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))
∈ ((SymGrp‘𝑁)
MndHom (mulGrp‘𝑅))) |
26 | 24, 25 | syl5eqel 2705 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑌 ∘ 𝑆) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
27 | 23, 18, 26 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑌 ∘ 𝑆) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
28 | | eqid 2622 |
. . . . . . . . 9
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
29 | 28, 11 | mgpbas 18495 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
30 | 4, 29 | mhmf 17340 |
. . . . . . 7
⊢ ((𝑌 ∘ 𝑆) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (𝑌 ∘ 𝑆):𝑃⟶(Base‘𝑅)) |
31 | 27, 30 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑌 ∘ 𝑆):𝑃⟶(Base‘𝑅)) |
32 | 31 | ffvelrnda 6359 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅)) |
33 | 8, 11 | mgpbas 18495 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑈) |
34 | 8 | crngmgp 18555 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑈 ∈ CMnd) |
35 | 34 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → 𝑈 ∈ CMnd) |
36 | 18 | adantr 481 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → 𝑁 ∈ Fin) |
37 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
38 | 2, 11, 3 | matbas2i 20228 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
39 | | elmapi 7879 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
40 | 37, 38, 39 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
41 | 40 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
42 | 19, 4 | symgbasf1o 17803 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ 𝑃 → 𝑞:𝑁–1-1-onto→𝑁) |
43 | 42 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → 𝑞:𝑁–1-1-onto→𝑁) |
44 | | f1of 6137 |
. . . . . . . . . 10
⊢ (𝑞:𝑁–1-1-onto→𝑁 → 𝑞:𝑁⟶𝑁) |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → 𝑞:𝑁⟶𝑁) |
46 | 45 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → (𝑞‘𝑦) ∈ 𝑁) |
47 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁) |
48 | 41, 46, 47 | fovrnd 6806 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → ((𝑞‘𝑦)𝑀𝑦) ∈ (Base‘𝑅)) |
49 | 48 | ralrimiva 2966 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → ∀𝑦 ∈ 𝑁 ((𝑞‘𝑦)𝑀𝑦) ∈ (Base‘𝑅)) |
50 | 33, 35, 36, 49 | gsummptcl 18366 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))) ∈ (Base‘𝑅)) |
51 | 11, 7 | ringcl 18561 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑌 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))) ∈ (Base‘𝑅)) → (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)))) ∈ (Base‘𝑅)) |
52 | 22, 32, 50, 51 | syl3anc 1326 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑞 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)))) ∈ (Base‘𝑅)) |
53 | 52 | ralrimiva 2966 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∀𝑞 ∈ 𝑃 (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)))) ∈ (Base‘𝑅)) |
54 | | eqid 2622 |
. . 3
⊢ (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) = (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) |
55 | | eqid 2622 |
. . . 4
⊢
(invg‘(SymGrp‘𝑁)) =
(invg‘(SymGrp‘𝑁)) |
56 | 19 | symggrp 17820 |
. . . . 5
⊢ (𝑁 ∈ Fin →
(SymGrp‘𝑁) ∈
Grp) |
57 | 18, 56 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (SymGrp‘𝑁) ∈ Grp) |
58 | 4, 55, 57 | grpinvf1o 17485 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(invg‘(SymGrp‘𝑁)):𝑃–1-1-onto→𝑃) |
59 | 11, 15, 21, 53, 54, 58 | gsummptfif1o 18367 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)))))) = (𝑅 Σg ((𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) ∘
(invg‘(SymGrp‘𝑁))))) |
60 | | f1of 6137 |
. . . . . . 7
⊢
((invg‘(SymGrp‘𝑁)):𝑃–1-1-onto→𝑃 →
(invg‘(SymGrp‘𝑁)):𝑃⟶𝑃) |
61 | 58, 60 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(invg‘(SymGrp‘𝑁)):𝑃⟶𝑃) |
62 | 61 | ffvelrnda 6359 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) →
((invg‘(SymGrp‘𝑁))‘𝑝) ∈ 𝑃) |
63 | 61 | feqmptd 6249 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(invg‘(SymGrp‘𝑁)) = (𝑝 ∈ 𝑃 ↦
((invg‘(SymGrp‘𝑁))‘𝑝))) |
64 | | eqidd 2623 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) = (𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)))))) |
65 | | fveq2 6191 |
. . . . . 6
⊢ (𝑞 =
((invg‘(SymGrp‘𝑁))‘𝑝) → ((𝑌 ∘ 𝑆)‘𝑞) = ((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝))) |
66 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑞 =
((invg‘(SymGrp‘𝑁))‘𝑝) → (𝑞‘𝑦) =
(((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)) |
67 | 66 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑞 =
((invg‘(SymGrp‘𝑁))‘𝑝) → ((𝑞‘𝑦)𝑀𝑦) =
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) |
68 | 67 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑞 =
((invg‘(SymGrp‘𝑁))‘𝑝) → (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)) = (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))) |
69 | 68 | oveq2d 6666 |
. . . . . 6
⊢ (𝑞 =
((invg‘(SymGrp‘𝑁))‘𝑝) → (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))) = (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))) |
70 | 65, 69 | oveq12d 6668 |
. . . . 5
⊢ (𝑞 =
((invg‘(SymGrp‘𝑁))‘𝑝) → (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦)))) = (((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))))) |
71 | 62, 63, 64, 70 | fmptco 6396 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) ∘
(invg‘(SymGrp‘𝑁))) = (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))))) |
72 | 19, 4, 55 | symginv 17822 |
. . . . . . . . 9
⊢ (𝑝 ∈ 𝑃 →
((invg‘(SymGrp‘𝑁))‘𝑝) = ◡𝑝) |
73 | 72 | adantl 482 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) →
((invg‘(SymGrp‘𝑁))‘𝑝) = ◡𝑝) |
74 | 73 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) = ((𝑌 ∘ 𝑆)‘◡𝑝)) |
75 | 12 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑅 ∈ Ring) |
76 | 18 | adantr 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑁 ∈ Fin) |
77 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃) |
78 | 4, 5, 6 | zrhpsgninv 19931 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘◡𝑝) = ((𝑌 ∘ 𝑆)‘𝑝)) |
79 | 75, 76, 77, 78 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘◡𝑝) = ((𝑌 ∘ 𝑆)‘𝑝)) |
80 | 74, 79 | eqtrd 2656 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) = ((𝑌 ∘ 𝑆)‘𝑝)) |
81 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑈) =
(Base‘𝑈) |
82 | 34 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑈 ∈ CMnd) |
83 | 40 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
84 | 72 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) →
((invg‘(SymGrp‘𝑁))‘𝑝) = ◡𝑝) |
85 | 84 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) →
(((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦) = (◡𝑝‘𝑦)) |
86 | 19, 4 | symgbasf1o 17803 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ 𝑃 → 𝑝:𝑁–1-1-onto→𝑁) |
87 | 86 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑝:𝑁–1-1-onto→𝑁) |
88 | | f1ocnv 6149 |
. . . . . . . . . . . . . 14
⊢ (𝑝:𝑁–1-1-onto→𝑁 → ◡𝑝:𝑁–1-1-onto→𝑁) |
89 | | f1of 6137 |
. . . . . . . . . . . . . 14
⊢ (◡𝑝:𝑁–1-1-onto→𝑁 → ◡𝑝:𝑁⟶𝑁) |
90 | 87, 88, 89 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ◡𝑝:𝑁⟶𝑁) |
91 | 90 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → (◡𝑝‘𝑦) ∈ 𝑁) |
92 | 85, 91 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) →
(((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦) ∈ 𝑁) |
93 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁) |
94 | 83, 92, 93 | fovrnd 6806 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) →
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) ∈ (Base‘𝑅)) |
95 | 94, 33 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑦 ∈ 𝑁) →
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) ∈ (Base‘𝑈)) |
96 | 95 | ralrimiva 2966 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ∀𝑦 ∈ 𝑁
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) ∈ (Base‘𝑈)) |
97 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) = (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) |
98 | 81, 82, 76, 96, 97, 87 | gsummptfif1o 18367 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))) = (𝑈 Σg ((𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝))) |
99 | | f1of 6137 |
. . . . . . . . . . . 12
⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁) |
100 | 87, 99 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑝:𝑁⟶𝑁) |
101 | 100 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
102 | 100 | feqmptd 6249 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → 𝑝 = (𝑥 ∈ 𝑁 ↦ (𝑝‘𝑥))) |
103 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) = (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))) |
104 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑝‘𝑥) →
(((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦) =
(((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥))) |
105 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑝‘𝑥) → 𝑦 = (𝑝‘𝑥)) |
106 | 104, 105 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑝‘𝑥) →
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦) =
((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥))𝑀(𝑝‘𝑥))) |
107 | 101, 102,
103, 106 | fmptco 6396 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ((𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝) = (𝑥 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥))𝑀(𝑝‘𝑥)))) |
108 | 72 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝑁) →
((invg‘(SymGrp‘𝑁))‘𝑝) = ◡𝑝) |
109 | 108 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝑁) →
(((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥)) = (◡𝑝‘(𝑝‘𝑥))) |
110 | | f1ocnvfv1 6532 |
. . . . . . . . . . . . 13
⊢ ((𝑝:𝑁–1-1-onto→𝑁 ∧ 𝑥 ∈ 𝑁) → (◡𝑝‘(𝑝‘𝑥)) = 𝑥) |
111 | 87, 110 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝑁) → (◡𝑝‘(𝑝‘𝑥)) = 𝑥) |
112 | 109, 111 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝑁) →
(((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥)) = 𝑥) |
113 | 112 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝑁) →
((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥))𝑀(𝑝‘𝑥)) = (𝑥𝑀(𝑝‘𝑥))) |
114 | 113 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → (𝑥 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘(𝑝‘𝑥))𝑀(𝑝‘𝑥))) = (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥)))) |
115 | 107, 114 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → ((𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝) = (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥)))) |
116 | 115 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → (𝑈 Σg ((𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)) ∘ 𝑝)) = (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥))))) |
117 | 98, 116 | eqtrd 2656 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))) = (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥))))) |
118 | 80, 117 | oveq12d 6668 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑝 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦)))) = (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥)))))) |
119 | 118 | mpteq2dva 4744 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘((invg‘(SymGrp‘𝑁))‘𝑝)) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦
((((invg‘(SymGrp‘𝑁))‘𝑝)‘𝑦)𝑀𝑦))))) = (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥))))))) |
120 | 71, 119 | eqtrd 2656 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) ∘
(invg‘(SymGrp‘𝑁))) = (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥))))))) |
121 | 120 | oveq2d 6666 |
. 2
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg ((𝑞 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑞) · (𝑈 Σg (𝑦 ∈ 𝑁 ↦ ((𝑞‘𝑦)𝑀𝑦))))) ∘
(invg‘(SymGrp‘𝑁)))) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥)))))))) |
122 | 10, 59, 121 | 3eqtrd 2660 |
1
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥)))))))) |