| Step | Hyp | Ref
| Expression |
| 1 | | mdetfval.d |
. 2
⊢ 𝐷 = (𝑁 maDet 𝑅) |
| 2 | | oveq12 7440 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
| 3 | | mdetfval.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = 𝐴) |
| 5 | 4 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘𝐴)) |
| 6 | | mdetfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
| 8 | | simpr 484 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅) |
| 9 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
| 10 | 9 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (SymGrp‘𝑛) = (SymGrp‘𝑁)) |
| 11 | 10 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(SymGrp‘𝑛)) =
(Base‘(SymGrp‘𝑁))) |
| 12 | | mdetfval.p |
. . . . . . . 8
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
| 13 | 11, 12 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(SymGrp‘𝑛)) = 𝑃) |
| 14 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
| 15 | 14 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (.r‘𝑟) = (.r‘𝑅)) |
| 16 | | mdetfval.t |
. . . . . . . . 9
⊢ · =
(.r‘𝑅) |
| 17 | 15, 16 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (.r‘𝑟) = · ) |
| 18 | 8 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (ℤRHom‘𝑟) = (ℤRHom‘𝑅)) |
| 19 | | mdetfval.y |
. . . . . . . . . . 11
⊢ 𝑌 = (ℤRHom‘𝑅) |
| 20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (ℤRHom‘𝑟) = 𝑌) |
| 21 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (pmSgn‘𝑛) = (pmSgn‘𝑁)) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (pmSgn‘𝑛) = (pmSgn‘𝑁)) |
| 23 | | mdetfval.s |
. . . . . . . . . . 11
⊢ 𝑆 = (pmSgn‘𝑁) |
| 24 | 22, 23 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (pmSgn‘𝑛) = 𝑆) |
| 25 | 20, 24 | coeq12d 5875 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛)) = (𝑌 ∘ 𝑆)) |
| 26 | 25 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝) = ((𝑌 ∘ 𝑆)‘𝑝)) |
| 27 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
| 28 | 27 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
| 29 | | mdetfval.u |
. . . . . . . . . 10
⊢ 𝑈 = (mulGrp‘𝑅) |
| 30 | 28, 29 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (mulGrp‘𝑟) = 𝑈) |
| 31 | 9 | mpteq1d 5237 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)) = (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))) |
| 32 | 30, 31 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))) = (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))) |
| 33 | 17, 26, 32 | oveq123d 7452 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))) = (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))) |
| 34 | 13, 33 | mpteq12dv 5233 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦
((((ℤRHom‘𝑟)
∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))) = (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))) |
| 35 | 8, 34 | oveq12d 7449 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |
| 36 | 7, 35 | mpteq12dv 5233 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 37 | | df-mdet 22591 |
. . . 4
⊢ maDet =
(𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 38 | 6 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 39 | 38 | mptex 7243 |
. . . 4
⊢ (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) ∈ V |
| 40 | 36, 37, 39 | ovmpoa 7588 |
. . 3
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 41 | 37 | reldmmpo 7567 |
. . . . . 6
⊢ Rel dom
maDet |
| 42 | 41 | ovprc 7469 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = ∅) |
| 43 | | mpt0 6710 |
. . . . 5
⊢ (𝑚 ∈ ∅ ↦ (𝑅 Σg
(𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) = ∅ |
| 44 | 42, 43 | eqtr4di 2795 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = (𝑚 ∈ ∅ ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 45 | | df-mat 22412 |
. . . . . . . . . 10
⊢ Mat =
(𝑦 ∈ Fin, 𝑧 ∈ V ↦ ((𝑧 freeLMod (𝑦 × 𝑦)) sSet 〈(.r‘ndx),
(𝑧 maMul 〈𝑦, 𝑦, 𝑦〉)〉)) |
| 46 | 45 | reldmmpo 7567 |
. . . . . . . . 9
⊢ Rel dom
Mat |
| 47 | 46 | ovprc 7469 |
. . . . . . . 8
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅) |
| 48 | 3, 47 | eqtrid 2789 |
. . . . . . 7
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → 𝐴 = ∅) |
| 49 | 48 | fveq2d 6910 |
. . . . . 6
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝐴) =
(Base‘∅)) |
| 50 | | base0 17252 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
| 51 | 49, 6, 50 | 3eqtr4g 2802 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
| 52 | 51 | mpteq1d 5237 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) = (𝑚 ∈ ∅ ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 53 | 44, 52 | eqtr4d 2780 |
. . 3
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 54 | 40, 53 | pm2.61i 182 |
. 2
⊢ (𝑁 maDet 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |
| 55 | 1, 54 | eqtri 2765 |
1
⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |