Step | Hyp | Ref
| Expression |
1 | | cramer.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ΄) |
2 | | cramer.a |
. . . . . . . . . 10
β’ π΄ = (π Mat π
) |
3 | 2 | fveq2i 6895 |
. . . . . . . . 9
β’
(Baseβπ΄) =
(Baseβ(π Mat π
)) |
4 | 1, 3 | eqtri 2761 |
. . . . . . . 8
β’ π΅ = (Baseβ(π Mat π
)) |
5 | | fvoveq1 7432 |
. . . . . . . 8
β’ (π = β
β
(Baseβ(π Mat π
)) = (Baseβ(β
Mat
π
))) |
6 | 4, 5 | eqtrid 2785 |
. . . . . . 7
β’ (π = β
β π΅ = (Baseβ(β
Mat
π
))) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π = β
β§ π
β CRing) β π΅ = (Baseβ(β
Mat
π
))) |
8 | 7 | eleq2d 2820 |
. . . . 5
β’ ((π = β
β§ π
β CRing) β (π β π΅ β π β (Baseβ(β
Mat π
)))) |
9 | | mat0dimbas0 21968 |
. . . . . . 7
β’ (π
β CRing β
(Baseβ(β
Mat π
)) = {β
}) |
10 | 9 | eleq2d 2820 |
. . . . . 6
β’ (π
β CRing β (π β (Baseβ(β
Mat
π
)) β π β
{β
})) |
11 | 10 | adantl 483 |
. . . . 5
β’ ((π = β
β§ π
β CRing) β (π β (Baseβ(β
Mat
π
)) β π β
{β
})) |
12 | 8, 11 | bitrd 279 |
. . . 4
β’ ((π = β
β§ π
β CRing) β (π β π΅ β π β {β
})) |
13 | | cramer.v |
. . . . . . . 8
β’ π = ((Baseβπ
) βm π) |
14 | 13 | a1i 11 |
. . . . . . 7
β’ ((π = β
β§ π
β CRing) β π = ((Baseβπ
) βm π)) |
15 | | oveq2 7417 |
. . . . . . . 8
β’ (π = β
β
((Baseβπ
)
βm π) =
((Baseβπ
)
βm β
)) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π = β
β§ π
β CRing) β
((Baseβπ
)
βm π) =
((Baseβπ
)
βm β
)) |
17 | | fvex 6905 |
. . . . . . . 8
β’
(Baseβπ
)
β V |
18 | | map0e 8876 |
. . . . . . . 8
β’
((Baseβπ
)
β V β ((Baseβπ
) βm β
) =
1o) |
19 | 17, 18 | mp1i 13 |
. . . . . . 7
β’ ((π = β
β§ π
β CRing) β
((Baseβπ
)
βm β
) = 1o) |
20 | 14, 16, 19 | 3eqtrd 2777 |
. . . . . 6
β’ ((π = β
β§ π
β CRing) β π =
1o) |
21 | 20 | eleq2d 2820 |
. . . . 5
β’ ((π = β
β§ π
β CRing) β (π β π β π β 1o)) |
22 | | el1o 8495 |
. . . . 5
β’ (π β 1o β
π =
β
) |
23 | 21, 22 | bitrdi 287 |
. . . 4
β’ ((π = β
β§ π
β CRing) β (π β π β π = β
)) |
24 | 12, 23 | anbi12d 632 |
. . 3
β’ ((π = β
β§ π
β CRing) β ((π β π΅ β§ π β π) β (π β {β
} β§ π = β
))) |
25 | | elsni 4646 |
. . . 4
β’ (π β {β
} β π = β
) |
26 | | mpteq1 5242 |
. . . . . . . . . 10
β’ (π = β
β (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) = (π β β
β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ)))) |
27 | | mpt0 6693 |
. . . . . . . . . 10
β’ (π β β
β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) = β
|
28 | 26, 27 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π = β
β (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) = β
) |
29 | 28 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = β
β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β π = β
)) |
30 | 29 | ad2antrr 725 |
. . . . . . 7
β’ (((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β π = β
)) |
31 | | simplrl 776 |
. . . . . . . . . 10
β’ ((((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β§ π = β
) β π = β
) |
32 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β§ π = β
) β π = β
) |
33 | 31, 32 | oveq12d 7427 |
. . . . . . . . 9
β’ ((((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β§ π = β
) β (π Β· π) = (β
Β·
β
)) |
34 | | cramer.x |
. . . . . . . . . . 11
β’ Β· =
(π
maVecMul β¨π, πβ©) |
35 | 34 | mavmul0 22054 |
. . . . . . . . . 10
β’ ((π = β
β§ π
β CRing) β (β
Β·
β
) = β
) |
36 | 35 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β§ π = β
) β (β
Β·
β
) = β
) |
37 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π = β
β§ π = β
) β π = β
) |
38 | 37 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((π = β
β§ π = β
) β β
=
π) |
39 | 38 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β§ π = β
) β β
=
π) |
40 | 33, 36, 39 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β§ π = β
) β (π Β· π) = π) |
41 | 40 | ex 414 |
. . . . . . 7
β’ (((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β (π = β
β (π Β· π) = π)) |
42 | 30, 41 | sylbid 239 |
. . . . . 6
β’ (((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β (π Β· π) = π)) |
43 | 42 | a1d 25 |
. . . . 5
β’ (((π = β
β§ π
β CRing) β§ (π = β
β§ π = β
)) β ((π·βπ) β (Unitβπ
) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β (π Β· π) = π))) |
44 | 43 | ex 414 |
. . . 4
β’ ((π = β
β§ π
β CRing) β ((π = β
β§ π = β
) β ((π·βπ) β (Unitβπ
) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β (π Β· π) = π)))) |
45 | 25, 44 | sylani 605 |
. . 3
β’ ((π = β
β§ π
β CRing) β ((π β {β
} β§ π = β
) β ((π·βπ) β (Unitβπ
) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β (π Β· π) = π)))) |
46 | 24, 45 | sylbid 239 |
. 2
β’ ((π = β
β§ π
β CRing) β ((π β π΅ β§ π β π) β ((π·βπ) β (Unitβπ
) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β (π Β· π) = π)))) |
47 | 46 | 3imp 1112 |
1
β’ (((π = β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (π = (π β π β¦ ((π·β((π(π matRepV π
)π)βπ)) / (π·βπ))) β (π Β· π) = π)) |