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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matunit.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
matunit.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matunit.u ⊢ 𝑈 = ( Unit ‘ 𝐴 )
matunit.v ⊢ 𝑉 = ( Unit ‘ 𝑅 )
Assertion matunit ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑈 ↔ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 matunit.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matunit.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
3 matunit.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 matunit.u ⊢ 𝑈 = ( Unit ‘ 𝐴 )
5 matunit.v ⊢ 𝑉 = ( Unit ‘ 𝑅 )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
10 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
11 10 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → 𝑅 ∈ Ring )
12 2 1 3 6 mdetcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
13 12 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
14 2 1 3 6 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
15 14 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
16 1 3 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
17 16 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
18 17 ad2antlr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → 𝑁 ∈ Fin )
19 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
20 18 11 19 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → 𝐴 ∈ Ring )
21 eqid ⊢ ( invr ‘ 𝐴 ) = ( invr ‘ 𝐴 )
22 4 21 3 ringinvcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑀 ∈ 𝑈 ) → ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ∈ 𝐵 )
23 20 22 sylancom ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ∈ 𝐵 )
24 15 23 ffvelrnd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑅 ) )
25 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
26 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
27 4 21 25 26 unitrinv ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑀 ∈ 𝑈 ) → ( 𝑀 ( .r ‘ 𝐴 ) ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) = ( 1r ‘ 𝐴 ) )
28 20 27 sylancom ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝑀 ( .r ‘ 𝐴 ) ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) = ( 1r ‘ 𝐴 ) )
29 28 fveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ ( 𝑀 ( .r ‘ 𝐴 ) ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) = ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) )
30 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → 𝑅 ∈ CRing )
31 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → 𝑀 ∈ 𝐵 )
32 1 3 2 7 25 mdetmul ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑀 ( .r ‘ 𝐴 ) ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) = ( ( 𝐷 ‘ 𝑀 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) )
33 30 31 23 32 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ ( 𝑀 ( .r ‘ 𝐴 ) ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) = ( ( 𝐷 ‘ 𝑀 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) )
34 2 1 26 8 mdet1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
35 30 18 34 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
36 29 33 35 3eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( ( 𝐷 ‘ 𝑀 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) = ( 1r ‘ 𝑅 ) )
37 4 21 25 26 unitlinv ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑀 ∈ 𝑈 ) → ( ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) = ( 1r ‘ 𝐴 ) )
38 20 37 sylancom ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) = ( 1r ‘ 𝐴 ) )
39 38 fveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ ( ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) ) = ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) )
40 1 3 2 7 25 mdetmul ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ∈ 𝐵 ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) ) = ( ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑀 ) ) )
41 30 23 31 40 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ ( ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) ) = ( ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑀 ) ) )
42 39 41 35 3eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑀 ) ) = ( 1r ‘ 𝑅 ) )
43 6 7 8 5 9 11 13 24 36 42 invrvald ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ∧ ( ( invr ‘ 𝑅 ) ‘ ( 𝐷 ‘ 𝑀 ) ) = ( 𝐷 ‘ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) ) ) )
44 43 simpld ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑀 ∈ 𝑈 ) → ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 )
45 eqid ⊢ ( 𝑁 maAdju 𝑅 ) = ( 𝑁 maAdju 𝑅 )
46 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
47 1 45 2 3 4 5 9 21 46 matinv ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝑀 ∈ 𝑈 ∧ ( ( invr ‘ 𝐴 ) ‘ 𝑀 ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐷 ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝐴 ) ( ( 𝑁 maAdju 𝑅 ) ‘ 𝑀 ) ) ) )
48 47 simpld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑀 ∈ 𝑈 )
49 48 3expa ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑀 ∈ 𝑈 )
50 44 49 impbida ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑈 ↔ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) )