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 \in CRing \land M \in B) \to (M \in U \leftrightarrow D (M) \in 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	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ 1_{R} = 1_{R}$
9		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
10		crngring	$⊢ R \in CRing \to R \in Ring$
11	10	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to R \in Ring$
12	2 1 3 6	mdetcl	$⊢ (R \in CRing \land M \in B) \to D (M) \in {Base}_{R}$
13	12	adantr	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D (M) \in {Base}_{R}$
14	2 1 3 6	mdetf	$⊢ R \in CRing \to D : B ⟶ {Base}_{R}$
15	14	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D : B ⟶ {Base}_{R}$
16	1 3	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
17	16	simpld	$⊢ M \in B \to N \in Fin$
18	17	ad2antlr	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to N \in Fin$
19	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
20	18 11 19	syl2anc	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to A \in Ring$
21		eqid	$⊢ {inv}_{r} (A) = {inv}_{r} (A)$
22	4 21 3	ringinvcl	$⊢ (A \in Ring \land M \in U) \to {inv}_{r} (A) (M) \in B$
23	20 22	sylancom	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to {inv}_{r} (A) (M) \in B$
24	15 23	ffvelcdmd	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D ({inv}_{r} (A) (M)) \in {Base}_{R}$
25		eqid	$⊢ \cdot_{A} = \cdot_{A}$
26		eqid	$⊢ 1_{A} = 1_{A}$
27	4 21 25 26	unitrinv	$⊢ (A \in Ring \land M \in U) \to M \cdot_{A} {inv}_{r} (A) (M) = 1_{A}$
28	20 27	sylancom	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to M \cdot_{A} {inv}_{r} (A) (M) = 1_{A}$
29	28	fveq2d	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D (M \cdot_{A} {inv}_{r} (A) (M)) = D (1_{A})$
30		simpll	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to R \in CRing$
31		simplr	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to M \in B$
32	1 3 2 7 25	mdetmul	$⊢ (R \in CRing \land M \in B \land {inv}_{r} (A) (M) \in B) \to D (M \cdot_{A} {inv}_{r} (A) (M)) = D (M) \cdot_{R} D ({inv}_{r} (A) (M))$
33	30 31 23 32	syl3anc	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D (M \cdot_{A} {inv}_{r} (A) (M)) = D (M) \cdot_{R} D ({inv}_{r} (A) (M))$
34	2 1 26 8	mdet1	$⊢ (R \in CRing \land N \in Fin) \to D (1_{A}) = 1_{R}$
35	30 18 34	syl2anc	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D (1_{A}) = 1_{R}$
36	29 33 35	3eqtr3d	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D (M) \cdot_{R} D ({inv}_{r} (A) (M)) = 1_{R}$
37	4 21 25 26	unitlinv	$⊢ (A \in Ring \land M \in U) \to {inv}_{r} (A) (M) \cdot_{A} M = 1_{A}$
38	20 37	sylancom	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to {inv}_{r} (A) (M) \cdot_{A} M = 1_{A}$
39	38	fveq2d	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D ({inv}_{r} (A) (M) \cdot_{A} M) = D (1_{A})$
40	1 3 2 7 25	mdetmul	$⊢ (R \in CRing \land {inv}_{r} (A) (M) \in B \land M \in B) \to D ({inv}_{r} (A) (M) \cdot_{A} M) = D ({inv}_{r} (A) (M)) \cdot_{R} D (M)$
41	30 23 31 40	syl3anc	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D ({inv}_{r} (A) (M) \cdot_{A} M) = D ({inv}_{r} (A) (M)) \cdot_{R} D (M)$
42	39 41 35	3eqtr3d	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D ({inv}_{r} (A) (M)) \cdot_{R} D (M) = 1_{R}$
43	6 7 8 5 9 11 13 24 36 42	invrvald	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to (D (M) \in V \land {inv}_{r} (R) (D (M)) = D ({inv}_{r} (A) (M)))$
44	43	simpld	$⊢ ((R \in CRing \land M \in B) \land M \in U) \to D (M) \in V$
45		eqid	$⊢ N maAdju R = N maAdju R$
46		eqid	$⊢ \cdot_{A} = \cdot_{A}$
47	1 45 2 3 4 5 9 21 46	matinv	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (M \in U \land {inv}_{r} (A) (M) = {inv}_{r} (R) (D (M)) \cdot_{A} (N maAdju R) (M))$
48	47	simpld	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to M \in U$
49	48	3expa	$⊢ ((R \in CRing \land M \in B) \land D (M) \in V) \to M \in U$
50	44 49	impbida	$⊢ (R \in CRing \land M \in B) \to (M \in U \leftrightarrow D (M) \in V)$

Metamath Proof Explorer

Theorem matunit

Proof