Step |
Hyp |
Ref |
Expression |
1 |
|
slesolex.a |
|- A = ( N Mat R ) |
2 |
|
slesolex.b |
|- B = ( Base ` A ) |
3 |
|
slesolex.v |
|- V = ( ( Base ` R ) ^m N ) |
4 |
|
slesolex.x |
|- .x. = ( R maVecMul <. N , N >. ) |
5 |
|
slesolex.d |
|- D = ( N maDet R ) |
6 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
7 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
8 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
9 |
8
|
adantl |
|- ( ( N =/= (/) /\ R e. CRing ) -> R e. Ring ) |
10 |
9
|
3ad2ant1 |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> R e. Ring ) |
11 |
1 2
|
matrcl |
|- ( X e. B -> ( N e. Fin /\ R e. _V ) ) |
12 |
11
|
simpld |
|- ( X e. B -> N e. Fin ) |
13 |
12
|
adantr |
|- ( ( X e. B /\ Y e. V ) -> N e. Fin ) |
14 |
13
|
3ad2ant2 |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> N e. Fin ) |
15 |
9 13
|
anim12ci |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. Ring ) ) |
16 |
15
|
3adant3 |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( N e. Fin /\ R e. Ring ) ) |
17 |
1
|
matring |
|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring ) |
18 |
16 17
|
syl |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A e. Ring ) |
19 |
|
eqid |
|- ( Unit ` A ) = ( Unit ` A ) |
20 |
|
eqid |
|- ( Unit ` R ) = ( Unit ` R ) |
21 |
1 5 2 19 20
|
matunit |
|- ( ( R e. CRing /\ X e. B ) -> ( X e. ( Unit ` A ) <-> ( D ` X ) e. ( Unit ` R ) ) ) |
22 |
21
|
bicomd |
|- ( ( R e. CRing /\ X e. B ) -> ( ( D ` X ) e. ( Unit ` R ) <-> X e. ( Unit ` A ) ) ) |
23 |
22
|
ad2ant2lr |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( ( D ` X ) e. ( Unit ` R ) <-> X e. ( Unit ` A ) ) ) |
24 |
23
|
biimp3a |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> X e. ( Unit ` A ) ) |
25 |
|
eqid |
|- ( invr ` A ) = ( invr ` A ) |
26 |
|
eqid |
|- ( Base ` A ) = ( Base ` A ) |
27 |
19 25 26
|
ringinvcl |
|- ( ( A e. Ring /\ X e. ( Unit ` A ) ) -> ( ( invr ` A ) ` X ) e. ( Base ` A ) ) |
28 |
18 24 27
|
syl2anc |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( invr ` A ) ` X ) e. ( Base ` A ) ) |
29 |
3
|
eleq2i |
|- ( Y e. V <-> Y e. ( ( Base ` R ) ^m N ) ) |
30 |
29
|
biimpi |
|- ( Y e. V -> Y e. ( ( Base ` R ) ^m N ) ) |
31 |
30
|
adantl |
|- ( ( X e. B /\ Y e. V ) -> Y e. ( ( Base ` R ) ^m N ) ) |
32 |
31
|
3ad2ant2 |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> Y e. ( ( Base ` R ) ^m N ) ) |
33 |
1 4 6 7 10 14 28 32
|
mavmulcl |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( invr ` A ) ` X ) .x. Y ) e. ( ( Base ` R ) ^m N ) ) |
34 |
33 3
|
eleqtrrdi |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( invr ` A ) ` X ) .x. Y ) e. V ) |
35 |
1 2 3 4 5 25
|
slesolinvbi |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( X .x. z ) = Y <-> z = ( ( ( invr ` A ) ` X ) .x. Y ) ) ) |
36 |
35
|
adantr |
|- ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( X .x. z ) = Y <-> z = ( ( ( invr ` A ) ` X ) .x. Y ) ) ) |
37 |
36
|
biimprd |
|- ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( z = ( ( ( invr ` A ) ` X ) .x. Y ) -> ( X .x. z ) = Y ) ) |
38 |
37
|
impancom |
|- ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z = ( ( ( invr ` A ) ` X ) .x. Y ) ) -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X .x. z ) = Y ) ) |
39 |
34 38
|
rspcimedv |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> E. z e. V ( X .x. z ) = Y ) ) |
40 |
39
|
pm2.43i |
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> E. z e. V ( X .x. z ) = Y ) |