Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2738 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | eqid 2738 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | mdetpmtr.t |
. . 3
⊢ · =
(.r‘𝑅) |
5 | | crngring 19795 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
6 | 5 | ad2antrr 723 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ Ring) |
7 | | mdetpmtr.g |
. . . . 5
⊢ 𝐺 =
(Base‘(SymGrp‘𝑁)) |
8 | 7 | fvexi 6788 |
. . . 4
⊢ 𝐺 ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ V) |
10 | | simplr 766 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑁 ∈ Fin) |
11 | | mdetpmtr.s |
. . . . . . 7
⊢ 𝑆 = (pmSgn‘𝑁) |
12 | 11, 7 | psgndmfi 31365 |
. . . . . 6
⊢ (𝑁 ∈ Fin → 𝑆 Fn 𝐺) |
13 | | fnfun 6533 |
. . . . . 6
⊢ (𝑆 Fn 𝐺 → Fun 𝑆) |
14 | 10, 12, 13 | 3syl 18 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → Fun 𝑆) |
15 | | simprr 770 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ 𝐺) |
16 | | fndm 6536 |
. . . . . . 7
⊢ (𝑆 Fn 𝐺 → dom 𝑆 = 𝐺) |
17 | 10, 12, 16 | 3syl 18 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → dom 𝑆 = 𝐺) |
18 | 15, 17 | eleqtrrd 2842 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ dom 𝑆) |
19 | | fvco 6866 |
. . . . 5
⊢ ((Fun
𝑆 ∧ 𝑃 ∈ dom 𝑆) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
20 | 14, 18, 19 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
21 | | mdetpmtr.z |
. . . . . 6
⊢ 𝑍 = (ℤRHom‘𝑅) |
22 | 7, 11, 21 | zrhpsgnelbas 20799 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
23 | 6, 10, 15, 22 | syl3anc 1370 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅)) |
24 | 20, 23 | eqeltrd 2839 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
25 | 6 | adantr 481 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑅 ∈ Ring) |
26 | 7, 11 | cofipsgn 20798 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
27 | 10, 26 | sylan 580 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝))) |
28 | | simpllr 773 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑁 ∈ Fin) |
29 | | simpr 485 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑝 ∈ 𝐺) |
30 | 7, 11, 21 | zrhpsgnelbas 20799 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
31 | 25, 28, 29, 30 | syl3anc 1370 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅)) |
32 | 27, 31 | eqeltrd 2839 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅)) |
33 | | eqid 2738 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
34 | 33, 1 | mgpbas 19726 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
35 | 33 | crngmgp 19791 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
36 | 35 | ad3antrrr 727 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
37 | | mdetpmtr.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
38 | | mdetpmtr.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
39 | | eqid 2738 |
. . . . . . . . 9
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
40 | 39, 7 | symgfv 18987 |
. . . . . . . 8
⊢ ((𝑝 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
41 | 40 | adantll 711 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁) |
42 | | simpr 485 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
43 | | mdetpmtr1.e |
. . . . . . . . 9
⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) |
44 | | simpll 764 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CRing) |
45 | | simp1rr 1238 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ 𝐺) |
46 | | simp2 1136 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
47 | 39, 7 | symgfv 18987 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
48 | 45, 46, 47 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
49 | | simp3 1137 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
50 | | simp1rl 1237 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
51 | 37, 1, 38, 48, 49, 50 | matecld 21575 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑃‘𝑖)𝑀𝑗) ∈ (Base‘𝑅)) |
52 | 37, 1, 38, 10, 44, 51 | matbas2d 21572 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ∈ 𝐵) |
53 | 43, 52 | eqeltrid 2843 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐸 ∈ 𝐵) |
54 | 53 | ad2antrr 723 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 ∈ 𝐵) |
55 | 37, 1, 38, 41, 42, 54 | matecld 21575 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
56 | 55 | ralrimiva 3103 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅)) |
57 | 34, 36, 28, 56 | gsummptcl 19568 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) |
58 | 1, 4 | ringcl 19800 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
59 | 25, 32, 57, 58 | syl3anc 1370 |
. . 3
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅)) |
60 | | eqid 2738 |
. . . 4
⊢ (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) |
61 | 39, 7 | symgbasfi 18986 |
. . . . 5
⊢ (𝑁 ∈ Fin → 𝐺 ∈ Fin) |
62 | 10, 61 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ Fin) |
63 | | ovexd 7310 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ V) |
64 | | fvexd 6789 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (0g‘𝑅) ∈ V) |
65 | 60, 62, 63, 64 | fsuppmptdm 9139 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) finSupp (0g‘𝑅)) |
66 | 1, 2, 3, 4, 6, 9, 24, 59, 65 | gsummulc2 19846 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
67 | | nfcv 2907 |
. . . 4
⊢
Ⅎ𝑞(((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
68 | | fveq2 6774 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑍 ∘ 𝑆)‘𝑞) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
69 | | fveq1 6773 |
. . . . . . . 8
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑞‘𝑥) = ((𝑃 ∘ 𝑝)‘𝑥)) |
70 | 69 | oveq1d 7290 |
. . . . . . 7
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑞‘𝑥)𝑀𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
71 | 70 | mpteq2dv 5176 |
. . . . . 6
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
72 | 71 | oveq2d 7291 |
. . . . 5
⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
73 | 68, 72 | oveq12d 7293 |
. . . 4
⊢ (𝑞 = (𝑃 ∘ 𝑝) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
74 | | ringcmn 19820 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
75 | 6, 74 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CMnd) |
76 | | ssidd 3944 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (Base‘𝑅) ⊆ (Base‘𝑅)) |
77 | 6 | adantr 481 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑅 ∈ Ring) |
78 | 7, 11 | cofipsgn 20798 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
79 | 10, 78 | sylan 580 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞))) |
80 | | simpllr 773 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑁 ∈ Fin) |
81 | | simpr 485 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑞 ∈ 𝐺) |
82 | 7, 11, 21 | zrhpsgnelbas 20799 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
83 | 77, 80, 81, 82 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅)) |
84 | 79, 83 | eqeltrd 2839 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅)) |
85 | 35 | ad3antrrr 727 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd) |
86 | 39, 7 | symgfv 18987 |
. . . . . . . . 9
⊢ ((𝑞 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
87 | 86 | adantll 711 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁) |
88 | | simpr 485 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
89 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑀 ∈ 𝐵) |
90 | 89 | ad2antrr 723 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
91 | 37, 1, 38, 87, 88, 90 | matecld 21575 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
92 | 91 | ralrimiva 3103 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅)) |
93 | 34, 85, 80, 92 | gsummptcl 19568 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) |
94 | 1, 4 | ringcl 19800 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
95 | 77, 84, 93, 94 | syl3anc 1370 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅)) |
96 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘(SymGrp‘𝑁)) =
(+g‘(SymGrp‘𝑁)) |
97 | 39, 7, 96 | symgov 18991 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) = (𝑃 ∘ 𝑝)) |
98 | 39, 7, 96 | symgcl 18992 |
. . . . . 6
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) ∈ 𝐺) |
99 | 97, 98 | eqeltrrd 2840 |
. . . . 5
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
100 | 15, 99 | sylan 580 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺) |
101 | 15 | adantr 481 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
102 | 7 | symgfcoeu 31351 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
103 | 80, 101, 81, 102 | syl3anc 1370 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝)) |
104 | 67, 1, 2, 73, 75, 62, 76, 95, 100, 103 | gsummptf1o 19564 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
105 | | mdetpmtr.d |
. . . . 5
⊢ 𝐷 = (𝑁 maDet 𝑅) |
106 | 105, 37, 38, 7, 21, 11, 4, 33 | mdetleib 21736 |
. . . 4
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
107 | 106 | ad2antrl 725 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))))))) |
108 | 24 | adantr 481 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
109 | 1, 4 | ringass 19803 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅) ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅))) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
110 | 25, 108, 32, 57, 109 | syl13anc 1371 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) |
111 | 20 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
112 | 111, 27 | oveq12d 7293 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
113 | 7, 11 | cofipsgn 20798 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ (𝑃 ∘ 𝑝) ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
114 | 28, 100, 113 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝)))) |
115 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
116 | 39, 11, 7 | psgnco 20788 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
117 | 28, 115, 29, 116 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝))) |
118 | 117 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))) = (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝)))) |
119 | 21 | zrhrhm 20713 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑍 ∈ (ℤring
RingHom 𝑅)) |
120 | 6, 119 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
121 | 120 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑍 ∈ (ℤring RingHom
𝑅)) |
122 | | 1z 12350 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
123 | | neg1z 12356 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
124 | | prssi 4754 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆
ℤ) |
125 | 122, 123,
124 | mp2an 689 |
. . . . . . . . . . 11
⊢ {1, -1}
⊆ ℤ |
126 | 7, 11 | psgnran 19123 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
127 | 28, 115, 126 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
128 | 125, 127 | sselid 3919 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ ℤ) |
129 | 7, 11 | psgnran 19123 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
130 | 10, 129 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1}) |
131 | 125, 130 | sselid 3919 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ ℤ) |
132 | | zringbas 20676 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
133 | | zringmulr 20679 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
134 | 132, 133,
4 | rhmmul 19971 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (ℤring
RingHom 𝑅) ∧ (𝑆‘𝑃) ∈ ℤ ∧ (𝑆‘𝑝) ∈ ℤ) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
135 | 121, 128,
131, 134 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝)))) |
136 | 114, 118,
135 | 3eqtrrd 2783 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
137 | 112, 136 | eqtrd 2778 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝))) |
138 | 43 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))) |
139 | | simprl 768 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑖 = (𝑝‘𝑥)) |
140 | 139 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = (𝑃‘(𝑝‘𝑥))) |
141 | | simpllr 773 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑝 ∈ 𝐺) |
142 | 39, 7 | symgbasf 18983 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐺 → 𝑝:𝑁⟶𝑁) |
143 | | ffun 6603 |
. . . . . . . . . . . . . 14
⊢ (𝑝:𝑁⟶𝑁 → Fun 𝑝) |
144 | 141, 142,
143 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → Fun 𝑝) |
145 | | simplr 766 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ 𝑁) |
146 | | fdm 6609 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:𝑁⟶𝑁 → dom 𝑝 = 𝑁) |
147 | 141, 142,
146 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → dom 𝑝 = 𝑁) |
148 | 145, 147 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ dom 𝑝) |
149 | | fvco 6866 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑝 ∧ 𝑥 ∈ dom 𝑝) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
150 | 144, 148,
149 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥))) |
151 | 140, 150 | eqtr4d 2781 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = ((𝑃 ∘ 𝑝)‘𝑥)) |
152 | | simprr 770 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑗 = 𝑥) |
153 | 151, 152 | oveq12d 7293 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃‘𝑖)𝑀𝑗) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
154 | | ovexd 7310 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥) ∈ V) |
155 | 138, 153,
41, 42, 154 | ovmpod 7425 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin) ∧
(𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)) |
156 | 155 | mpteq2dva 5174 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))) |
157 | 156 | oveq2d 7291 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))) |
158 | 137, 157 | oveq12d 7293 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
159 | 110, 158 | eqtr3d 2780 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))) |
160 | 159 | mpteq2dva 5174 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))) |
161 | 160 | oveq2d 7291 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))) |
162 | 104, 107,
161 | 3eqtr4d 2788 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
163 | 105, 37, 38, 7, 21, 11, 4, 33 | mdetleib 21736 |
. . . 4
⊢ (𝐸 ∈ 𝐵 → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
164 | 53, 163 | syl 17 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) |
165 | 164 | oveq2d 7291 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))) |
166 | 66, 162, 165 | 3eqtr4d 2788 |
1
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) |