Step | Hyp | Ref
| Expression |
1 | | madufval.j |
. 2
β’ π½ = (π maAdju π
) |
2 | | fvoveq1 7374 |
. . . . . 6
β’ (π = π β (Baseβ(π Mat π)) = (Baseβ(π Mat π))) |
3 | | id 22 |
. . . . . . 7
β’ (π = π β π = π) |
4 | | oveq1 7358 |
. . . . . . . 8
β’ (π = π β (π maDet π) = (π maDet π)) |
5 | | eqidd 2738 |
. . . . . . . . 9
β’ (π = π β if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)) = if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))) |
6 | 3, 3, 5 | mpoeq123dv 7426 |
. . . . . . . 8
β’ (π = π β (π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))) = (π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)))) |
7 | 4, 6 | fveq12d 6846 |
. . . . . . 7
β’ (π = π β ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)))) = ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))))) |
8 | 3, 3, 7 | mpoeq123dv 7426 |
. . . . . 6
β’ (π = π β (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))))) = (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)))))) |
9 | 2, 8 | mpteq12dv 5194 |
. . . . 5
β’ (π = π β (π β (Baseβ(π Mat π)) β¦ (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)))))) = (π β (Baseβ(π Mat π)) β¦ (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))))))) |
10 | | oveq2 7359 |
. . . . . . 7
β’ (π = π
β (π Mat π) = (π Mat π
)) |
11 | 10 | fveq2d 6843 |
. . . . . 6
β’ (π = π
β (Baseβ(π Mat π)) = (Baseβ(π Mat π
))) |
12 | | oveq2 7359 |
. . . . . . . 8
β’ (π = π
β (π maDet π) = (π maDet π
)) |
13 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (π = π
β (1rβπ) = (1rβπ
)) |
14 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (π = π
β (0gβπ) = (0gβπ
)) |
15 | 13, 14 | ifeq12d 4505 |
. . . . . . . . . 10
β’ (π = π
β if(π = π, (1rβπ), (0gβπ)) = if(π = π, (1rβπ
), (0gβπ
))) |
16 | 15 | ifeq1d 4503 |
. . . . . . . . 9
β’ (π = π
β if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)) = if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))) |
17 | 16 | mpoeq3dv 7430 |
. . . . . . . 8
β’ (π = π
β (π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))) = (π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ)))) |
18 | 12, 17 | fveq12d 6846 |
. . . . . . 7
β’ (π = π
β ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)))) = ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))))) |
19 | 18 | mpoeq3dv 7430 |
. . . . . 6
β’ (π = π
β (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))))) = (π β π, π β π β¦ ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ)))))) |
20 | 11, 19 | mpteq12dv 5194 |
. . . . 5
β’ (π = π
β (π β (Baseβ(π Mat π)) β¦ (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ)))))) = (π β (Baseβ(π Mat π
)) β¦ (π β π, π β π β¦ ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))))))) |
21 | | df-madu 21935 |
. . . . 5
β’ maAdju =
(π β V, π β V β¦ (π β (Baseβ(π Mat π)) β¦ (π β π, π β π β¦ ((π maDet π)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ), (0gβπ)), (πππ))))))) |
22 | | fvex 6852 |
. . . . . 6
β’
(Baseβ(π Mat
π
)) β
V |
23 | 22 | mptex 7169 |
. . . . 5
β’ (π β (Baseβ(π Mat π
)) β¦ (π β π, π β π β¦ ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ)))))) β V |
24 | 9, 20, 21, 23 | ovmpo 7509 |
. . . 4
β’ ((π β V β§ π
β V) β (π maAdju π
) = (π β (Baseβ(π Mat π
)) β¦ (π β π, π β π β¦ ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))))))) |
25 | | madufval.b |
. . . . . 6
β’ π΅ = (Baseβπ΄) |
26 | | madufval.a |
. . . . . . 7
β’ π΄ = (π Mat π
) |
27 | 26 | fveq2i 6842 |
. . . . . 6
β’
(Baseβπ΄) =
(Baseβ(π Mat π
)) |
28 | 25, 27 | eqtri 2765 |
. . . . 5
β’ π΅ = (Baseβ(π Mat π
)) |
29 | | madufval.d |
. . . . . . . 8
β’ π· = (π maDet π
) |
30 | | madufval.o |
. . . . . . . . . . . 12
β’ 1 =
(1rβπ
) |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β 1 =
(1rβπ
)) |
32 | | madufval.z |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ
) |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β 0 =
(0gβπ
)) |
34 | 31, 33 | ifeq12d 4505 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β if(π = π, 1 , 0 ) = if(π = π, (1rβπ
), (0gβπ
))) |
35 | 34 | ifeq1d 4503 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β if(π = π, if(π = π, 1 , 0 ), (πππ)) = if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))) |
36 | 35 | mpoeq3ia 7429 |
. . . . . . . 8
β’ (π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ))) = (π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))) |
37 | 29, 36 | fveq12i 6845 |
. . . . . . 7
β’ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))) = ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ)))) |
38 | 37 | a1i 11 |
. . . . . 6
β’ ((π β π β§ π β π) β (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))) = ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))))) |
39 | 38 | mpoeq3ia 7429 |
. . . . 5
β’ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ))))) = (π β π, π β π β¦ ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ))))) |
40 | 28, 39 | mpteq12i 5209 |
. . . 4
β’ (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))))) = (π β (Baseβ(π Mat π
)) β¦ (π β π, π β π β¦ ((π maDet π
)β(π β π, π β π β¦ if(π = π, if(π = π, (1rβπ
), (0gβπ
)), (πππ)))))) |
41 | 24, 40 | eqtr4di 2795 |
. . 3
β’ ((π β V β§ π
β V) β (π maAdju π
) = (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ))))))) |
42 | 21 | reldmmpo 7484 |
. . . . 5
β’ Rel dom
maAdju |
43 | 42 | ovprc 7389 |
. . . 4
β’ (Β¬
(π β V β§ π
β V) β (π maAdju π
) = β
) |
44 | | df-mat 21707 |
. . . . . . . . . . 11
β’ Mat =
(π β Fin, π β V β¦ ((π freeLMod (π Γ π)) sSet β¨(.rβndx),
(π maMul β¨π, π, πβ©)β©)) |
45 | 44 | reldmmpo 7484 |
. . . . . . . . . 10
β’ Rel dom
Mat |
46 | 45 | ovprc 7389 |
. . . . . . . . 9
β’ (Β¬
(π β V β§ π
β V) β (π Mat π
) = β
) |
47 | 26, 46 | eqtrid 2789 |
. . . . . . . 8
β’ (Β¬
(π β V β§ π
β V) β π΄ = β
) |
48 | 47 | fveq2d 6843 |
. . . . . . 7
β’ (Β¬
(π β V β§ π
β V) β
(Baseβπ΄) =
(Baseββ
)) |
49 | | base0 17048 |
. . . . . . 7
β’ β
=
(Baseββ
) |
50 | 48, 25, 49 | 3eqtr4g 2802 |
. . . . . 6
β’ (Β¬
(π β V β§ π
β V) β π΅ = β
) |
51 | 50 | mpteq1d 5198 |
. . . . 5
β’ (Β¬
(π β V β§ π
β V) β (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))))) = (π β β
β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ))))))) |
52 | | mpt0 6640 |
. . . . 5
β’ (π β β
β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))))) = β
|
53 | 51, 52 | eqtrdi 2793 |
. . . 4
β’ (Β¬
(π β V β§ π
β V) β (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))))) = β
) |
54 | 43, 53 | eqtr4d 2780 |
. . 3
β’ (Β¬
(π β V β§ π
β V) β (π maAdju π
) = (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ))))))) |
55 | 41, 54 | pm2.61i 182 |
. 2
β’ (π maAdju π
) = (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))))) |
56 | 1, 55 | eqtri 2765 |
1
β’ π½ = (π β π΅ β¦ (π β π, π β π β¦ (π·β(π β π, π β π β¦ if(π = π, if(π = π, 1 , 0 ), (πππ)))))) |