Step | Hyp | Ref
| Expression |
1 | | slesolex.a |
. . 3
β’ π΄ = (π Mat π
) |
2 | | eqid 2731 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | slesolex.x |
. . 3
β’ Β· =
(π
maVecMul β¨π, πβ©) |
4 | | crngring 20005 |
. . . . 5
β’ (π
β CRing β π
β Ring) |
5 | 4 | adantl 482 |
. . . 4
β’ ((π β β
β§ π
β CRing) β π
β Ring) |
6 | 5 | 3ad2ant1 1133 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π
β Ring) |
7 | | slesolex.b |
. . . . . . 7
β’ π΅ = (Baseβπ΄) |
8 | 1, 7 | matrcl 21811 |
. . . . . 6
β’ (π β π΅ β (π β Fin β§ π
β V)) |
9 | 8 | simpld 495 |
. . . . 5
β’ (π β π΅ β π β Fin) |
10 | 9 | adantr 481 |
. . . 4
β’ ((π β π΅ β§ π β π) β π β Fin) |
11 | 10 | 3ad2ant2 1134 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π β Fin) |
12 | 4 | anim2i 617 |
. . . . . . 7
β’ ((π β β
β§ π
β CRing) β (π β β
β§ π
β Ring)) |
13 | 12 | anim1i 615 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β ((π β β
β§ π
β Ring) β§ (π β π΅ β§ π β π))) |
14 | 13 | 3adant3 1132 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β ((π β β
β§ π
β Ring) β§ (π β π΅ β§ π β π))) |
15 | | simpr 485 |
. . . . . 6
β’ (((π·βπ) β (Unitβπ
) β§ (π Β· π) = π) β (π Β· π) = π) |
16 | 15 | 3ad2ant3 1135 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (π Β· π) = π) |
17 | | slesolex.v |
. . . . . 6
β’ π = ((Baseβπ
) βm π) |
18 | 1, 7, 17, 3 | slesolvec 22080 |
. . . . 5
β’ (((π β β
β§ π
β Ring) β§ (π β π΅ β§ π β π)) β ((π Β· π) = π β π β π)) |
19 | 14, 16, 18 | sylc 65 |
. . . 4
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π β π) |
20 | 19, 17 | eleqtrdi 2842 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π β ((Baseβπ
) βm π)) |
21 | | eqid 2731 |
. . 3
β’ (π
maMul β¨π, π, πβ©) = (π
maMul β¨π, π, πβ©) |
22 | 5, 10 | anim12ci 614 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β (π β Fin β§ π
β Ring)) |
23 | 22 | 3adant3 1132 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (π β Fin β§ π
β Ring)) |
24 | 1 | matring 21844 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
25 | 23, 24 | syl 17 |
. . . 4
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π΄ β Ring) |
26 | | slesolex.d |
. . . . . . . . . 10
β’ π· = (π maDet π
) |
27 | | eqid 2731 |
. . . . . . . . . 10
β’
(Unitβπ΄) =
(Unitβπ΄) |
28 | | eqid 2731 |
. . . . . . . . . 10
β’
(Unitβπ
) =
(Unitβπ
) |
29 | 1, 26, 7, 27, 28 | matunit 22079 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β π΅) β (π β (Unitβπ΄) β (π·βπ) β (Unitβπ
))) |
30 | 29 | bicomd 222 |
. . . . . . . 8
β’ ((π
β CRing β§ π β π΅) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
31 | 30 | ad2ant2lr 746 |
. . . . . . 7
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
32 | 31 | biimpd 228 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β ((π·βπ) β (Unitβπ
) β π β (Unitβπ΄))) |
33 | 32 | adantrd 492 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β (((π·βπ) β (Unitβπ
) β§ (π Β· π) = π) β π β (Unitβπ΄))) |
34 | 33 | 3impia 1117 |
. . . 4
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π β (Unitβπ΄)) |
35 | | slesolinv.i |
. . . . 5
β’ πΌ = (invrβπ΄) |
36 | | eqid 2731 |
. . . . 5
β’
(Baseβπ΄) =
(Baseβπ΄) |
37 | 27, 35, 36 | ringinvcl 20134 |
. . . 4
β’ ((π΄ β Ring β§ π β (Unitβπ΄)) β (πΌβπ) β (Baseβπ΄)) |
38 | 25, 34, 37 | syl2anc 584 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (πΌβπ) β (Baseβπ΄)) |
39 | 7 | eleq2i 2824 |
. . . . . 6
β’ (π β π΅ β π β (Baseβπ΄)) |
40 | 39 | biimpi 215 |
. . . . 5
β’ (π β π΅ β π β (Baseβπ΄)) |
41 | 40 | adantr 481 |
. . . 4
β’ ((π β π΅ β§ π β π) β π β (Baseβπ΄)) |
42 | 41 | 3ad2ant2 1134 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π β (Baseβπ΄)) |
43 | 1, 2, 3, 6, 11, 20, 21, 38, 42 | mavmulass 21950 |
. 2
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (((πΌβπ)(π
maMul β¨π, π, πβ©)π) Β· π) = ((πΌβπ) Β· (π Β· π))) |
44 | | simpr 485 |
. . . . . . . . 9
β’ ((π β β
β§ π
β CRing) β π
β CRing) |
45 | 44, 10 | anim12ci 614 |
. . . . . . . 8
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π)) β (π β Fin β§ π
β CRing)) |
46 | 45 | 3adant3 1132 |
. . . . . . 7
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (π β Fin β§ π
β CRing)) |
47 | 1, 21 | matmulr 21839 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
48 | 46, 47 | syl 17 |
. . . . . 6
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
49 | 48 | oveqd 7394 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β ((πΌβπ)(π
maMul β¨π, π, πβ©)π) = ((πΌβπ)(.rβπ΄)π)) |
50 | | eqid 2731 |
. . . . . . 7
β’
(.rβπ΄) = (.rβπ΄) |
51 | | eqid 2731 |
. . . . . . 7
β’
(1rβπ΄) = (1rβπ΄) |
52 | 27, 35, 50, 51 | unitlinv 20135 |
. . . . . 6
β’ ((π΄ β Ring β§ π β (Unitβπ΄)) β ((πΌβπ)(.rβπ΄)π) = (1rβπ΄)) |
53 | 25, 34, 52 | syl2anc 584 |
. . . . 5
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β ((πΌβπ)(.rβπ΄)π) = (1rβπ΄)) |
54 | 49, 53 | eqtrd 2771 |
. . . 4
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β ((πΌβπ)(π
maMul β¨π, π, πβ©)π) = (1rβπ΄)) |
55 | 54 | oveq1d 7392 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (((πΌβπ)(π
maMul β¨π, π, πβ©)π) Β· π) = ((1rβπ΄) Β· π)) |
56 | 1, 2, 3, 6, 11, 20 | 1mavmul 21949 |
. . 3
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β ((1rβπ΄) Β· π) = π) |
57 | 55, 56 | eqtrd 2771 |
. 2
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β (((πΌβπ)(π
maMul β¨π, π, πβ©)π) Β· π) = π) |
58 | | oveq2 7385 |
. . . 4
β’ ((π Β· π) = π β ((πΌβπ) Β· (π Β· π)) = ((πΌβπ) Β· π)) |
59 | 58 | adantl 482 |
. . 3
β’ (((π·βπ) β (Unitβπ
) β§ (π Β· π) = π) β ((πΌβπ) Β· (π Β· π)) = ((πΌβπ) Β· π)) |
60 | 59 | 3ad2ant3 1135 |
. 2
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β ((πΌβπ) Β· (π Β· π)) = ((πΌβπ) Β· π)) |
61 | 43, 57, 60 | 3eqtr3d 2779 |
1
β’ (((π β β
β§ π
β CRing) β§ (π β π΅ β§ π β π) β§ ((π·βπ) β (Unitβπ
) β§ (π Β· π) = π)) β π = ((πΌβπ) Β· π)) |