| Step | Hyp | Ref
| Expression |
| 1 | | mdetrsca.eq |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))) |
| 2 | 1 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼))) |
| 3 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼))) |
| 4 | | mdetrsca.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ∈ 𝑁) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ 𝑁) |
| 6 | | snidg 4660 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼}) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼}) |
| 8 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
| 9 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
| 10 | 8, 9 | symgbasf1o 19392 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁) |
| 11 | 10 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁) |
| 12 | | f1of 6848 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁) |
| 14 | 13, 5 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁) |
| 15 | | ovres 7599 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼))) |
| 16 | 7, 14, 15 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼))) |
| 17 | 7, 14 | opelxpd 5724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) |
| 18 | | snfi 9083 |
. . . . . . . . . . . . . . . 16
⊢ {𝐼} ∈ Fin |
| 19 | | mdetrsca.x |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 20 | | mdetrsca.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 21 | | mdetrsca.b |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 = (Base‘𝐴) |
| 22 | 20, 21 | matrcl 22416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 24 | 23 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin) |
| 26 | | xpfi 9358 |
. . . . . . . . . . . . . . . 16
⊢ (({𝐼} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ Fin) |
| 27 | 18, 25, 26 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ Fin) |
| 28 | | mdetrsca.y |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ 𝐾) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌 ∈ 𝐾) |
| 30 | | mdetrsca.z |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 31 | | mdetrsca.k |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐾 = (Base‘𝑅) |
| 32 | 20, 31, 21 | matbas2i 22428 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ (𝐾 ↑m (𝑁 × 𝑁))) |
| 33 | | elmapi 8889 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑍 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
| 34 | 30, 32, 33 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
| 36 | 35 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍 Fn (𝑁 × 𝑁)) |
| 37 | 5 | snssd 4809 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁) |
| 38 | | xpss1 5704 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) |
| 40 | 36, 39 | fnssresd 6692 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) |
| 41 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) → ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) = ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉)) |
| 42 | 27, 29, 40, 41 | ofc1 7725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) → (((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉))) |
| 43 | 17, 42 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉))) |
| 44 | | df-ov 7434 |
. . . . . . . . . . . . 13
⊢ (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) |
| 45 | | df-ov 7434 |
. . . . . . . . . . . . . 14
⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) |
| 46 | 45 | oveq2i 7442 |
. . . . . . . . . . . . 13
⊢ (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉)) |
| 47 | 43, 44, 46 | 3eqtr4g 2802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)))) |
| 48 | 3, 16, 47 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)))) |
| 49 | | ovres 7599 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼))) |
| 50 | 7, 14, 49 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼))) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · (𝐼𝑍(𝑝‘𝐼)))) |
| 52 | 48, 51 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼𝑍(𝑝‘𝐼)))) |
| 53 | 52 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 54 | | mdetrsca.r |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 55 | 54 | crngringd 20243 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 56 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
| 57 | 35, 5, 14 | fovcdmd 7605 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾) |
| 58 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 59 | 58, 31 | mgpbas 20142 |
. . . . . . . . . . 11
⊢ 𝐾 =
(Base‘(mulGrp‘𝑅)) |
| 60 | 58 | crngmgp 20238 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
| 61 | 54, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd) |
| 63 | | difssd 4137 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁) |
| 64 | 25, 63 | ssfid 9301 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin) |
| 65 | | eldifi 4131 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁) |
| 66 | 34 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐾) |
| 67 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁) |
| 68 | 13 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁) |
| 69 | 66, 67, 68 | fovcdmd 7605 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
| 70 | 65, 69 | sylan2 593 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
| 71 | 70 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
| 72 | 59, 62, 64, 71 | gsummptcl 19985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾) |
| 73 | | mdetrsca.t |
. . . . . . . . . . 11
⊢ · =
(.r‘𝑅) |
| 74 | 31, 73 | ringass 20250 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 75 | 56, 29, 57, 72, 74 | syl13anc 1374 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 76 | 53, 75 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 77 | 58, 73 | mgpplusg 20141 |
. . . . . . . . . 10
⊢ · =
(+g‘(mulGrp‘𝑅)) |
| 78 | 20, 31, 21 | matbas2i 22428 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (𝐾 ↑m (𝑁 × 𝑁))) |
| 79 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
| 80 | 19, 78, 79 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
| 81 | 80 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
| 82 | 81, 67, 68 | fovcdmd 7605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ 𝐾) |
| 83 | | disjdif 4472 |
. . . . . . . . . . 11
⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅ |
| 84 | 83 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅) |
| 85 | | undif 4482 |
. . . . . . . . . . . 12
⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁) |
| 86 | 37, 85 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁) |
| 87 | 86 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼}))) |
| 88 | 59, 77, 62, 25, 82, 84, 87 | gsummptfidmsplit 19948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 89 | 62 | cmnmndd 19822 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd) |
| 90 | 80 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶𝐾) |
| 91 | 90, 5, 14 | fovcdmd 7605 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾) |
| 92 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼) |
| 93 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼)) |
| 94 | 92, 93 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼))) |
| 95 | 59, 94 | gsumsn 19972 |
. . . . . . . . . . 11
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼))) |
| 96 | 89, 5, 91, 95 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼))) |
| 97 | | mdetrsca.ne |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) |
| 98 | 97 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟))) |
| 99 | 98 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟))) |
| 100 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼})) |
| 101 | 65, 68 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁) |
| 102 | | ovres 7599 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
| 103 | 100, 101,
102 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
| 104 | | ovres 7599 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
| 105 | 100, 101,
104 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
| 106 | 99, 103, 105 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
| 107 | 106 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) |
| 108 | 107 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) |
| 109 | 96, 108 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 110 | 88, 109 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((𝐼𝑋(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 111 | 59, 77, 62, 25, 69, 84, 87 | gsummptfidmsplit 19948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 112 | 92, 93 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼))) |
| 113 | 59, 112 | gsumsn 19972 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼))) |
| 114 | 89, 5, 57, 113 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼))) |
| 115 | 114 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 116 | 111, 115 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 117 | 116 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 118 | 76, 110, 117 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 119 | 118 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 120 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ CRing) |
| 121 | | zrhpsgnmhm 21602 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))
∈ ((SymGrp‘𝑁)
MndHom (mulGrp‘𝑅))) |
| 122 | 55, 24, 121 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
| 123 | 9, 59 | mhmf 18802 |
. . . . . . . . . . 11
⊢
(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾) |
| 124 | 122, 123 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾) |
| 125 | 124 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾) |
| 126 | 31, 73 | crngcom 20248 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝))) |
| 127 | 120, 125,
29, 126 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝))) |
| 128 | 127 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 129 | 69 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾) |
| 130 | 59, 62, 25, 129 | gsummptcl 19985 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾) |
| 131 | 31, 73 | ringass 20250 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 132 | 56, 125, 29, 130, 131 | syl13anc 1374 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 133 | 31, 73 | ringass 20250 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 134 | 56, 29, 125, 130, 133 | syl13anc 1374 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 ·
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 135 | 128, 132,
134 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 136 | 119, 135 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 137 | 136 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
| 138 | 137 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 139 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 140 | 8, 9 | symgbasfi 19396 |
. . . . 5
⊢ (𝑁 ∈ Fin →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
| 141 | 24, 140 | syl 17 |
. . . 4
⊢ (𝜑 →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
| 142 | 31, 73, 56, 125, 130 | ringcld 20257 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ 𝐾) |
| 143 | | eqid 2737 |
. . . . 5
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 144 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V) |
| 145 | | fvexd 6921 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
| 146 | 143, 141,
144, 145 | fsuppmptdm 9416 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) finSupp (0g‘𝑅)) |
| 147 | 31, 139, 73, 55, 141, 28, 142, 146 | gsummulc2 20314 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ (𝑌 ·
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 148 | 138, 147 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 149 | | mdetrsca.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
| 150 | | eqid 2737 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
| 151 | | eqid 2737 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
| 152 | 149, 20, 21, 9, 150, 151, 73, 58 | mdetleib2 22594 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
| 153 | 54, 19, 152 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
| 154 | 149, 20, 21, 9, 150, 151, 73, 58 | mdetleib2 22594 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
| 155 | 54, 30, 154 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
| 156 | 155 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝑌 · (𝐷‘𝑍)) = (𝑌 · (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ·
((mulGrp‘𝑅)
Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 157 | 148, 153,
156 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍))) |