Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2610 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | eqid 2610 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | mdetpmtr.t |
. . 3
⊢ · =
(.r‘𝑅) |
5 | | simpll 786 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CRing) |
6 | | crngring 18381 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ Ring) |
8 | | mdetpmtr.g |
. . . . 5
⊢ 𝐺 =
(Base‘(SymGrp‘𝑁)) |
9 | | fvex 6113 |
. . . . 5
⊢
(Base‘(SymGrp‘𝑁)) ∈ V |
10 | 8, 9 | eqeltri 2684 |
. . . 4
⊢ 𝐺 ∈ V |
11 | 10 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ V) |
12 | | simplr 788 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑁 ∈ Fin) |
13 | | mdetpmtr.s |
. . . . . . 7
⊢ 𝑆 = (pmSgn‘𝑁) |
14 | 13, 8 | psgndmfi 29177 |
. . . . . 6
⊢ (𝑁 ∈ Fin → 𝑆 Fn 𝐺) |
15 | | fnfun 5902 |
. . . . . 6
⊢ (𝑆 Fn 𝐺 → Fun 𝑆) |
16 | 12, 14, 15 | 3syl 18 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → Fun 𝑆) |
17 | | simprr 792 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ 𝐺) |
18 | | fndm 5904 |
. . . . . . 7
⊢ (𝑆 Fn 𝐺 → dom 𝑆 = 𝐺) |
19 | 12, 14, 18 | 3syl 18 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → dom 𝑆 = 𝐺) |
20 | 17, 19 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ dom 𝑆) |
21 | | fvco 6184 |
. . . . 5
⊢ ((Fun
𝑆 ∧ 𝑃 ∈ dom 𝑆) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
22 | 16, 20, 21 | syl2anc 691 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
23 | | mdetpmtr.z |
. . . . . 6
⊢ 𝑍 = (ℤRHom‘𝑅) |
24 | 8, 13, 23 | zrhpsgnelbas 19759 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
25 | 7, 12, 17, 24 | syl3anc 1318 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
26 | 22, 25 | eqeltrd 2688 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
27 | 7 | adantr 480 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑅 ∈ Ring) |
28 | 8, 23, 13 | zrhcofipsgn 19758 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
29 | 12, 28 | sylan 487 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
30 | 12 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑁 ∈ Fin) |
31 | | simpr 476 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑝 ∈ 𝐺) |
32 | 8, 13, 23 | zrhpsgnelbas 19759 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
33 | 27, 30, 31, 32 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
34 | 29, 33 | eqeltrd 2688 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅)) |
35 | | eqid 2610 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
36 | 35, 1 | mgpbas 18318 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
37 | 35 | crngmgp 18378 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
38 | 37 | ad3antrrr 762 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
39 | | mdetpmtr.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
40 | | mdetpmtr.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
41 | | simplr 788 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑝 ∈ 𝐺) |
42 | | simpr 476 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
43 | | eqid 2610 |
. . . . . . . . 9
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
44 | 43, 8 | symgfv 17630 |
. . . . . . . 8
⊢ ((𝑝 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
45 | 41, 42, 44 | syl2anc 691 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
46 | | mdetpmtr1.e |
. . . . . . . . 9
⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) |
47 | | simp1rr 1120 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ 𝐺) |
48 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
49 | 43, 8 | symgfv 17630 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
50 | 47, 48, 49 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
51 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
52 | | simp1rl 1119 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
53 | 39, 1, 40, 50, 51, 52 | matecld 20051 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑃‘𝑖)𝑀𝑗) ∈ (Base‘𝑅)) |
54 | 39, 1, 40, 12, 5, 53 | matbas2d 20048 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ∈ 𝐵) |
55 | 46, 54 | syl5eqel 2692 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐸 ∈ 𝐵) |
56 | 55 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 ∈ 𝐵) |
57 | 39, 1, 40, 45, 42, 56 | matecld 20051 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
58 | 57 | ralrimiva 2949 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
59 | 36, 38, 30, 58 | gsummptcl 18189 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) |
60 | 1, 4 | ringcl 18384 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
61 | 27, 34, 59, 60 | syl3anc 1318 |
. . 3
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
62 | | eqid 2610 |
. . . 4
⊢ (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) |
63 | 43, 8 | symgbasfi 17629 |
. . . . 5
⊢ (𝑁 ∈ Fin → 𝐺 ∈ Fin) |
64 | 12, 63 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ Fin) |
65 | | ovex 6577 |
. . . . 5
⊢ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ V |
66 | 65 | a1i 11 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ V) |
67 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
68 | 67 | a1i 11 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (0g‘𝑅) ∈ V) |
69 | 62, 64, 66, 68 | fsuppmptdm 8169 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) finSupp (0g‘𝑅)) |
70 | 1, 2, 3, 4, 7, 11,
26, 61, 69 | gsummulc2 18430 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
71 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑞(((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
72 | | fveq2 6103 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑍 ∘ 𝑆)‘𝑞) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
73 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑞‘𝑥) = ((𝑃 ∘ 𝑝)‘𝑥)) |
74 | 73 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑞‘𝑥)𝑀𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
75 | 74 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
76 | 75 | oveq2d 6565 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
77 | 72, 76 | oveq12d 6567 |
. . . 4
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
78 | | ringcmn 18404 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
79 | 7, 78 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CMnd) |
80 | | ssid 3587 |
. . . . 5
⊢
(Base‘𝑅)
⊆ (Base‘𝑅) |
81 | 80 | a1i 11 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (Base‘𝑅) ⊆ (Base‘𝑅)) |
82 | 7 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑅 ∈ Ring) |
83 | 12 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑁 ∈ Fin) |
84 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑞 ∈ 𝐺) |
85 | 8, 23, 13 | zrhcofipsgn 19758 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
86 | 83, 84, 85 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
87 | 8, 13, 23 | zrhpsgnelbas 19759 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
88 | 82, 83, 84, 87 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
89 | 86, 88 | eqeltrd 2688 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅)) |
90 | 37 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
91 | | simpllr 795 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑁 ∈ Fin) |
92 | | simplr 788 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑞 ∈ 𝐺) |
93 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
94 | 43, 8 | symgfv 17630 |
. . . . . . . . 9
⊢ ((𝑞 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
95 | 92, 93, 94 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
96 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑀 ∈ 𝐵) |
97 | 96 | ad2antrr 758 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
98 | 39, 1, 40, 95, 93, 97 | matecld 20051 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
99 | 98 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
100 | 36, 90, 91, 99 | gsummptcl 18189 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) |
101 | 1, 4 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
102 | 82, 89, 100, 101 | syl3anc 1318 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
103 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘(SymGrp‘𝑁)) =
(+g‘(SymGrp‘𝑁)) |
104 | 43, 8, 103 | symgov 17633 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) = (𝑃 ∘ 𝑝)) |
105 | 43, 8, 103 | symgcl 17634 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) ∈ 𝐺) |
106 | 104, 105 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
107 | 17, 106 | sylan 487 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
108 | 17 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
109 | 8 | symgfcoeu 29176 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
110 | 83, 108, 84, 109 | syl3anc 1318 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
111 | 71, 1, 2, 77, 79, 64, 81, 102, 107, 110 | gsummptf1o 18185 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
112 | | mdetpmtr.d |
. . . . 5
⊢ 𝐷 = (𝑁 maDet 𝑅) |
113 | 112, 39, 40, 8, 23, 13, 4, 35 | mdetleib 20212 |
. . . 4
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
114 | 113 | ad2antrl 760 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
115 | 26 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
116 | 1, 4 | ringass 18387 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅) ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅))) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
117 | 27, 115, 34, 59, 116 | syl13anc 1320 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
118 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
119 | 118, 29 | oveq12d 6567 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
120 | 8, 23, 13 | zrhcofipsgn 19758 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ (𝑃 ∘ 𝑝) ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
121 | 30, 107, 120 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
122 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
123 | 43, 13, 8 | psgnco 19748 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
124 | 30, 122, 31, 123 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
125 | 124 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))) = (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝)))) |
126 | 23 | zrhrhm 19679 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑍 ∈ (ℤring
RingHom 𝑅)) |
127 | 7, 126 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
128 | 127 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
129 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
130 | | neg1z 11290 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
131 | | prssi 4293 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆
ℤ) |
132 | 129, 130,
131 | mp2an 704 |
. . . . . . . . . . 11
⊢ {1, -1}
⊆ ℤ |
133 | 8, 13 | psgnran 17758 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
134 | 30, 122, 133 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
135 | 132, 134 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ ℤ) |
136 | 8, 13 | psgnran 17758 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
137 | 30, 31, 136 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
138 | 132, 137 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ ℤ) |
139 | | zringbas 19643 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
140 | | zringmulr 19646 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
141 | 139, 140,
4 | rhmmul 18550 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (ℤring
RingHom 𝑅) ∧ (𝑆‘𝑃) ∈ ℤ ∧ (𝑆‘𝑝) ∈ ℤ) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
142 | 128, 135,
138, 141 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
143 | 121, 125,
142 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
144 | 119, 143 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
145 | 46 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))) |
146 | | simprl 790 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑖 = (𝑝‘𝑥)) |
147 | 146 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = (𝑃‘(𝑝‘𝑥))) |
148 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑝 ∈ 𝐺) |
149 | 43, 8 | symgbasf 17627 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐺 → 𝑝:𝑁⟶𝑁) |
150 | | ffun 5961 |
. . . . . . . . . . . . . 14
⊢ (𝑝:𝑁⟶𝑁 → Fun 𝑝) |
151 | 148, 149,
150 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → Fun 𝑝) |
152 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ 𝑁) |
153 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:𝑁⟶𝑁 → dom 𝑝 = 𝑁) |
154 | 148, 149,
153 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → dom 𝑝 = 𝑁) |
155 | 152, 154 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ dom 𝑝) |
156 | | fvco 6184 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑝 ∧ 𝑥 ∈ dom 𝑝) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
157 | 151, 155,
156 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
158 | 147, 157 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = ((𝑃 ∘ 𝑝)‘𝑥)) |
159 | | simprr 792 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑗 = 𝑥) |
160 | 158, 159 | oveq12d 6567 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃‘𝑖)𝑀𝑗) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
161 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥) ∈ V |
162 | 161 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥) ∈ V) |
163 | 145, 160,
45, 42, 162 | ovmpt2d 6686 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
164 | 163 | mpteq2dva 4672 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
165 | 164 | oveq2d 6565 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
166 | 144, 165 | oveq12d 6567 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
167 | 117, 166 | eqtr3d 2646 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
168 | 167 | mpteq2dva 4672 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))) |
169 | 168 | oveq2d 6565 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
170 | 111, 114,
169 | 3eqtr4d 2654 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
171 | 112, 39, 40, 8, 23, 13, 4, 35 | mdetleib 20212 |
. . . 4
⊢ (𝐸 ∈ 𝐵 → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
172 | 55, 171 | syl 17 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
173 | 172 | oveq2d 6565 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
174 | 70, 170, 173 | 3eqtr4d 2654 |
1
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) |