Step | Hyp | Ref
| Expression |
1 | | mdetfval.d |
. 2
β’ π· = (π maDet π
) |
2 | | oveq12 7370 |
. . . . . . . 8
β’ ((π = π β§ π = π
) β (π Mat π) = (π Mat π
)) |
3 | | mdetfval.a |
. . . . . . . 8
β’ π΄ = (π Mat π
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
β’ ((π = π β§ π = π
) β (π Mat π) = π΄) |
5 | 4 | fveq2d 6850 |
. . . . . 6
β’ ((π = π β§ π = π
) β (Baseβ(π Mat π)) = (Baseβπ΄)) |
6 | | mdetfval.b |
. . . . . 6
β’ π΅ = (Baseβπ΄) |
7 | 5, 6 | eqtr4di 2791 |
. . . . 5
β’ ((π = π β§ π = π
) β (Baseβ(π Mat π)) = π΅) |
8 | | simpr 486 |
. . . . . 6
β’ ((π = π β§ π = π
) β π = π
) |
9 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = π β§ π = π
) β π = π) |
10 | 9 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π = π β§ π = π
) β (SymGrpβπ) = (SymGrpβπ)) |
11 | 10 | fveq2d 6850 |
. . . . . . . 8
β’ ((π = π β§ π = π
) β (Baseβ(SymGrpβπ)) =
(Baseβ(SymGrpβπ))) |
12 | | mdetfval.p |
. . . . . . . 8
β’ π =
(Baseβ(SymGrpβπ)) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . . 7
β’ ((π = π β§ π = π
) β (Baseβ(SymGrpβπ)) = π) |
14 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π
β (.rβπ) = (.rβπ
)) |
15 | 14 | adantl 483 |
. . . . . . . . 9
β’ ((π = π β§ π = π
) β (.rβπ) = (.rβπ
)) |
16 | | mdetfval.t |
. . . . . . . . 9
β’ Β· =
(.rβπ
) |
17 | 15, 16 | eqtr4di 2791 |
. . . . . . . 8
β’ ((π = π β§ π = π
) β (.rβπ) = Β· ) |
18 | 8 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π
) β (β€RHomβπ) = (β€RHomβπ
)) |
19 | | mdetfval.y |
. . . . . . . . . . 11
β’ π = (β€RHomβπ
) |
20 | 18, 19 | eqtr4di 2791 |
. . . . . . . . . 10
β’ ((π = π β§ π = π
) β (β€RHomβπ) = π) |
21 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π = π β (pmSgnβπ) = (pmSgnβπ)) |
22 | 21 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π
) β (pmSgnβπ) = (pmSgnβπ)) |
23 | | mdetfval.s |
. . . . . . . . . . 11
β’ π = (pmSgnβπ) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . . . 10
β’ ((π = π β§ π = π
) β (pmSgnβπ) = π) |
25 | 20, 24 | coeq12d 5824 |
. . . . . . . . 9
β’ ((π = π β§ π = π
) β ((β€RHomβπ) β (pmSgnβπ)) = (π β π)) |
26 | 25 | fveq1d 6848 |
. . . . . . . 8
β’ ((π = π β§ π = π
) β (((β€RHomβπ) β (pmSgnβπ))βπ) = ((π β π)βπ)) |
27 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π
β (mulGrpβπ) = (mulGrpβπ
)) |
28 | 27 | adantl 483 |
. . . . . . . . . 10
β’ ((π = π β§ π = π
) β (mulGrpβπ) = (mulGrpβπ
)) |
29 | | mdetfval.u |
. . . . . . . . . 10
β’ π = (mulGrpβπ
) |
30 | 28, 29 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π = π β§ π = π
) β (mulGrpβπ) = π) |
31 | 9 | mpteq1d 5204 |
. . . . . . . . 9
β’ ((π = π β§ π = π
) β (π₯ β π β¦ ((πβπ₯)ππ₯)) = (π₯ β π β¦ ((πβπ₯)ππ₯))) |
32 | 30, 31 | oveq12d 7379 |
. . . . . . . 8
β’ ((π = π β§ π = π
) β ((mulGrpβπ) Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))) = (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))) |
33 | 17, 26, 32 | oveq123d 7382 |
. . . . . . 7
β’ ((π = π β§ π = π
) β ((((β€RHomβπ) β (pmSgnβπ))βπ)(.rβπ)((mulGrpβπ) Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))) = (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))) |
34 | 13, 33 | mpteq12dv 5200 |
. . . . . 6
β’ ((π = π β§ π = π
) β (π β (Baseβ(SymGrpβπ)) β¦
((((β€RHomβπ)
β (pmSgnβπ))βπ)(.rβπ)((mulGrpβπ) Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))) = (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))) |
35 | 8, 34 | oveq12d 7379 |
. . . . 5
β’ ((π = π β§ π = π
) β (π Ξ£g (π β
(Baseβ(SymGrpβπ)) β¦ ((((β€RHomβπ) β (pmSgnβπ))βπ)(.rβπ)((mulGrpβπ) Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))) = (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) |
36 | 7, 35 | mpteq12dv 5200 |
. . . 4
β’ ((π = π β§ π = π
) β (π β (Baseβ(π Mat π)) β¦ (π Ξ£g (π β
(Baseβ(SymGrpβπ)) β¦ ((((β€RHomβπ) β (pmSgnβπ))βπ)(.rβπ)((mulGrpβπ) Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) = (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))))) |
37 | | df-mdet 21957 |
. . . 4
β’ maDet =
(π β V, π β V β¦ (π β (Baseβ(π Mat π)) β¦ (π Ξ£g (π β
(Baseβ(SymGrpβπ)) β¦ ((((β€RHomβπ) β (pmSgnβπ))βπ)(.rβπ)((mulGrpβπ) Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))))) |
38 | 6 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
39 | 38 | mptex 7177 |
. . . 4
β’ (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) β V |
40 | 36, 37, 39 | ovmpoa 7514 |
. . 3
β’ ((π β V β§ π
β V) β (π maDet π
) = (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))))) |
41 | 37 | reldmmpo 7494 |
. . . . . 6
β’ Rel dom
maDet |
42 | 41 | ovprc 7399 |
. . . . 5
β’ (Β¬
(π β V β§ π
β V) β (π maDet π
) = β
) |
43 | | mpt0 6647 |
. . . . 5
β’ (π β β
β¦ (π
Ξ£g
(π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) = β
|
44 | 42, 43 | eqtr4di 2791 |
. . . 4
β’ (Β¬
(π β V β§ π
β V) β (π maDet π
) = (π β β
β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))))) |
45 | | df-mat 21778 |
. . . . . . . . . 10
β’ Mat =
(π¦ β Fin, π§ β V β¦ ((π§ freeLMod (π¦ Γ π¦)) sSet β¨(.rβndx),
(π§ maMul β¨π¦, π¦, π¦β©)β©)) |
46 | 45 | reldmmpo 7494 |
. . . . . . . . 9
β’ Rel dom
Mat |
47 | 46 | ovprc 7399 |
. . . . . . . 8
β’ (Β¬
(π β V β§ π
β V) β (π Mat π
) = β
) |
48 | 3, 47 | eqtrid 2785 |
. . . . . . 7
β’ (Β¬
(π β V β§ π
β V) β π΄ = β
) |
49 | 48 | fveq2d 6850 |
. . . . . 6
β’ (Β¬
(π β V β§ π
β V) β
(Baseβπ΄) =
(Baseββ
)) |
50 | | base0 17096 |
. . . . . 6
β’ β
=
(Baseββ
) |
51 | 49, 6, 50 | 3eqtr4g 2798 |
. . . . 5
β’ (Β¬
(π β V β§ π
β V) β π΅ = β
) |
52 | 51 | mpteq1d 5204 |
. . . 4
β’ (Β¬
(π β V β§ π
β V) β (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) = (π β β
β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))))) |
53 | 44, 52 | eqtr4d 2776 |
. . 3
β’ (Β¬
(π β V β§ π
β V) β (π maDet π
) = (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯)))))))) |
54 | 40, 53 | pm2.61i 182 |
. 2
β’ (π maDet π
) = (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) |
55 | 1, 54 | eqtri 2761 |
1
β’ π· = (π β π΅ β¦ (π
Ξ£g (π β π β¦ (((π β π)βπ) Β· (π Ξ£g (π₯ β π β¦ ((πβπ₯)ππ₯))))))) |