Step | Hyp | Ref
| Expression |
1 | | slesolex.a |
. . . . 5
β’ π΄ = (π Mat π
) |
2 | | slesolex.x |
. . . . 5
β’ Β· =
(π
maVecMul β¨π, πβ©) |
3 | | eqid 2736 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
4 | | eqid 2736 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
5 | | crngring 19974 |
. . . . . . 7
β’ (π
β CRing β π
β Ring) |
6 | 5 | adantl 482 |
. . . . . 6
β’ ((π β β
β§ π
β CRing) β π
β Ring) |
7 | 6 | 3ad2ant1 1133 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π
β Ring) |
8 | | slesolex.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ΄) |
9 | 1, 8 | matrcl 21757 |
. . . . . . . 8
β’ (π β π΅ β (π β Fin β§ π
β V)) |
10 | 9 | simpld 495 |
. . . . . . 7
β’ (π β π΅ β π β Fin) |
11 | 10 | adantr 481 |
. . . . . 6
β’ ((π β π΅ β§ π β π) β π β Fin) |
12 | 11 | 3ad2ant2 1134 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π β Fin) |
13 | 6, 11 | anim12ci 614 |
. . . . . . . 8
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β (π β Fin β§ π
β Ring)) |
14 | 13 | 3adant3 1132 |
. . . . . . 7
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (π β Fin β§ π
β Ring)) |
15 | 1 | matring 21790 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π΄ β Ring) |
17 | | slesolex.d |
. . . . . . . . . 10
β’ π· = (π maDet π
) |
18 | | eqid 2736 |
. . . . . . . . . 10
β’
(Unitβπ΄) =
(Unitβπ΄) |
19 | | eqid 2736 |
. . . . . . . . . 10
β’
(Unitβπ
) =
(Unitβπ
) |
20 | 1, 17, 8, 18, 19 | matunit 22025 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β π΅) β (π β (Unitβπ΄) β (π·βπ) β (Unitβπ
))) |
21 | 20 | bicomd 222 |
. . . . . . . 8
β’ ((π
β CRing β§ π β π΅) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
22 | 21 | ad2ant2lr 746 |
. . . . . . 7
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
23 | 22 | biimp3a 1469 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π β (Unitβπ΄)) |
24 | | eqid 2736 |
. . . . . . 7
β’
(invrβπ΄) = (invrβπ΄) |
25 | | eqid 2736 |
. . . . . . 7
β’
(Baseβπ΄) =
(Baseβπ΄) |
26 | 18, 24, 25 | ringinvcl 20103 |
. . . . . 6
β’ ((π΄ β Ring β§ π β (Unitβπ΄)) β
((invrβπ΄)βπ) β (Baseβπ΄)) |
27 | 16, 23, 26 | syl2anc 584 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β ((invrβπ΄)βπ) β (Baseβπ΄)) |
28 | | slesolex.v |
. . . . . . . . 9
β’ π = ((Baseβπ
) βm π) |
29 | 28 | eleq2i 2829 |
. . . . . . . 8
β’ (π β π β π β ((Baseβπ
) βm π)) |
30 | 29 | biimpi 215 |
. . . . . . 7
β’ (π β π β π β ((Baseβπ
) βm π)) |
31 | 30 | adantl 482 |
. . . . . 6
β’ ((π β π΅ β§ π β π) β π β ((Baseβπ
) βm π)) |
32 | 31 | 3ad2ant2 1134 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β π β ((Baseβπ
) βm π)) |
33 | 1, 2, 3, 4, 7, 12,
27, 32 | mavmulcl 21894 |
. . . 4
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (((invrβπ΄)βπ) Β· π) β ((Baseβπ
) βm π)) |
34 | 33, 28 | eleqtrrdi 2849 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (((invrβπ΄)βπ) Β· π) β π) |
35 | 1, 8, 28, 2, 17, 24 | slesolinvbi 22028 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β ((π Β· π§) = π β π§ = (((invrβπ΄)βπ) Β· π))) |
36 | 35 | adantr 481 |
. . . . 5
β’ ((((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β§ ((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
))) β ((π Β· π§) = π β π§ = (((invrβπ΄)βπ) Β· π))) |
37 | 36 | biimprd 247 |
. . . 4
β’ ((((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β§ ((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
))) β (π§ = (((invrβπ΄)βπ) Β· π) β (π Β· π§) = π)) |
38 | 37 | impancom 452 |
. . 3
β’ ((((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β§ π§ = (((invrβπ΄)βπ) Β· π)) β (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (π Β· π§) = π)) |
39 | 34, 38 | rspcimedv 3572 |
. 2
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β βπ§ β π (π Β· π§) = π)) |
40 | 39 | pm2.43i 52 |
1
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ (π·βπ) β (Unitβπ
)) β βπ§ β π (π Β· π§) = π) |