MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetrsca Structured version   Visualization version   GIF version

Theorem mdetrsca 20700
Description: The determinant function is homogeneous for each row: The matrices X and Z are identical except for the I's row, and the I's row of the matrix X is the componentwise product of the I's row of the matrix Z and the scalar Y. In this case the determinant of X is the determinant of Z multiplied by Y. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
Hypotheses
Ref Expression
mdetrsca.d 𝐷 = (𝑁 maDet 𝑅)
mdetrsca.a 𝐴 = (𝑁 Mat 𝑅)
mdetrsca.b 𝐵 = (Base‘𝐴)
mdetrsca.k 𝐾 = (Base‘𝑅)
mdetrsca.t · = (.r𝑅)
mdetrsca.r (𝜑𝑅 ∈ CRing)
mdetrsca.x (𝜑𝑋𝐵)
mdetrsca.y (𝜑𝑌𝐾)
mdetrsca.z (𝜑𝑍𝐵)
mdetrsca.i (𝜑𝐼𝑁)
mdetrsca.eq (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁))))
mdetrsca.ne (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
Assertion
Ref Expression
mdetrsca (𝜑 → (𝐷𝑋) = (𝑌 · (𝐷𝑍)))

Proof of Theorem mdetrsca
Dummy variables 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetrsca.eq . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁))))
21oveqd 6863 . . . . . . . . . . . . 13 (𝜑 → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)))
32adantr 472 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)))
4 mdetrsca.i . . . . . . . . . . . . . . 15 (𝜑𝐼𝑁)
54adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼𝑁)
6 snidg 4366 . . . . . . . . . . . . . 14 (𝐼𝑁𝐼 ∈ {𝐼})
75, 6syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼})
8 eqid 2765 . . . . . . . . . . . . . . . . 17 (SymGrp‘𝑁) = (SymGrp‘𝑁)
9 eqid 2765 . . . . . . . . . . . . . . . . 17 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
108, 9symgbasf1o 18080 . . . . . . . . . . . . . . . 16 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁1-1-onto𝑁)
1110adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁1-1-onto𝑁)
12 f1of 6324 . . . . . . . . . . . . . . 15 (𝑝:𝑁1-1-onto𝑁𝑝:𝑁𝑁)
1311, 12syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁𝑁)
1413, 5ffvelrnd 6554 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝𝐼) ∈ 𝑁)
15 ovres 7002 . . . . . . . . . . . . 13 ((𝐼 ∈ {𝐼} ∧ (𝑝𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑋(𝑝𝐼)))
167, 14, 15syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑋(𝑝𝐼)))
17 opelxpi 5316 . . . . . . . . . . . . . . 15 ((𝐼 ∈ {𝐼} ∧ (𝑝𝐼) ∈ 𝑁) → ⟨𝐼, (𝑝𝐼)⟩ ∈ ({𝐼} × 𝑁))
187, 14, 17syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ⟨𝐼, (𝑝𝐼)⟩ ∈ ({𝐼} × 𝑁))
19 snfi 8249 . . . . . . . . . . . . . . . 16 {𝐼} ∈ Fin
20 mdetrsca.x . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋𝐵)
21 mdetrsca.a . . . . . . . . . . . . . . . . . . . 20 𝐴 = (𝑁 Mat 𝑅)
22 mdetrsca.b . . . . . . . . . . . . . . . . . . . 20 𝐵 = (Base‘𝐴)
2321, 22matrcl 20508 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
2420, 23syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
2524simpld 488 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ Fin)
2625adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
27 xpfi 8442 . . . . . . . . . . . . . . . 16 (({𝐼} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ Fin)
2819, 26, 27sylancr 581 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ Fin)
29 mdetrsca.y . . . . . . . . . . . . . . . 16 (𝜑𝑌𝐾)
3029adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌𝐾)
31 mdetrsca.z . . . . . . . . . . . . . . . . . . 19 (𝜑𝑍𝐵)
32 mdetrsca.k . . . . . . . . . . . . . . . . . . . 20 𝐾 = (Base‘𝑅)
3321, 32, 22matbas2i 20518 . . . . . . . . . . . . . . . . . . 19 (𝑍𝐵𝑍 ∈ (𝐾𝑚 (𝑁 × 𝑁)))
34 elmapi 8086 . . . . . . . . . . . . . . . . . . 19 (𝑍 ∈ (𝐾𝑚 (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
3531, 33, 343syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍:(𝑁 × 𝑁)⟶𝐾)
3635adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
3736ffnd 6226 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍 Fn (𝑁 × 𝑁))
385snssd 4496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁)
39 xpss1 5298 . . . . . . . . . . . . . . . . 17 ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
4038, 39syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
41 fnssres 6184 . . . . . . . . . . . . . . . 16 ((𝑍 Fn (𝑁 × 𝑁) ∧ ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
4237, 40, 41syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
43 eqidd 2766 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ ⟨𝐼, (𝑝𝐼)⟩ ∈ ({𝐼} × 𝑁)) → ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩))
4428, 30, 42, 43ofc1 7122 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ ⟨𝐼, (𝑝𝐼)⟩ ∈ ({𝐼} × 𝑁)) → (((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝𝐼)⟩) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)))
4518, 44mpdan 678 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝𝐼)⟩) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)))
46 df-ov 6849 . . . . . . . . . . . . 13 (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)) = (((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝𝐼)⟩)
47 df-ov 6849 . . . . . . . . . . . . . 14 (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)
4847oveq2i 6857 . . . . . . . . . . . . 13 (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩))
4945, 46, 483eqtr4g 2824 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘𝑓 · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))))
503, 16, 493eqtr3d 2807 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))))
51 ovres 7002 . . . . . . . . . . . . 13 ((𝐼 ∈ {𝐼} ∧ (𝑝𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑍(𝑝𝐼)))
527, 14, 51syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑍(𝑝𝐼)))
5352oveq2d 6862 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))) = (𝑌 · (𝐼𝑍(𝑝𝐼))))
5450, 53eqtrd 2799 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝𝐼)) = (𝑌 · (𝐼𝑍(𝑝𝐼))))
5554oveq1d 6861 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))) = ((𝑌 · (𝐼𝑍(𝑝𝐼))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
56 mdetrsca.r . . . . . . . . . . . 12 (𝜑𝑅 ∈ CRing)
57 crngring 18839 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
5856, 57syl 17 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
5958adantr 472 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
6036, 5, 14fovrnd 7008 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝𝐼)) ∈ 𝐾)
61 eqid 2765 . . . . . . . . . . . 12 (mulGrp‘𝑅) = (mulGrp‘𝑅)
6261, 32mgpbas 18776 . . . . . . . . . . 11 𝐾 = (Base‘(mulGrp‘𝑅))
6361crngmgp 18836 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
6456, 63syl 17 . . . . . . . . . . . 12 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
6564adantr 472 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
66 difssd 3902 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁)
67 ssfi 8391 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝐼}) ⊆ 𝑁) → (𝑁 ∖ {𝐼}) ∈ Fin)
6826, 66, 67syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin)
69 eldifi 3896 . . . . . . . . . . . . 13 (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟𝑁)
7035ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
71 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑟𝑁)
7213ffvelrnda 6553 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑝𝑟) ∈ 𝑁)
7370, 71, 72fovrnd 7008 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑟𝑍(𝑝𝑟)) ∈ 𝐾)
7469, 73sylan2 586 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝𝑟)) ∈ 𝐾)
7574ralrimiva 3113 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑍(𝑝𝑟)) ∈ 𝐾)
7662, 65, 68, 75gsummptcl 18646 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))) ∈ 𝐾)
77 mdetrsca.t . . . . . . . . . . 11 · = (.r𝑅)
7832, 77ringass 18845 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (𝑌𝐾 ∧ (𝐼𝑍(𝑝𝐼)) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))) ∈ 𝐾)) → ((𝑌 · (𝐼𝑍(𝑝𝐼))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))))))
7959, 30, 60, 76, 78syl13anc 1491 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (𝐼𝑍(𝑝𝐼))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))))))
8055, 79eqtrd 2799 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))))))
8161, 77mgpplusg 18774 . . . . . . . . . 10 · = (+g‘(mulGrp‘𝑅))
8221, 32, 22matbas2i 20518 . . . . . . . . . . . . 13 (𝑋𝐵𝑋 ∈ (𝐾𝑚 (𝑁 × 𝑁)))
83 elmapi 8086 . . . . . . . . . . . . 13 (𝑋 ∈ (𝐾𝑚 (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
8420, 82, 833syl 18 . . . . . . . . . . . 12 (𝜑𝑋:(𝑁 × 𝑁)⟶𝐾)
8584ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
8685, 71, 72fovrnd 7008 . . . . . . . . . 10 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑟𝑋(𝑝𝑟)) ∈ 𝐾)
87 disjdif 4202 . . . . . . . . . . 11 ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅
8887a1i 11 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅)
89 undif 4211 . . . . . . . . . . . 12 ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
9038, 89sylib 209 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
9190eqcomd 2771 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼})))
9262, 81, 65, 26, 86, 88, 91gsummptfidmsplit 18610 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
93 cmnmnd 18488 . . . . . . . . . . . 12 ((mulGrp‘𝑅) ∈ CMnd → (mulGrp‘𝑅) ∈ Mnd)
9465, 93syl 17 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd)
9584adantr 472 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
9695, 5, 14fovrnd 7008 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝𝐼)) ∈ 𝐾)
97 id 22 . . . . . . . . . . . . 13 (𝑟 = 𝐼𝑟 = 𝐼)
98 fveq2 6379 . . . . . . . . . . . . 13 (𝑟 = 𝐼 → (𝑝𝑟) = (𝑝𝐼))
9997, 98oveq12d 6864 . . . . . . . . . . . 12 (𝑟 = 𝐼 → (𝑟𝑋(𝑝𝑟)) = (𝐼𝑋(𝑝𝐼)))
10062, 99gsumsn 18634 . . . . . . . . . . 11 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼𝑁 ∧ (𝐼𝑋(𝑝𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) = (𝐼𝑋(𝑝𝐼)))
10194, 5, 96, 100syl3anc 1490 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) = (𝐼𝑋(𝑝𝐼)))
102 mdetrsca.ne . . . . . . . . . . . . . . 15 (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
103102oveqd 6863 . . . . . . . . . . . . . 14 (𝜑 → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)))
104103ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)))
105 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼}))
10669, 72sylan2 586 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝𝑟) ∈ 𝑁)
107 ovres 7002 . . . . . . . . . . . . . 14 ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑋(𝑝𝑟)))
108105, 106, 107syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑋(𝑝𝑟)))
109 ovres 7002 . . . . . . . . . . . . . 14 ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑍(𝑝𝑟)))
110105, 106, 109syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑍(𝑝𝑟)))
111104, 108, 1103eqtr3d 2807 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝𝑟)) = (𝑟𝑍(𝑝𝑟)))
112111mpteq2dva 4905 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))
113112oveq2d 6862 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))))
114101, 113oveq12d 6864 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) = ((𝐼𝑋(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
11592, 114eqtrd 2799 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))) = ((𝐼𝑋(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
11662, 81, 65, 26, 73, 88, 91gsummptfidmsplit 18610 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
11797, 98oveq12d 6864 . . . . . . . . . . . . 13 (𝑟 = 𝐼 → (𝑟𝑍(𝑝𝑟)) = (𝐼𝑍(𝑝𝐼)))
11862, 117gsumsn 18634 . . . . . . . . . . . 12 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼𝑁 ∧ (𝐼𝑍(𝑝𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) = (𝐼𝑍(𝑝𝐼)))
11994, 5, 60, 118syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) = (𝐼𝑍(𝑝𝐼)))
120119oveq1d 6861 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))) = ((𝐼𝑍(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
121116, 120eqtrd 2799 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) = ((𝐼𝑍(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
122121oveq2d 6862 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))))))
12380, 115, 1223eqtr4d 2809 . . . . . . 7 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))) = (𝑌 · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))
124123oveq2d 6862 . . . . . 6 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
12556adantr 472 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ CRing)
126 zrhpsgnmhm 20216 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
12758, 25, 126syl2anc 579 . . . . . . . . . . 11 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
1289, 62mhmf 17620 . . . . . . . . . . 11 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
129127, 128syl 17 . . . . . . . . . 10 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
130129ffvelrnda 6553 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾)
13132, 77crngcom 18843 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾𝑌𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)))
132125, 130, 30, 131syl3anc 1490 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)))
133132oveq1d 6861 . . . . . . 7 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))
13473ralrimiva 3113 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟𝑁 (𝑟𝑍(𝑝𝑟)) ∈ 𝐾)
13562, 65, 26, 134gsummptcl 18646 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ 𝐾)
13632, 77ringass 18845 . . . . . . . 8 ((𝑅 ∈ Ring ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾𝑌𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ 𝐾)) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
13759, 130, 30, 135, 136syl13anc 1491 . . . . . . 7 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
13832, 77ringass 18845 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑌𝐾 ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ 𝐾)) → ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
13959, 30, 130, 135, 138syl13anc 1491 . . . . . . 7 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
140133, 137, 1393eqtr3d 2807 . . . . . 6 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
141124, 140eqtrd 2799 . . . . 5 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
142141mpteq2dva 4905 . . . 4 (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))))
143142oveq2d 6862 . . 3 (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
144 eqid 2765 . . . 4 (0g𝑅) = (0g𝑅)
145 eqid 2765 . . . 4 (+g𝑅) = (+g𝑅)
1468, 9symgbasfi 18083 . . . . 5 (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
14725, 146syl 17 . . . 4 (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
14832, 77ringcl 18842 . . . . 5 ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) ∈ 𝐾)
14959, 130, 135, 148syl3anc 1490 . . . 4 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) ∈ 𝐾)
150 eqid 2765 . . . . 5 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))
151 ovexd 6880 . . . . 5 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) ∈ V)
152 fvexd 6394 . . . . 5 (𝜑 → (0g𝑅) ∈ V)
153150, 147, 151, 152fsuppmptdm 8497 . . . 4 (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) finSupp (0g𝑅))
15432, 144, 145, 77, 58, 147, 29, 149, 153gsummulc2 18888 . . 3 (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
155143, 154eqtrd 2799 . 2 (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
156 mdetrsca.d . . . 4 𝐷 = (𝑁 maDet 𝑅)
157 eqid 2765 . . . 4 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
158 eqid 2765 . . . 4 (pmSgn‘𝑁) = (pmSgn‘𝑁)
159156, 21, 22, 9, 157, 158, 77, 61mdetleib2 20685 . . 3 ((𝑅 ∈ CRing ∧ 𝑋𝐵) → (𝐷𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))))
16056, 20, 159syl2anc 579 . 2 (𝜑 → (𝐷𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))))
161156, 21, 22, 9, 157, 158, 77, 61mdetleib2 20685 . . . 4 ((𝑅 ∈ CRing ∧ 𝑍𝐵) → (𝐷𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))))
16256, 31, 161syl2anc 579 . . 3 (𝜑 → (𝐷𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))))
163162oveq2d 6862 . 2 (𝜑 → (𝑌 · (𝐷𝑍)) = (𝑌 · (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
164155, 160, 1633eqtr4d 2809 1 (𝜑 → (𝐷𝑋) = (𝑌 · (𝐷𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  {csn 4336  cop 4342  cmpt 4890   × cxp 5277  cres 5281  ccom 5283   Fn wfn 6065  wf 6066  1-1-ontowf1o 6069  cfv 6070  (class class class)co 6846  𝑓 cof 7097  𝑚 cmap 8064  Fincfn 8164  Basecbs 16144  +gcplusg 16228  .rcmulr 16229  0gc0g 16380   Σg cgsu 16381  Mndcmnd 17574   MndHom cmhm 17613  SymGrpcsymg 18074  pmSgncpsgn 18186  CMndccmn 18473  mulGrpcmgp 18770  Ringcrg 18828  CRingccrg 18829  ℤRHomczrh 20135   Mat cmat 20503   maDet cmdat 20681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-xor 1634  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-ot 4345  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-tpos 7559  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-sup 8559  df-oi 8626  df-card 9020  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-xnn0 11615  df-z 11629  df-dec 11746  df-uz 11892  df-rp 12034  df-fz 12539  df-fzo 12679  df-seq 13014  df-exp 13073  df-hash 13327  df-word 13492  df-lsw 13540  df-concat 13548  df-s1 13573  df-substr 13623  df-pfx 13672  df-splice 13779  df-reverse 13797  df-s2 13891  df-struct 16146  df-ndx 16147  df-slot 16148  df-base 16150  df-sets 16151  df-ress 16152  df-plusg 16241  df-mulr 16242  df-starv 16243  df-sca 16244  df-vsca 16245  df-ip 16246  df-tset 16247  df-ple 16248  df-ds 16250  df-unif 16251  df-hom 16252  df-cco 16253  df-0g 16382  df-gsum 16383  df-prds 16388  df-pws 16390  df-mre 16526  df-mrc 16527  df-acs 16529  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-mhm 17615  df-submnd 17616  df-grp 17706  df-minusg 17707  df-mulg 17822  df-subg 17869  df-ghm 17936  df-gim 17979  df-cntz 18027  df-oppg 18053  df-symg 18075  df-pmtr 18139  df-psgn 18188  df-cmn 18475  df-abl 18476  df-mgp 18771  df-ur 18783  df-ring 18830  df-cring 18831  df-oppr 18904  df-dvdsr 18922  df-unit 18923  df-invr 18953  df-dvr 18964  df-rnghom 18998  df-drng 19032  df-subrg 19061  df-sra 19460  df-rgmod 19461  df-cnfld 20034  df-zring 20106  df-zrh 20139  df-dsmm 20366  df-frlm 20381  df-mat 20504  df-mdet 20682
This theorem is referenced by:  mdetrsca2  20701  mdetuni0  20718  mdetmul  20720  smadiadetg  20771
  Copyright terms: Public domain W3C validator