| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . . 6
⊢
(Base‘(SymGrp‘𝑁)) ∈ V |
| 2 | | ovex 7464 |
. . . . . . 7
⊢
((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ V |
| 3 | | eqid 2737 |
. . . . . . 7
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) |
| 4 | 2, 3 | fnmpti 6711 |
. . . . . 6
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁)) |
| 5 | | ovex 7464 |
. . . . . . 7
⊢
((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V |
| 6 | | eqid 2737 |
. . . . . . 7
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 7 | 5, 6 | fnmpti 6711 |
. . . . . 6
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁)) |
| 8 | | ofmpteq 7720 |
. . . . . 6
⊢
(((Base‘(SymGrp‘𝑁)) ∈ V ∧ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁)) ∧ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁))) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) +
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
| 9 | 1, 4, 7, 8 | mp3an 1463 |
. . . . 5
⊢ ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) +
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 10 | | mdetrlin.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 11 | | crngring 20242 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 13 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
| 14 | | mdetrlin.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 15 | | mdetrlin.a |
. . . . . . . . . . . . . 14
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 16 | | mdetrlin.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝐴) |
| 17 | 15, 16 | matrcl 22416 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 18 | 14, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 19 | 18 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 20 | | zrhpsgnmhm 21602 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))
∈ ((SymGrp‘𝑁)
MndHom (mulGrp‘𝑅))) |
| 21 | 12, 19, 20 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅))) |
| 22 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
| 23 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 24 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 25 | 23, 24 | mgpbas 20142 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 26 | 22, 25 | mhmf 18802 |
. . . . . . . . . 10
⊢
(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅)) |
| 27 | 21, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅)) |
| 28 | 27 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅)) |
| 29 | 23 | crngmgp 20238 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
| 30 | 10, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
| 31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd) |
| 32 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin) |
| 33 | 15, 24, 16 | matbas2i 22428 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 34 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 35 | 14, 33, 34 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 36 | 35 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 37 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
| 39 | 38, 22 | symgbasf 19393 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
(Base‘(SymGrp‘𝑁)) → 𝑝:𝑁⟶𝑁) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁) |
| 41 | 40 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁) |
| 42 | 36, 37, 41 | fovcdmd 7605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑌(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 43 | 42 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑌(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 44 | 25, 31, 32, 43 | gsummptcl 19985 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅)) |
| 45 | | mdetrlin.z |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 46 | 15, 24, 16 | matbas2i 22428 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 47 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 49 | 48 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 50 | 49, 37, 41 | fovcdmd 7605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 51 | 50 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 52 | 25, 31, 32, 51 | gsummptcl 19985 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅)) |
| 53 | | mdetrlin.p |
. . . . . . . . 9
⊢ + =
(+g‘𝑅) |
| 54 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 55 | 24, 53, 54 | ringdi 20258 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) +
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 56 | 13, 28, 44, 52, 55 | syl13anc 1374 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) +
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) |
| 57 | | cmnmnd 19815 |
. . . . . . . . . . . . 13
⊢
((mulGrp‘𝑅)
∈ CMnd → (mulGrp‘𝑅) ∈ Mnd) |
| 58 | 31, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd) |
| 59 | | mdetrlin.i |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ 𝑁) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ 𝑁) |
| 61 | 35 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 62 | 40, 60 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁) |
| 63 | 61, 60, 62 | fovcdmd 7605 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑌(𝑝‘𝐼)) ∈ (Base‘𝑅)) |
| 64 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼) |
| 65 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼)) |
| 66 | 64, 65 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → (𝑟𝑌(𝑝‘𝑟)) = (𝐼𝑌(𝑝‘𝐼))) |
| 67 | 25, 66 | gsumsn 19972 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑌(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) = (𝐼𝑌(𝑝‘𝐼))) |
| 68 | 58, 60, 63, 67 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) = (𝐼𝑌(𝑝‘𝐼))) |
| 69 | 68, 63 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅)) |
| 70 | 48 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 71 | 70, 60, 62 | fovcdmd 7605 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ (Base‘𝑅)) |
| 72 | 64, 65 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼))) |
| 73 | 25, 72 | gsumsn 19972 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼))) |
| 74 | 58, 60, 71, 73 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼))) |
| 75 | 74, 71 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅)) |
| 76 | | difssd 4137 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁) |
| 77 | 32, 76 | ssfid 9301 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin) |
| 78 | | eldifi 4131 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁) |
| 79 | | mdetrlin.x |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 80 | 15, 24, 16 | matbas2i 22428 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 81 | | elmapi 8889 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 82 | 79, 80, 81 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 83 | 82 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 84 | 83, 37, 41 | fovcdmd 7605 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 85 | 78, 84 | sylan2 593 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 86 | 85 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅)) |
| 87 | 25, 31, 77, 86 | gsummptcl 19985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) ∈ (Base‘𝑅)) |
| 88 | 24, 53, 54 | ringdir 20259 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
(((mulGrp‘𝑅)
Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) ∈ (Base‘𝑅))) → ((((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))) |
| 89 | 13, 69, 75, 87, 88 | syl13anc 1374 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((mulGrp‘𝑅)
Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))) |
| 90 | 23, 54 | mgpplusg 20141 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 91 | | disjdif 4472 |
. . . . . . . . . . . 12
⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅ |
| 92 | 91 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅) |
| 93 | 59 | snssd 4809 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝐼} ⊆ 𝑁) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁) |
| 95 | | undif 4482 |
. . . . . . . . . . . . 13
⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁) |
| 96 | 94, 95 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁) |
| 97 | 96 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼}))) |
| 98 | 25, 90, 31, 32, 84, 92, 97 | gsummptfidmsplit 19948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 99 | | mdetrlin.eq |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))) |
| 100 | 99 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))) |
| 101 | 100 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼))) |
| 102 | | xpss1 5704 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) |
| 103 | 94, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) |
| 104 | 61, 103 | fssresd 6775 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅)) |
| 105 | 104 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) |
| 106 | 70, 103 | fssresd 6775 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅)) |
| 107 | 106 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) |
| 108 | | snex 5436 |
. . . . . . . . . . . . . . . . 17
⊢ {𝐼} ∈ V |
| 109 | | xpexg 7770 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐼} ∈ V ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ V) |
| 110 | 108, 32, 109 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ V) |
| 111 | | snidg 4660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼}) |
| 112 | 60, 111 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼}) |
| 113 | 112, 62 | opelxpd 5724 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁)) |
| 114 | | fnfvof 7714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁) ∧ (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) ∧ (({𝐼} × 𝑁) ∈ V ∧ 〈𝐼, (𝑝‘𝐼)〉 ∈ ({𝐼} × 𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) = (((𝑌 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) + ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉))) |
| 115 | 105, 107,
110, 113, 114 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) = (((𝑌 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) + ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉))) |
| 116 | | df-ov 7434 |
. . . . . . . . . . . . . . 15
⊢ (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘〈𝐼, (𝑝‘𝐼)〉) |
| 117 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑌 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) |
| 118 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) |
| 119 | 117, 118 | oveq12i 7443 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (((𝑌 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉) + ((𝑍 ↾ ({𝐼} × 𝑁))‘〈𝐼, (𝑝‘𝐼)〉)) |
| 120 | 115, 116,
119 | 3eqtr4g 2802 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)))) |
| 121 | 101, 120 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)))) |
| 122 | | ovres 7599 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼))) |
| 123 | 112, 62, 122 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼))) |
| 124 | | ovres 7599 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑌(𝑝‘𝐼))) |
| 125 | 112, 62, 124 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑌(𝑝‘𝐼))) |
| 126 | | ovres 7599 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼))) |
| 127 | 112, 62, 126 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼))) |
| 128 | 125, 127 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼)))) |
| 129 | 121, 123,
128 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼)))) |
| 130 | 82 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
| 131 | 130, 60, 62 | fovcdmd 7605 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ (Base‘𝑅)) |
| 132 | 64, 65 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼))) |
| 133 | 25, 132 | gsumsn 19972 |
. . . . . . . . . . . . 13
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼))) |
| 134 | 58, 60, 131, 133 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼))) |
| 135 | 68, 74 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼)))) |
| 136 | 129, 134,
135 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 137 | 136 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 138 | 98, 137 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 139 | 25, 90, 31, 32, 42, 92, 97 | gsummptfidmsplit 19948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟)))))) |
| 140 | | mdetrlin.ne1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) |
| 141 | 140 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) |
| 142 | 141 | oveqd 7448 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟))) |
| 143 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼})) |
| 144 | 78, 41 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁) |
| 145 | | ovres 7599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
| 146 | 143, 144,
145 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
| 147 | | ovres 7599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑌(𝑝‘𝑟))) |
| 148 | 143, 144,
147 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑌(𝑝‘𝑟))) |
| 149 | 142, 146,
148 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑌(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
| 150 | 149 | mpteq2dva 5242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) |
| 151 | 150 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) |
| 152 | 151 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 153 | 139, 152 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 154 | 25, 90, 31, 32, 50, 92, 97 | gsummptfidmsplit 19948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))) |
| 155 | | mdetrlin.ne2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) |
| 156 | 155 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) |
| 157 | 156 | oveqd 7448 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟))) |
| 158 | | ovres 7599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
| 159 | 143, 144,
158 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟))) |
| 160 | 157, 146,
159 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟))) |
| 161 | 160 | mpteq2dva 5242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) |
| 162 | 161 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) |
| 163 | 162 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 164 | 154, 163 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 165 | 153, 164 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg
(𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))) |
| 166 | 89, 138, 165 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) |
| 167 | 166 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg
(𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 168 | 56, 167 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) +
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))) |
| 169 | 168 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
(((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) +
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) |
| 170 | 9, 169 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) |
| 171 | 170 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
| 172 | | ringcmn 20279 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 173 | 10, 11, 172 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 174 | 38, 22 | symgbasfi 19396 |
. . . . 5
⊢ (𝑁 ∈ Fin →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
| 175 | 19, 174 | syl 17 |
. . . 4
⊢ (𝜑 →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
| 176 | 24, 54 | ringcl 20247 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ (Base‘𝑅)) |
| 177 | 13, 28, 44, 176 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ (Base‘𝑅)) |
| 178 | 24, 54 | ringcl 20247 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ (Base‘𝑅)) |
| 179 | 13, 28, 52, 178 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) →
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ (Base‘𝑅)) |
| 180 | 24, 53, 173, 175, 177, 179, 3, 6 | gsummptfidmadd2 19944 |
. . 3
⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = ((𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 181 | 171, 180 | eqtr3d 2779 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = ((𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 182 | | mdetrlin.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
| 183 | | eqid 2737 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
| 184 | | eqid 2737 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
| 185 | 182, 15, 16, 22, 183, 184, 54, 23 | mdetleib2 22594 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
| 186 | 10, 79, 185 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))) |
| 187 | 182, 15, 16, 22, 183, 184, 54, 23 | mdetleib2 22594 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∈ 𝐵) → (𝐷‘𝑌) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))))) |
| 188 | 10, 14, 187 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐷‘𝑌) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))))) |
| 189 | 182, 15, 16, 22, 183, 184, 54, 23 | mdetleib2 22594 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
| 190 | 10, 45, 189 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) |
| 191 | 188, 190 | oveq12d 7449 |
. 2
⊢ (𝜑 → ((𝐷‘𝑌) + (𝐷‘𝑍)) = ((𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))) |
| 192 | 181, 186,
191 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐷‘𝑋) = ((𝐷‘𝑌) + (𝐷‘𝑍))) |