| Step | Hyp | Ref
| Expression |
|---|
| 1 | | slesolex.a |
. . . . 5
β’ π΄ = (π Mat π
) |
| 2 | | slesolex.x |
. . . . 5
β’ Β· =
(π
maVecMul β¨π, πβ©) |
| 3 | | eqid 2726 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
| 4 | | eqid 2726 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
| 5 | | crngring 20150 |
. . . . . . 7
β’ (π
β CRing β π
β Ring) |
| 6 | 5 | adantl 481 |
. . . . . 6
β’ ((π β β
β§ π
β CRing) β π
β Ring) |
| 7 | 6 | 3ad2ant1 1130 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π
β Ring) |
| 8 | | slesolex.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ΄) |
| 9 | 1, 8 | matrcl 22267 |
. . . . . . . 8
β’ (π β π΅ β (π β Fin β§ π
β V)) |
| 10 | 9 | simpld 494 |
. . . . . . 7
β’ (π β π΅ β π β Fin) |
| 11 | 10 | adantr 480 |
. . . . . 6
β’ ((π β π΅ β§ π β π) β π β Fin) |
| 12 | 11 | 3ad2ant2 1131 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π β Fin) |
| 13 | 6, 11 | anim12ci 613 |
. . . . . . . 8
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β (π β Fin β§ π
β Ring)) |
| 14 | 13 | 3adant3 1129 |
. . . . . . 7
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (π β Fin β§ π
β Ring)) |
| 15 | 1 | matring 22300 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
| 16 | 14, 15 | syl 17 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π΄ β Ring) |
| 17 | | slesolex.d |
. . . . . . . . . 10
β’ π· = (π maDet π
) |
| 18 | | eqid 2726 |
. . . . . . . . . 10
β’
(Unitβπ΄) =
(Unitβπ΄) |
| 19 | | eqid 2726 |
. . . . . . . . . 10
β’
(Unitβπ
) =
(Unitβπ
) |
| 20 | 1, 17, 8, 18, 19 | matunit 22535 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β π΅) β (π β (Unitβπ΄) β (π·βπ) β (Unitβπ
))) |
| 21 | 20 | bicomd 222 |
. . . . . . . 8
β’ ((π
β CRing β§ π β π΅) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
| 22 | 21 | ad2ant2lr 745 |
. . . . . . 7
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
| 23 | 22 | biimp3a 1465 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π β (Unitβπ΄)) |
| 24 | | eqid 2726 |
. . . . . . 7
β’
(invrβπ΄) = (invrβπ΄) |
| 25 | | eqid 2726 |
. . . . . . 7
β’
(Baseβπ΄) =
(Baseβπ΄) |
| 26 | 18, 24, 25 | ringinvcl 20294 |
. . . . . 6
β’ ((π΄ β Ring β§ π β (Unitβπ΄)) β
((invrβπ΄)βπ) β (Baseβπ΄)) |
| 27 | 16, 23, 26 | syl2anc 583 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β ((invrβπ΄)βπ) β (Baseβπ΄)) |
| 28 | | slesolex.v |
. . . . . . . . 9
β’ π = ((Baseβπ
) βm π) |
| 29 | 28 | eleq2i 2819 |
. . . . . . . 8
β’ (π β π β π β ((Baseβπ
) βm π)) |
| 30 | 29 | biimpi 215 |
. . . . . . 7
β’ (π β π β π β ((Baseβπ
) βm π)) |
| 31 | 30 | adantl 481 |
. . . . . 6
β’ ((π β π΅ β§ π β π) β π β ((Baseβπ
) βm π)) |
| 32 | 31 | 3ad2ant2 1131 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π β ((Baseβπ
) βm π)) |
| 33 | 1, 2, 3, 4, 7, 12,
27, 32 | mavmulcl 22404 |
. . . 4
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (((invrβπ΄)βπ) Β· π) β ((Baseβπ
) βm π)) |
| 34 | 33, 28 | eleqtrrdi 2838 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (((invrβπ΄)βπ) Β· π) β π) |
| 35 | 1, 8, 28, 2, 17, 24 | slesolinvbi 22538 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β ((π Β· π§) = π β π§ = (((invrβπ΄)βπ) Β· π))) |
| 36 | 35 | adantr 480 |
. . . . 5
β’ ((((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β§ ((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
))) β ((π Β· π§) = π β π§ = (((invrβπ΄)βπ) Β· π))) |
| 37 | 36 | biimprd 247 |
. . . 4
β’ ((((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β§ ((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
))) β (π§ = (((invrβπ΄)βπ) Β· π) β (π Β· π§) = π)) |
| 38 | 37 | impancom 451 |
. . 3
β’ ((((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β§ π§ = (((invrβπ΄)βπ) Β· π)) β (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (π Β· π§) = π)) |
| 39 | 34, 38 | rspcimedv 3597 |
. 2
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β βπ§ β π (π Β· π§) = π)) |
| 40 | 39 | pm2.43i 52 |
1
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β βπ§ β π (π Β· π§) = π) |
