Step | Hyp | Ref
| Expression |
1 | | eqid 2821 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2821 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | eqid 2821 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | mdetpmtr.t |
. . 3
⊢ · =
(.r‘𝑅) |
5 | | crngring 19302 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
6 | 5 | ad2antrr 724 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ Ring) |
7 | | mdetpmtr.g |
. . . . 5
⊢ 𝐺 =
(Base‘(SymGrp‘𝑁)) |
8 | 7 | fvexi 6678 |
. . . 4
⊢ 𝐺 ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ V) |
10 | | simplr 767 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑁 ∈ Fin) |
11 | | mdetpmtr.s |
. . . . . . 7
⊢ 𝑆 = (pmSgn‘𝑁) |
12 | 11, 7 | psgndmfi 30735 |
. . . . . 6
⊢ (𝑁 ∈ Fin → 𝑆 Fn 𝐺) |
13 | | fnfun 6447 |
. . . . . 6
⊢ (𝑆 Fn 𝐺 → Fun 𝑆) |
14 | 10, 12, 13 | 3syl 18 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → Fun 𝑆) |
15 | | simprr 771 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ 𝐺) |
16 | | fndm 6449 |
. . . . . . 7
⊢ (𝑆 Fn 𝐺 → dom 𝑆 = 𝐺) |
17 | 10, 12, 16 | 3syl 18 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → dom 𝑆 = 𝐺) |
18 | 15, 17 | eleqtrrd 2916 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ dom 𝑆) |
19 | | fvco 6753 |
. . . . 5
⊢ ((Fun
𝑆 ∧ 𝑃 ∈ dom 𝑆) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
20 | 14, 18, 19 | syl2anc 586 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
21 | | mdetpmtr.z |
. . . . . 6
⊢ 𝑍 = (ℤRHom‘𝑅) |
22 | 7, 11, 21 | zrhpsgnelbas 20732 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
23 | 6, 10, 15, 22 | syl3anc 1367 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
24 | 20, 23 | eqeltrd 2913 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
25 | 6 | adantr 483 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑅 ∈ Ring) |
26 | 7, 11 | cofipsgn 20731 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
27 | 10, 26 | sylan 582 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
28 | | simpllr 774 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑁 ∈ Fin) |
29 | | simpr 487 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑝 ∈ 𝐺) |
30 | 7, 11, 21 | zrhpsgnelbas 20732 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
31 | 25, 28, 29, 30 | syl3anc 1367 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
32 | 27, 31 | eqeltrd 2913 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅)) |
33 | | eqid 2821 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
34 | 33, 1 | mgpbas 19239 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
35 | 33 | crngmgp 19299 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
36 | 35 | ad3antrrr 728 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
37 | | mdetpmtr.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
38 | | mdetpmtr.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
39 | | eqid 2821 |
. . . . . . . . 9
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
40 | 39, 7 | symgfv 18502 |
. . . . . . . 8
⊢ ((𝑝 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
41 | 40 | adantll 712 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
42 | | simpr 487 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
43 | | mdetpmtr1.e |
. . . . . . . . 9
⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) |
44 | | simpll 765 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CRing) |
45 | | simp1rr 1235 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ 𝐺) |
46 | | simp2 1133 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
47 | 39, 7 | symgfv 18502 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
48 | 45, 46, 47 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
49 | | simp3 1134 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
50 | | simp1rl 1234 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
51 | 37, 1, 38, 48, 49, 50 | matecld 21029 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑃‘𝑖)𝑀𝑗) ∈ (Base‘𝑅)) |
52 | 37, 1, 38, 10, 44, 51 | matbas2d 21026 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ∈ 𝐵) |
53 | 43, 52 | eqeltrid 2917 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐸 ∈ 𝐵) |
54 | 53 | ad2antrr 724 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 ∈ 𝐵) |
55 | 37, 1, 38, 41, 42, 54 | matecld 21029 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
56 | 55 | ralrimiva 3182 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
57 | 34, 36, 28, 56 | gsummptcl 19081 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) |
58 | 1, 4 | ringcl 19305 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
59 | 25, 32, 57, 58 | syl3anc 1367 |
. . 3
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
60 | | eqid 2821 |
. . . 4
⊢ (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) |
61 | 39, 7 | symgbasfi 18501 |
. . . . 5
⊢ (𝑁 ∈ Fin → 𝐺 ∈ Fin) |
62 | 10, 61 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ Fin) |
63 | | ovexd 7185 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ V) |
64 | | fvexd 6679 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (0g‘𝑅) ∈ V) |
65 | 60, 62, 63, 64 | fsuppmptdm 8838 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) finSupp (0g‘𝑅)) |
66 | 1, 2, 3, 4, 6, 9, 24, 59, 65 | gsummulc2 19351 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
67 | | nfcv 2977 |
. . . 4
⊢
Ⅎ𝑞(((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
68 | | fveq2 6664 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑍 ∘ 𝑆)‘𝑞) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
69 | | fveq1 6663 |
. . . . . . . 8
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑞‘𝑥) = ((𝑃 ∘ 𝑝)‘𝑥)) |
70 | 69 | oveq1d 7165 |
. . . . . . 7
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑞‘𝑥)𝑀𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
71 | 70 | mpteq2dv 5154 |
. . . . . 6
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
72 | 71 | oveq2d 7166 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
73 | 68, 72 | oveq12d 7168 |
. . . 4
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
74 | | ringcmn 19325 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
75 | 6, 74 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CMnd) |
76 | | ssidd 3989 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (Base‘𝑅) ⊆ (Base‘𝑅)) |
77 | 6 | adantr 483 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑅 ∈ Ring) |
78 | 7, 11 | cofipsgn 20731 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
79 | 10, 78 | sylan 582 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
80 | | simpllr 774 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑁 ∈ Fin) |
81 | | simpr 487 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑞 ∈ 𝐺) |
82 | 7, 11, 21 | zrhpsgnelbas 20732 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
83 | 77, 80, 81, 82 | syl3anc 1367 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
84 | 79, 83 | eqeltrd 2913 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅)) |
85 | 35 | ad3antrrr 728 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
86 | 39, 7 | symgfv 18502 |
. . . . . . . . 9
⊢ ((𝑞 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
87 | 86 | adantll 712 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
88 | | simpr 487 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
89 | | simprl 769 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑀 ∈ 𝐵) |
90 | 89 | ad2antrr 724 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
91 | 37, 1, 38, 87, 88, 90 | matecld 21029 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
92 | 91 | ralrimiva 3182 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
93 | 34, 85, 80, 92 | gsummptcl 19081 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) |
94 | 1, 4 | ringcl 19305 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
95 | 77, 84, 93, 94 | syl3anc 1367 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
96 | | eqid 2821 |
. . . . . . 7
⊢
(+g‘(SymGrp‘𝑁)) =
(+g‘(SymGrp‘𝑁)) |
97 | 39, 7, 96 | symgov 18506 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) = (𝑃 ∘ 𝑝)) |
98 | 39, 7, 96 | symgcl 18507 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) ∈ 𝐺) |
99 | 97, 98 | eqeltrrd 2914 |
. . . . 5
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
100 | 15, 99 | sylan 582 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
101 | 15 | adantr 483 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
102 | 7 | symgfcoeu 30721 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
103 | 80, 101, 81, 102 | syl3anc 1367 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
104 | 67, 1, 2, 73, 75, 62, 76, 95, 100, 103 | gsummptf1o 19077 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
105 | | mdetpmtr.d |
. . . . 5
⊢ 𝐷 = (𝑁 maDet 𝑅) |
106 | 105, 37, 38, 7, 21, 11, 4, 33 | mdetleib 21190 |
. . . 4
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
107 | 106 | ad2antrl 726 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
108 | 24 | adantr 483 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
109 | 1, 4 | ringass 19308 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅) ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅))) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
110 | 25, 108, 32, 57, 109 | syl13anc 1368 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
111 | 20 | adantr 483 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
112 | 111, 27 | oveq12d 7168 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
113 | 7, 11 | cofipsgn 20731 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ (𝑃 ∘ 𝑝) ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
114 | 28, 100, 113 | syl2anc 586 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
115 | 15 | adantr 483 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
116 | 39, 11, 7 | psgnco 20721 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
117 | 28, 115, 29, 116 | syl3anc 1367 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
118 | 117 | fveq2d 6668 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))) = (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝)))) |
119 | 21 | zrhrhm 20653 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑍 ∈ (ℤring
RingHom 𝑅)) |
120 | 6, 119 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
121 | 120 | adantr 483 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
122 | | 1z 12006 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
123 | | neg1z 12012 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
124 | | prssi 4747 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆
ℤ) |
125 | 122, 123,
124 | mp2an 690 |
. . . . . . . . . . 11
⊢ {1, -1}
⊆ ℤ |
126 | 7, 11 | psgnran 18637 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
127 | 28, 115, 126 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
128 | 125, 127 | sseldi 3964 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ ℤ) |
129 | 7, 11 | psgnran 18637 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
130 | 10, 129 | sylan 582 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
131 | 125, 130 | sseldi 3964 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ ℤ) |
132 | | zringbas 20617 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
133 | | zringmulr 20620 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
134 | 132, 133,
4 | rhmmul 19473 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (ℤring
RingHom 𝑅) ∧ (𝑆‘𝑃) ∈ ℤ ∧ (𝑆‘𝑝) ∈ ℤ) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
135 | 121, 128,
131, 134 | syl3anc 1367 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
136 | 114, 118,
135 | 3eqtrrd 2861 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
137 | 112, 136 | eqtrd 2856 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
138 | 43 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))) |
139 | | simprl 769 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑖 = (𝑝‘𝑥)) |
140 | 139 | fveq2d 6668 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = (𝑃‘(𝑝‘𝑥))) |
141 | | simpllr 774 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑝 ∈ 𝐺) |
142 | 39, 7 | symgbasf 18498 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐺 → 𝑝:𝑁⟶𝑁) |
143 | | ffun 6511 |
. . . . . . . . . . . . . 14
⊢ (𝑝:𝑁⟶𝑁 → Fun 𝑝) |
144 | 141, 142,
143 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → Fun 𝑝) |
145 | | simplr 767 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ 𝑁) |
146 | | fdm 6516 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:𝑁⟶𝑁 → dom 𝑝 = 𝑁) |
147 | 141, 142,
146 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → dom 𝑝 = 𝑁) |
148 | 145, 147 | eleqtrrd 2916 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ dom 𝑝) |
149 | | fvco 6753 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑝 ∧ 𝑥 ∈ dom 𝑝) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
150 | 144, 148,
149 | syl2anc 586 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
151 | 140, 150 | eqtr4d 2859 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = ((𝑃 ∘ 𝑝)‘𝑥)) |
152 | | simprr 771 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑗 = 𝑥) |
153 | 151, 152 | oveq12d 7168 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃‘𝑖)𝑀𝑗) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
154 | | ovexd 7185 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥) ∈ V) |
155 | 138, 153,
41, 42, 154 | ovmpod 7296 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
156 | 155 | mpteq2dva 5153 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
157 | 156 | oveq2d 7166 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
158 | 137, 157 | oveq12d 7168 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
159 | 110, 158 | eqtr3d 2858 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
160 | 159 | mpteq2dva 5153 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))) |
161 | 160 | oveq2d 7166 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
162 | 104, 107,
161 | 3eqtr4d 2866 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
163 | 105, 37, 38, 7, 21, 11, 4, 33 | mdetleib 21190 |
. . . 4
⊢ (𝐸 ∈ 𝐵 → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
164 | 53, 163 | syl 17 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
165 | 164 | oveq2d 7166 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
166 | 66, 162, 165 | 3eqtr4d 2866 |
1
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) |