Metamath Proof Explorer

Theorem matunit

Description: A matrix is a unit in the ring of matrices iff its determinant is a unit in the underlying ring. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses matunit.a 
|- A = ( N Mat R )
matunit.d 
|- D = ( N maDet R )
matunit.b 
|- B = ( Base ` A )
matunit.u 
|- U = ( Unit ` A )
matunit.v 
|- V = ( Unit ` R )
Assertion matunit 
|- ( ( R e. CRing /\ M e. B ) -> ( M e. U <-> ( D ` M ) e. V ) )

Proof

Step Hyp Ref Expression
1 matunit.a 
 |-  A = ( N Mat R )
2 matunit.d 
 |-  D = ( N maDet R )
3 matunit.b 
 |-  B = ( Base ` A )
4 matunit.u 
 |-  U = ( Unit ` A )
5 matunit.v 
 |-  V = ( Unit ` R )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 eqid 
 |-  ( invr ` R ) = ( invr ` R )
10 crngring 
 |-  ( R e. CRing -> R e. Ring )
11 10 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> R e. Ring )
12 2 1 3 6 mdetcl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( D ` M ) e. ( Base ` R ) )
13 12 adantr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` M ) e. ( Base ` R ) )
14 2 1 3 6 mdetf 
 |-  ( R e. CRing -> D : B --> ( Base ` R ) )
15 14 ad2antrr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> D : B --> ( Base ` R ) )
16 1 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
17 16 simpld 
 |-  ( M e. B -> N e. Fin )
18 17 ad2antlr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> N e. Fin )
19 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
20 18 11 19 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> A e. Ring )
21 eqid 
 |-  ( invr ` A ) = ( invr ` A )
22 4 21 3 ringinvcl 
 |-  ( ( A e. Ring /\ M e. U ) -> ( ( invr ` A ) ` M ) e. B )
23 20 22 sylancom 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( ( invr ` A ) ` M ) e. B )
24 15 23 ffvelcdmd 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` ( ( invr ` A ) ` M ) ) e. ( Base ` R ) )
25 eqid 
 |-  ( .r ` A ) = ( .r ` A )
26 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
27 4 21 25 26 unitrinv 
 |-  ( ( A e. Ring /\ M e. U ) -> ( M ( .r ` A ) ( ( invr ` A ) ` M ) ) = ( 1r ` A ) )
28 20 27 sylancom 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( M ( .r ` A ) ( ( invr ` A ) ` M ) ) = ( 1r ` A ) )
29 28 fveq2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` ( M ( .r ` A ) ( ( invr ` A ) ` M ) ) ) = ( D ` ( 1r ` A ) ) )
30 simpll 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> R e. CRing )
31 simplr 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> M e. B )
32 1 3 2 7 25 mdetmul 
 |-  ( ( R e. CRing /\ M e. B /\ ( ( invr ` A ) ` M ) e. B ) -> ( D ` ( M ( .r ` A ) ( ( invr ` A ) ` M ) ) ) = ( ( D ` M ) ( .r ` R ) ( D ` ( ( invr ` A ) ` M ) ) ) )
33 30 31 23 32 syl3anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` ( M ( .r ` A ) ( ( invr ` A ) ` M ) ) ) = ( ( D ` M ) ( .r ` R ) ( D ` ( ( invr ` A ) ` M ) ) ) )
34 2 1 26 8 mdet1 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( D ` ( 1r ` A ) ) = ( 1r ` R ) )
35 30 18 34 syl2anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` ( 1r ` A ) ) = ( 1r ` R ) )
36 29 33 35 3eqtr3d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( ( D ` M ) ( .r ` R ) ( D ` ( ( invr ` A ) ` M ) ) ) = ( 1r ` R ) )
37 4 21 25 26 unitlinv 
 |-  ( ( A e. Ring /\ M e. U ) -> ( ( ( invr ` A ) ` M ) ( .r ` A ) M ) = ( 1r ` A ) )
38 20 37 sylancom 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( ( ( invr ` A ) ` M ) ( .r ` A ) M ) = ( 1r ` A ) )
39 38 fveq2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` ( ( ( invr ` A ) ` M ) ( .r ` A ) M ) ) = ( D ` ( 1r ` A ) ) )
40 1 3 2 7 25 mdetmul 
 |-  ( ( R e. CRing /\ ( ( invr ` A ) ` M ) e. B /\ M e. B ) -> ( D ` ( ( ( invr ` A ) ` M ) ( .r ` A ) M ) ) = ( ( D ` ( ( invr ` A ) ` M ) ) ( .r ` R ) ( D ` M ) ) )
41 30 23 31 40 syl3anc 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` ( ( ( invr ` A ) ` M ) ( .r ` A ) M ) ) = ( ( D ` ( ( invr ` A ) ` M ) ) ( .r ` R ) ( D ` M ) ) )
42 39 41 35 3eqtr3d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( ( D ` ( ( invr ` A ) ` M ) ) ( .r ` R ) ( D ` M ) ) = ( 1r ` R ) )
43 6 7 8 5 9 11 13 24 36 42 invrvald 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( ( D ` M ) e. V /\ ( ( invr ` R ) ` ( D ` M ) ) = ( D ` ( ( invr ` A ) ` M ) ) ) )
44 43 simpld 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ M e. U ) -> ( D ` M ) e. V )
45 eqid 
 |-  ( N maAdju R ) = ( N maAdju R )
46 eqid 
 |-  ( .s ` A ) = ( .s ` A )
47 1 45 2 3 4 5 9 21 46 matinv 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M e. U /\ ( ( invr ` A ) ` M ) = ( ( ( invr ` R ) ` ( D ` M ) ) ( .s ` A ) ( ( N maAdju R ) ` M ) ) ) )
48 47 simpld 
 |-  ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> M e. U )
49 48 3expa 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ ( D ` M ) e. V ) -> M e. U )
50 44 49 impbida 
 |-  ( ( R e. CRing /\ M e. B ) -> ( M e. U <-> ( D ` M ) e. V ) )