Step | Hyp | Ref
| Expression |
1 | | mdetfval.d |
. 2
⊢ 𝐷 = (𝑁 maDet 𝑅) |
2 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
3 | | mdetfval.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = 𝐴) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘𝐴)) |
6 | | mdetfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
8 | | simpr 476 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅) |
9 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
10 | 9 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (SymGrp‘𝑛) = (SymGrp‘𝑁)) |
11 | 10 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(SymGrp‘𝑛)) =
(Base‘(SymGrp‘𝑁))) |
12 | | mdetfval.p |
. . . . . . . 8
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(SymGrp‘𝑛)) = 𝑃) |
14 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
15 | 14 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (.r‘𝑟) = (.r‘𝑅)) |
16 | | mdetfval.t |
. . . . . . . . 9
⊢ · =
(.r‘𝑅) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (.r‘𝑟) = · ) |
18 | 8 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (ℤRHom‘𝑟) = (ℤRHom‘𝑅)) |
19 | | mdetfval.y |
. . . . . . . . . . 11
⊢ 𝑌 = (ℤRHom‘𝑅) |
20 | 18, 19 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (ℤRHom‘𝑟) = 𝑌) |
21 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (pmSgn‘𝑛) = (pmSgn‘𝑁)) |
22 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (pmSgn‘𝑛) = (pmSgn‘𝑁)) |
23 | | mdetfval.s |
. . . . . . . . . . 11
⊢ 𝑆 = (pmSgn‘𝑁) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (pmSgn‘𝑛) = 𝑆) |
25 | 20, 24 | coeq12d 5208 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛)) = (𝑌 ∘ 𝑆)) |
26 | 25 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝) = ((𝑌 ∘ 𝑆)‘𝑝)) |
27 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
28 | 27 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
29 | | mdetfval.u |
. . . . . . . . . 10
⊢ 𝑈 = (mulGrp‘𝑅) |
30 | 28, 29 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (mulGrp‘𝑟) = 𝑈) |
31 | 9 | mpteq1d 4666 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)) = (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))) |
32 | 30, 31 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))) = (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))) |
33 | 17, 26, 32 | oveq123d 6570 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))) = (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))) |
34 | 13, 33 | mpteq12dv 4663 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦
((((ℤRHom‘𝑟)
∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))) = (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))) |
35 | 8, 34 | oveq12d 6567 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |
36 | 7, 35 | mpteq12dv 4663 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
37 | | df-mdet 20210 |
. . . 4
⊢ maDet =
(𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
38 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐴)
∈ V |
39 | 6, 38 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
40 | 39 | mptex 6390 |
. . . 4
⊢ (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) ∈ V |
41 | 36, 37, 40 | ovmpt2a 6689 |
. . 3
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
42 | 37 | reldmmpt2 6669 |
. . . . . 6
⊢ Rel dom
maDet |
43 | 42 | ovprc 6581 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = ∅) |
44 | | mpt0 5934 |
. . . . 5
⊢ (𝑚 ∈ ∅ ↦ (𝑅 Σg
(𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) = ∅ |
45 | 43, 44 | syl6eqr 2662 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = (𝑚 ∈ ∅ ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
46 | | df-mat 20033 |
. . . . . . . . . 10
⊢ Mat =
(𝑦 ∈ Fin, 𝑧 ∈ V ↦ ((𝑧 freeLMod (𝑦 × 𝑦)) sSet 〈(.r‘ndx),
(𝑧 maMul 〈𝑦, 𝑦, 𝑦〉)〉)) |
47 | 46 | reldmmpt2 6669 |
. . . . . . . . 9
⊢ Rel dom
Mat |
48 | 47 | ovprc 6581 |
. . . . . . . 8
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅) |
49 | 3, 48 | syl5eq 2656 |
. . . . . . 7
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → 𝐴 = ∅) |
50 | 49 | fveq2d 6107 |
. . . . . 6
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝐴) =
(Base‘∅)) |
51 | | base0 15740 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
52 | 50, 6, 51 | 3eqtr4g 2669 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
53 | 52 | mpteq1d 4666 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) = (𝑚 ∈ ∅ ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
54 | 45, 53 | eqtr4d 2647 |
. . 3
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 maDet 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
55 | 41, 54 | pm2.61i 175 |
. 2
⊢ (𝑁 maDet 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |
56 | 1, 55 | eqtri 2632 |
1
⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |