Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2731 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | mdetpmtr.t |
. . 3
⊢ · =
(.r‘𝑅) |
4 | | crngring 20146 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
5 | 4 | ad2antrr 723 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ Ring) |
6 | | mdetpmtr.g |
. . . . 5
⊢ 𝐺 =
(Base‘(SymGrp‘𝑁)) |
7 | 6 | fvexi 6905 |
. . . 4
⊢ 𝐺 ∈ V |
8 | 7 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ V) |
9 | | simplr 766 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑁 ∈ Fin) |
10 | | mdetpmtr.s |
. . . . . . 7
⊢ 𝑆 = (pmSgn‘𝑁) |
11 | 10, 6 | psgndmfi 32693 |
. . . . . 6
⊢ (𝑁 ∈ Fin → 𝑆 Fn 𝐺) |
12 | | fnfun 6649 |
. . . . . 6
⊢ (𝑆 Fn 𝐺 → Fun 𝑆) |
13 | 9, 11, 12 | 3syl 18 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → Fun 𝑆) |
14 | | simprr 770 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ 𝐺) |
15 | | fndm 6652 |
. . . . . . 7
⊢ (𝑆 Fn 𝐺 → dom 𝑆 = 𝐺) |
16 | 9, 11, 15 | 3syl 18 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → dom 𝑆 = 𝐺) |
17 | 14, 16 | eleqtrrd 2835 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ dom 𝑆) |
18 | | fvco 6989 |
. . . . 5
⊢ ((Fun
𝑆 ∧ 𝑃 ∈ dom 𝑆) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
19 | 13, 17, 18 | syl2anc 583 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
20 | | mdetpmtr.z |
. . . . . 6
⊢ 𝑍 = (ℤRHom‘𝑅) |
21 | 6, 10, 20 | zrhpsgnelbas 21457 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
22 | 5, 9, 14, 21 | syl3anc 1370 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
23 | 19, 22 | eqeltrd 2832 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
24 | 5 | adantr 480 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑅 ∈ Ring) |
25 | 6, 10 | cofipsgn 21456 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
26 | 9, 25 | sylan 579 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
27 | | simpllr 773 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑁 ∈ Fin) |
28 | | simpr 484 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑝 ∈ 𝐺) |
29 | 6, 10, 20 | zrhpsgnelbas 21457 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
30 | 24, 27, 28, 29 | syl3anc 1370 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
31 | 26, 30 | eqeltrd 2832 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅)) |
32 | | eqid 2731 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
33 | 32, 1 | mgpbas 20041 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
34 | 32 | crngmgp 20142 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
35 | 34 | ad3antrrr 727 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
36 | | mdetpmtr.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
37 | | mdetpmtr.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
38 | | eqid 2731 |
. . . . . . . . 9
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
39 | 38, 6 | symgfv 19295 |
. . . . . . . 8
⊢ ((𝑝 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
40 | 39 | adantll 711 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
41 | | simpr 484 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
42 | | mdetpmtr1.e |
. . . . . . . . 9
⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) |
43 | | simpll 764 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CRing) |
44 | | simp1rr 1238 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ 𝐺) |
45 | | simp2 1136 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
46 | 38, 6 | symgfv 19295 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
47 | 44, 45, 46 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
48 | | simp3 1137 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
49 | | simp1rl 1237 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
50 | 36, 1, 37, 47, 48, 49 | matecld 22248 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑃‘𝑖)𝑀𝑗) ∈ (Base‘𝑅)) |
51 | 36, 1, 37, 9, 43, 50 | matbas2d 22245 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ∈ 𝐵) |
52 | 42, 51 | eqeltrid 2836 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐸 ∈ 𝐵) |
53 | 52 | ad2antrr 723 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 ∈ 𝐵) |
54 | 36, 1, 37, 40, 41, 53 | matecld 22248 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
55 | 54 | ralrimiva 3145 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
56 | 33, 35, 27, 55 | gsummptcl 19883 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) |
57 | 1, 3 | ringcl 20151 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
58 | 24, 31, 56, 57 | syl3anc 1370 |
. . 3
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
59 | | eqid 2731 |
. . . 4
⊢ (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) |
60 | 38, 6 | symgbasfi 19294 |
. . . . 5
⊢ (𝑁 ∈ Fin → 𝐺 ∈ Fin) |
61 | 9, 60 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ Fin) |
62 | | ovexd 7447 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ V) |
63 | | fvexd 6906 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (0g‘𝑅) ∈ V) |
64 | 59, 61, 62, 63 | fsuppmptdm 9380 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) finSupp (0g‘𝑅)) |
65 | 1, 2, 3, 5, 8, 23,
58, 64 | gsummulc2 20212 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
66 | | nfcv 2902 |
. . . 4
⊢
Ⅎ𝑞(((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
67 | | fveq2 6891 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑍 ∘ 𝑆)‘𝑞) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
68 | | fveq1 6890 |
. . . . . . . 8
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑞‘𝑥) = ((𝑃 ∘ 𝑝)‘𝑥)) |
69 | 68 | oveq1d 7427 |
. . . . . . 7
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑞‘𝑥)𝑀𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
70 | 69 | mpteq2dv 5250 |
. . . . . 6
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
71 | 70 | oveq2d 7428 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
72 | 67, 71 | oveq12d 7430 |
. . . 4
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
73 | | ringcmn 20177 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
74 | 5, 73 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CMnd) |
75 | | ssidd 4005 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (Base‘𝑅) ⊆ (Base‘𝑅)) |
76 | 5 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑅 ∈ Ring) |
77 | 6, 10 | cofipsgn 21456 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
78 | 9, 77 | sylan 579 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
79 | | simpllr 773 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑁 ∈ Fin) |
80 | | simpr 484 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑞 ∈ 𝐺) |
81 | 6, 10, 20 | zrhpsgnelbas 21457 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
82 | 76, 79, 80, 81 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
83 | 78, 82 | eqeltrd 2832 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅)) |
84 | 34 | ad3antrrr 727 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
85 | 38, 6 | symgfv 19295 |
. . . . . . . . 9
⊢ ((𝑞 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
86 | 85 | adantll 711 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
87 | | simpr 484 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
88 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑀 ∈ 𝐵) |
89 | 88 | ad2antrr 723 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
90 | 36, 1, 37, 86, 87, 89 | matecld 22248 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
91 | 90 | ralrimiva 3145 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
92 | 33, 84, 79, 91 | gsummptcl 19883 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) |
93 | 1, 3 | ringcl 20151 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
94 | 76, 83, 92, 93 | syl3anc 1370 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
95 | | eqid 2731 |
. . . . . . 7
⊢
(+g‘(SymGrp‘𝑁)) =
(+g‘(SymGrp‘𝑁)) |
96 | 38, 6, 95 | symgov 19299 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) = (𝑃 ∘ 𝑝)) |
97 | 38, 6, 95 | symgcl 19300 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) ∈ 𝐺) |
98 | 96, 97 | eqeltrrd 2833 |
. . . . 5
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
99 | 14, 98 | sylan 579 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
100 | 14 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
101 | 6 | symgfcoeu 32679 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
102 | 79, 100, 80, 101 | syl3anc 1370 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
103 | 66, 1, 2, 72, 74, 61, 75, 94, 99, 102 | gsummptf1o 19879 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
104 | | mdetpmtr.d |
. . . . 5
⊢ 𝐷 = (𝑁 maDet 𝑅) |
105 | 104, 36, 37, 6, 20, 10, 3, 32 | mdetleib 22409 |
. . . 4
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
106 | 105 | ad2antrl 725 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
107 | 23 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
108 | 1, 3 | ringass 20154 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅) ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅))) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
109 | 24, 107, 31, 56, 108 | syl13anc 1371 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
110 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
111 | 110, 26 | oveq12d 7430 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
112 | 6, 10 | cofipsgn 21456 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ (𝑃 ∘ 𝑝) ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
113 | 27, 99, 112 | syl2anc 583 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
114 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
115 | 38, 10, 6 | psgnco 21446 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
116 | 27, 114, 28, 115 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
117 | 116 | fveq2d 6895 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))) = (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝)))) |
118 | 20 | zrhrhm 21371 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑍 ∈ (ℤring
RingHom 𝑅)) |
119 | 5, 118 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
120 | 119 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
121 | | 1z 12599 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
122 | | neg1z 12605 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
123 | | prssi 4824 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆
ℤ) |
124 | 121, 122,
123 | mp2an 689 |
. . . . . . . . . . 11
⊢ {1, -1}
⊆ ℤ |
125 | 6, 10 | psgnran 19431 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
126 | 27, 114, 125 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
127 | 124, 126 | sselid 3980 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ ℤ) |
128 | 6, 10 | psgnran 19431 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
129 | 9, 128 | sylan 579 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
130 | 124, 129 | sselid 3980 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ ℤ) |
131 | | zringbas 21313 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
132 | | zringmulr 21317 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
133 | 131, 132,
3 | rhmmul 20384 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (ℤring
RingHom 𝑅) ∧ (𝑆‘𝑃) ∈ ℤ ∧ (𝑆‘𝑝) ∈ ℤ) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
134 | 120, 127,
130, 133 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
135 | 113, 117,
134 | 3eqtrrd 2776 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
136 | 111, 135 | eqtrd 2771 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
137 | 42 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))) |
138 | | simprl 768 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑖 = (𝑝‘𝑥)) |
139 | 138 | fveq2d 6895 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = (𝑃‘(𝑝‘𝑥))) |
140 | | simpllr 773 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑝 ∈ 𝐺) |
141 | 38, 6 | symgbasf 19291 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐺 → 𝑝:𝑁⟶𝑁) |
142 | | ffun 6720 |
. . . . . . . . . . . . . 14
⊢ (𝑝:𝑁⟶𝑁 → Fun 𝑝) |
143 | 140, 141,
142 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → Fun 𝑝) |
144 | | simplr 766 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ 𝑁) |
145 | | fdm 6726 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:𝑁⟶𝑁 → dom 𝑝 = 𝑁) |
146 | 140, 141,
145 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → dom 𝑝 = 𝑁) |
147 | 144, 146 | eleqtrrd 2835 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ dom 𝑝) |
148 | | fvco 6989 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑝 ∧ 𝑥 ∈ dom 𝑝) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
149 | 143, 147,
148 | syl2anc 583 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
150 | 139, 149 | eqtr4d 2774 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = ((𝑃 ∘ 𝑝)‘𝑥)) |
151 | | simprr 770 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑗 = 𝑥) |
152 | 150, 151 | oveq12d 7430 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃‘𝑖)𝑀𝑗) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
153 | | ovexd 7447 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥) ∈ V) |
154 | 137, 152,
40, 41, 153 | ovmpod 7563 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
155 | 154 | mpteq2dva 5248 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
156 | 155 | oveq2d 7428 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
157 | 136, 156 | oveq12d 7430 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
158 | 109, 157 | eqtr3d 2773 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
159 | 158 | mpteq2dva 5248 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))) |
160 | 159 | oveq2d 7428 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
161 | 103, 106,
160 | 3eqtr4d 2781 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
162 | 104, 36, 37, 6, 20, 10, 3, 32 | mdetleib 22409 |
. . . 4
⊢ (𝐸 ∈ 𝐵 → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
163 | 52, 162 | syl 17 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
164 | 163 | oveq2d 7428 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
165 | 65, 161, 164 | 3eqtr4d 2781 |
1
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) |