Step | Hyp | Ref
| Expression |
1 | | mdetrsca.eq |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))) |
2 | 1 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼))) |
3 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼))) |
4 | | mdetrsca.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ∈ 𝑁) |
5 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ 𝑁) |
6 | | snidg 4153 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼}) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼}) |
8 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
9 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
10 | 8, 9 | symgbasf1o 17626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁) |
12 | | f1of 6050 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁) |
14 | 13, 5 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁) |
15 | | ovres 6698 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼))) |
16 | 7, 14, 15 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼))) |
17 | | opelxpi 5072 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) |
18 | 7, 14, 17 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) |
19 | | snfi 7923 |
. . . . . . . . . . . . . . . 16
⊢ {𝐼} ∈ Fin |
20 | | mdetrsca.x |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
21 | | mdetrsca.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = (𝑁 Mat 𝑅) |
22 | | mdetrsca.b |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 = (Base‘𝐴) |
23 | 21, 22 | matrcl 20037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
25 | 24 | simpld 474 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ Fin) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin) |
27 | | xpfi 8116 |
. . . . . . . . . . . . . . . 16
⊢ (({𝐼} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ Fin) |
28 | 19, 26, 27 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ Fin) |
29 | | mdetrsca.y |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ 𝐾) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌 ∈ 𝐾) |
31 | | mdetrsca.z |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
32 | | mdetrsca.k |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐾 = (Base‘𝑅) |
33 | 21, 32, 22 | matbas2i 20047 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ (𝐾 ↑𝑚 (𝑁 × 𝑁))) |
34 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑍 ∈ (𝐾 ↑𝑚 (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
37 | | ffn 5958 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍:(𝑁 × 𝑁)⟶𝐾 → 𝑍 Fn (𝑁 × 𝑁)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍 Fn (𝑁 × 𝑁)) |
39 | 5 | snssd 4281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁) |
40 | | xpss1 5151 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) |
42 | | fnssres 5918 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑍 Fn (𝑁 × 𝑁) ∧ ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) |
43 | 38, 41, 42 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) |
44 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) → ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) = ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉)) |
45 | 28, 30, 43, 44 | ofc1 6818 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) → (((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉))) |
46 | 18, 45 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉))) |
47 | | df-ov 6552 |
. . . . . . . . . . . . 13
⊢ (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) |
48 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) |
49 | 48 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉)) |
50 | 46, 47, 49 | 3eqtr4g 2669 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)))) |
51 | 3, 16, 50 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)))) |
52 | | ovres 6698 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼))) |
53 | 7, 14, 52 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼))) |
54 | 53 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · (𝐼𝑍(𝑝‘𝐼)))) |
55 | 51, 54 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼𝑍(𝑝‘𝐼)))) |
56 | 55 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
57 | | mdetrsca.r |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ CRing) |
58 | | crngring 18381 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
60 | 59 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
61 | 36, 5, 14 | fovrnd 6704 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾) |
62 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
63 | 62, 32 | mgpbas 18318 |
. . . . . . . . . . 11
⊢ 𝐾 =
(Base‘(mulGrp‘𝑅)) |
64 | 62 | crngmgp 18378 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
65 | 57, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd) |
67 | | difssd 3700 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁) |
68 | | ssfi 8065 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝐼}) ⊆ 𝑁) → (𝑁 ∖ {𝐼}) ∈ Fin) |
69 | 26, 67, 68 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin) |
70 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁) |
71 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
72 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁) |
73 | 13 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁) |
74 | 71, 72, 73 | fovrnd 6704 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
75 | 70, 74 | sylan2 490 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
76 | 75 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
77 | 63, 66, 69, 76 | gsummptcl 18189 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾) |
78 | | mdetrsca.t |
. . . . . . . . . . 11
⊢ · =
(.r‘𝑅) |
79 | 32, 78 | ringass 18387 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
80 | 60, 30, 61, 77, 79 | syl13anc 1320 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
81 | 56, 80 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
82 | 62, 78 | mgpplusg 18316 |
. . . . . . . . . 10
⊢ · =
(+g‘(mulGrp‘𝑅)) |
83 | 21, 32, 22 | matbas2i 20047 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (𝐾 ↑𝑚 (𝑁 × 𝑁))) |
84 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ (𝐾 ↑𝑚 (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
85 | 20, 83, 84 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
86 | 85 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
87 | 86, 72, 73 | fovrnd 6704 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ 𝐾) |
88 | | disjdif 3992 |
. . . . . . . . . . 11
⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅ |
89 | 88 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅) |
90 | | undif 4001 |
. . . . . . . . . . . 12
⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁) |
91 | 39, 90 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁) |
92 | 91 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼}))) |
93 | 63, 82, 66, 26, 87, 89, 92 | gsummptfidmsplit 18153 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
94 | | cmnmnd 18031 |
. . . . . . . . . . . 12
⊢
((mulGrp‘𝑅)
∈ CMnd → (mulGrp‘𝑅) ∈ Mnd) |
95 | 66, 94 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd) |
96 | 85 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
97 | 96, 5, 14 | fovrnd 6704 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾) |
98 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼) |
99 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼)) |
100 | 98, 99 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼))) |
101 | 63, 100 | gsumsn 18177 |
. . . . . . . . . . 11
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼))) |
102 | 95, 5, 97, 101 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼))) |
103 | | mdetrsca.ne |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) |
104 | 103 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟))) |
105 | 104 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟))) |
106 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼})) |
107 | 70, 73 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁) |
108 | | ovres 6698 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
109 | 106, 107,
108 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
110 | | ovres 6698 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
111 | 106, 107,
110 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
112 | 105, 109,
111 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
113 | 112 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) |
114 | 113 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) |
115 | 102, 114 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
116 | 93, 115 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
117 | 63, 82, 66, 26, 74, 89, 92 | gsummptfidmsplit 18153 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
118 | 98, 99 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼))) |
119 | 63, 118 | gsumsn 18177 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼))) |
120 | 95, 5, 61, 119 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼))) |
121 | 120 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
122 | 117, 121 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
123 | 122 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
124 | 81, 116, 123 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
125 | 124 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
126 | 57 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ CRing) |
127 | | zrhpsgnmhm 19749 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))
∈ ((SymGrp‘𝑁)
MndHom (mulGrp‘𝑅))) |
128 | 59, 25, 127 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
129 | 9, 63 | mhmf 17163 |
. . . . . . . . . . 11
⊢
(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾) |
130 | 128, 129 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾) |
131 | 130 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾) |
132 | 32, 78 | crngcom 18385 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝))) |
133 | 126, 131,
30, 132 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝))) |
134 | 133 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
135 | 74 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
136 | 63, 66, 26, 135 | gsummptcl 18189 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾) |
137 | 32, 78 | ringass 18387 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
138 | 60, 131, 30, 136, 137 | syl13anc 1320 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
139 | 32, 78 | ringass 18387 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
140 | 60, 30, 131, 136, 139 | syl13anc 1320 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
141 | 134, 138,
140 | 3eqtr3d 2652 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
142 | 125, 141 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
143 | 142 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
144 | 143 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
145 | | eqid 2610 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
146 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
147 | 8, 9 | symgbasfi 17629 |
. . . . 5
⊢ (𝑁 ∈ Fin →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
148 | 25, 147 | syl 17 |
. . . 4
⊢ (𝜑 →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
149 | 32, 78 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ 𝐾) |
150 | 60, 131, 136, 149 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ 𝐾) |
151 | | eqid 2610 |
. . . . 5
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
152 | | ovex 6577 |
. . . . . 6
⊢
((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V |
153 | 152 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V) |
154 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
155 | 154 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
156 | 151, 148,
153, 155 | fsuppmptdm 8169 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) finSupp (0g‘𝑅)) |
157 | 32, 145, 146, 78, 59, 148, 29, 150, 156 | gsummulc2 18430 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
158 | 144, 157 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
159 | | mdetrsca.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
160 | | eqid 2610 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
161 | | eqid 2610 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
162 | 159, 21, 22, 9, 160, 161, 78, 62 | mdetleib2 20213 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
163 | 57, 20, 162 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
164 | 159, 21, 22, 9, 160, 161, 78, 62 | mdetleib2 20213 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
165 | 57, 31, 164 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
166 | 165 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝑌 · (𝐷‘𝑍)) = (𝑌 · (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
167 | 158, 163,
166 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍))) |