Step |
Hyp |
Ref |
Expression |
1 |
|
slesolex.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
slesolex.b |
โข ๐ต = ( Base โ ๐ด ) |
3 |
|
slesolex.v |
โข ๐ = ( ( Base โ ๐
) โm ๐ ) |
4 |
|
slesolex.x |
โข ยท = ( ๐
maVecMul โจ ๐ , ๐ โฉ ) |
5 |
|
slesolex.d |
โข ๐ท = ( ๐ maDet ๐
) |
6 |
|
slesolinv.i |
โข ๐ผ = ( invr โ ๐ด ) |
7 |
|
simpl1 |
โข ( ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โง ( ๐ ยท ๐ ) = ๐ ) โ ( ๐ โ โ
โง ๐
โ CRing ) ) |
8 |
|
simpl2 |
โข ( ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โง ( ๐ ยท ๐ ) = ๐ ) โ ( ๐ โ ๐ต โง ๐ โ ๐ ) ) |
9 |
|
simp3 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) |
10 |
9
|
anim1i |
โข ( ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โง ( ๐ ยท ๐ ) = ๐ ) โ ( ( ๐ท โ ๐ ) โ ( Unit โ ๐
) โง ( ๐ ยท ๐ ) = ๐ ) ) |
11 |
1 2 3 4 5 6
|
slesolinv |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ( ๐ท โ ๐ ) โ ( Unit โ ๐
) โง ( ๐ ยท ๐ ) = ๐ ) ) โ ๐ = ( ( ๐ผ โ ๐ ) ยท ๐ ) ) |
12 |
7 8 10 11
|
syl3anc |
โข ( ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โง ( ๐ ยท ๐ ) = ๐ ) โ ๐ = ( ( ๐ผ โ ๐ ) ยท ๐ ) ) |
13 |
|
oveq2 |
โข ( ๐ = ( ( ๐ผ โ ๐ ) ยท ๐ ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ( ( ๐ผ โ ๐ ) ยท ๐ ) ) ) |
14 |
|
simpr |
โข ( ( ๐ โ โ
โง ๐
โ CRing ) โ ๐
โ CRing ) |
15 |
1 2
|
matrcl |
โข ( ๐ โ ๐ต โ ( ๐ โ Fin โง ๐
โ V ) ) |
16 |
15
|
simpld |
โข ( ๐ โ ๐ต โ ๐ โ Fin ) |
17 |
16
|
adantr |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ ) โ ๐ โ Fin ) |
18 |
14 17
|
anim12ci |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) ) โ ( ๐ โ Fin โง ๐
โ CRing ) ) |
19 |
18
|
3adant3 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ โ Fin โง ๐
โ CRing ) ) |
20 |
|
eqid |
โข ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) = ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) |
21 |
1 20
|
matmulr |
โข ( ( ๐ โ Fin โง ๐
โ CRing ) โ ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) = ( .r โ ๐ด ) ) |
22 |
19 21
|
syl |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) = ( .r โ ๐ด ) ) |
23 |
22
|
oveqd |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) ( ๐ผ โ ๐ ) ) = ( ๐ ( .r โ ๐ด ) ( ๐ผ โ ๐ ) ) ) |
24 |
|
crngring |
โข ( ๐
โ CRing โ ๐
โ Ring ) |
25 |
24
|
adantl |
โข ( ( ๐ โ โ
โง ๐
โ CRing ) โ ๐
โ Ring ) |
26 |
25 17
|
anim12ci |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) ) โ ( ๐ โ Fin โง ๐
โ Ring ) ) |
27 |
26
|
3adant3 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ โ Fin โง ๐
โ Ring ) ) |
28 |
1
|
matring |
โข ( ( ๐ โ Fin โง ๐
โ Ring ) โ ๐ด โ Ring ) |
29 |
27 28
|
syl |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ๐ด โ Ring ) |
30 |
|
eqid |
โข ( Unit โ ๐ด ) = ( Unit โ ๐ด ) |
31 |
|
eqid |
โข ( Unit โ ๐
) = ( Unit โ ๐
) |
32 |
1 5 2 30 31
|
matunit |
โข ( ( ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ โ ( Unit โ ๐ด ) โ ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) ) |
33 |
32
|
ad2ant2lr |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) ) โ ( ๐ โ ( Unit โ ๐ด ) โ ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) ) |
34 |
33
|
biimp3ar |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ๐ โ ( Unit โ ๐ด ) ) |
35 |
|
eqid |
โข ( .r โ ๐ด ) = ( .r โ ๐ด ) |
36 |
|
eqid |
โข ( 1r โ ๐ด ) = ( 1r โ ๐ด ) |
37 |
30 6 35 36
|
unitrinv |
โข ( ( ๐ด โ Ring โง ๐ โ ( Unit โ ๐ด ) ) โ ( ๐ ( .r โ ๐ด ) ( ๐ผ โ ๐ ) ) = ( 1r โ ๐ด ) ) |
38 |
29 34 37
|
syl2anc |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ ( .r โ ๐ด ) ( ๐ผ โ ๐ ) ) = ( 1r โ ๐ด ) ) |
39 |
23 38
|
eqtrd |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) ( ๐ผ โ ๐ ) ) = ( 1r โ ๐ด ) ) |
40 |
39
|
oveq1d |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ( ๐ ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) ( ๐ผ โ ๐ ) ) ยท ๐ ) = ( ( 1r โ ๐ด ) ยท ๐ ) ) |
41 |
|
eqid |
โข ( Base โ ๐
) = ( Base โ ๐
) |
42 |
25
|
3ad2ant1 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ๐
โ Ring ) |
43 |
17
|
3ad2ant2 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ๐ โ Fin ) |
44 |
3
|
eleq2i |
โข ( ๐ โ ๐ โ ๐ โ ( ( Base โ ๐
) โm ๐ ) ) |
45 |
44
|
biimpi |
โข ( ๐ โ ๐ โ ๐ โ ( ( Base โ ๐
) โm ๐ ) ) |
46 |
45
|
adantl |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ ) โ ๐ โ ( ( Base โ ๐
) โm ๐ ) ) |
47 |
46
|
3ad2ant2 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ๐ โ ( ( Base โ ๐
) โm ๐ ) ) |
48 |
2
|
eleq2i |
โข ( ๐ โ ๐ต โ ๐ โ ( Base โ ๐ด ) ) |
49 |
48
|
biimpi |
โข ( ๐ โ ๐ต โ ๐ โ ( Base โ ๐ด ) ) |
50 |
49
|
adantr |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ ) โ ๐ โ ( Base โ ๐ด ) ) |
51 |
50
|
3ad2ant2 |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ๐ โ ( Base โ ๐ด ) ) |
52 |
|
eqid |
โข ( Base โ ๐ด ) = ( Base โ ๐ด ) |
53 |
30 6 52
|
ringinvcl |
โข ( ( ๐ด โ Ring โง ๐ โ ( Unit โ ๐ด ) ) โ ( ๐ผ โ ๐ ) โ ( Base โ ๐ด ) ) |
54 |
29 34 53
|
syl2anc |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ผ โ ๐ ) โ ( Base โ ๐ด ) ) |
55 |
1 41 4 42 43 47 20 51 54
|
mavmulass |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ( ๐ ( ๐
maMul โจ ๐ , ๐ , ๐ โฉ ) ( ๐ผ โ ๐ ) ) ยท ๐ ) = ( ๐ ยท ( ( ๐ผ โ ๐ ) ยท ๐ ) ) ) |
56 |
1 41 4 42 43 47
|
1mavmul |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ( 1r โ ๐ด ) ยท ๐ ) = ๐ ) |
57 |
40 55 56
|
3eqtr3d |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ๐ ยท ( ( ๐ผ โ ๐ ) ยท ๐ ) ) = ๐ ) |
58 |
13 57
|
sylan9eqr |
โข ( ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โง ๐ = ( ( ๐ผ โ ๐ ) ยท ๐ ) ) โ ( ๐ ยท ๐ ) = ๐ ) |
59 |
12 58
|
impbida |
โข ( ( ( ๐ โ โ
โง ๐
โ CRing ) โง ( ๐ โ ๐ต โง ๐ โ ๐ ) โง ( ๐ท โ ๐ ) โ ( Unit โ ๐
) ) โ ( ( ๐ ยท ๐ ) = ๐ โ ๐ = ( ( ๐ผ โ ๐ ) ยท ๐ ) ) ) |