matinv

Description: The inverse of a matrix is the adjunct of the matrix multiplied with the inverse of the determinant of the matrix if the determinant is a unit in the underlying ring. Proposition 4.16 in Lang p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018)

	Ref	Expression
Hypotheses	matinv.a	$⊢ A = N Mat R$
	matinv.j	$⊢ J = N maAdju R$
	matinv.d	$⊢ D = N maDet R$
	matinv.b	$⊢ B = {Base}_{A}$
	matinv.u	$⊢ U = Unit (A)$
	matinv.v	$⊢ V = Unit (R)$
	matinv.h	$⊢ H = {inv}_{r} (R)$
	matinv.i	$⊢ I = {inv}_{r} (A)$
	matinv.t	$⊢ \underset{˙}{∙} = \cdot_{A}$
Assertion	matinv	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (M \in U \land I (M) = H (D (M)) \underset{˙}{∙} J (M))$

Proof

Step	Hyp	Ref	Expression
1		matinv.a	$⊢ A = N Mat R$
2		matinv.j	$⊢ J = N maAdju R$
3		matinv.d	$⊢ D = N maDet R$
4		matinv.b	$⊢ B = {Base}_{A}$
5		matinv.u	$⊢ U = Unit (A)$
6		matinv.v	$⊢ V = Unit (R)$
7		matinv.h	$⊢ H = {inv}_{r} (R)$
8		matinv.i	$⊢ I = {inv}_{r} (A)$
9		matinv.t	$⊢ \underset{˙}{∙} = \cdot_{A}$
10		eqid	$⊢ \cdot_{A} = \cdot_{A}$
11		eqid	$⊢ 1_{A} = 1_{A}$
12	1 4	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
13	12	simpld	$⊢ M \in B \to N \in Fin$
14	13	3ad2ant2	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to N \in Fin$
15		simp1	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to R \in CRing$
16	1	matassa	$⊢ (N \in Fin \land R \in CRing) \to A \in AssAlg$
17	14 15 16	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to A \in AssAlg$
18		assaring	$⊢ A \in AssAlg \to A \in Ring$
19	17 18	syl	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to A \in Ring$
20		simp2	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to M \in B$
21		assalmod	$⊢ A \in AssAlg \to A \in LMod$
22	17 21	syl	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to A \in LMod$
23		crngring	$⊢ R \in CRing \to R \in Ring$
24	23	3ad2ant1	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to R \in Ring$
25		simp3	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to D (M) \in V$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27	6 7 26	ringinvcl	$⊢ (R \in Ring \land D (M) \in V) \to H (D (M)) \in {Base}_{R}$
28	24 25 27	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \in {Base}_{R}$
29	1	matsca2	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (A)$
30	14 15 29	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to R = Scalar (A)$
31	30	fveq2d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to {Base}_{R} = {Base}_{Scalar (A)}$
32	28 31	eleqtrd	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \in {Base}_{Scalar (A)}$
33	1 2 4	maduf	$⊢ R \in CRing \to J : B ⟶ B$
34	33	3ad2ant1	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to J : B ⟶ B$
35	34 20	ffvelcdmd	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to J (M) \in B$
36		eqid	$⊢ Scalar (A) = Scalar (A)$
37		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
38	4 36 9 37	lmodvscl	$⊢ (A \in LMod \land H (D (M)) \in {Base}_{Scalar (A)} \land J (M) \in B) \to H (D (M)) \underset{˙}{∙} J (M) \in B$
39	22 32 35 38	syl3anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \underset{˙}{∙} J (M) \in B$
40	4 36 37 9 10	assaassr	$⊢ (A \in AssAlg \land (H (D (M)) \in {Base}_{Scalar (A)} \land M \in B \land J (M) \in B)) \to M \cdot_{A} (H (D (M)) \underset{˙}{∙} J (M)) = H (D (M)) \underset{˙}{∙} (M \cdot_{A} J (M))$
41	17 32 20 35 40	syl13anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to M \cdot_{A} (H (D (M)) \underset{˙}{∙} J (M)) = H (D (M)) \underset{˙}{∙} (M \cdot_{A} J (M))$
42	1 4 2 3 11 10 9	madurid	$⊢ (M \in B \land R \in CRing) \to M \cdot_{A} J (M) = D (M) \underset{˙}{∙} 1_{A}$
43	20 15 42	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to M \cdot_{A} J (M) = D (M) \underset{˙}{∙} 1_{A}$
44	43	oveq2d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \underset{˙}{∙} (M \cdot_{A} J (M)) = H (D (M)) \underset{˙}{∙} (D (M) \underset{˙}{∙} 1_{A})$
45		eqid	$⊢ \cdot_{R} = \cdot_{R}$
46		eqid	$⊢ 1_{R} = 1_{R}$
47	6 7 45 46	unitlinv	$⊢ (R \in Ring \land D (M) \in V) \to H (D (M)) \cdot_{R} D (M) = 1_{R}$
48	24 25 47	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \cdot_{R} D (M) = 1_{R}$
49	30	fveq2d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to \cdot_{R} = \cdot_{Scalar (A)}$
50	49	oveqd	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \cdot_{R} D (M) = H (D (M)) \cdot_{Scalar (A)} D (M)$
51	30	fveq2d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to 1_{R} = 1_{Scalar (A)}$
52	48 50 51	3eqtr3d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \cdot_{Scalar (A)} D (M) = 1_{Scalar (A)}$
53	52	oveq1d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (H (D (M)) \cdot_{Scalar (A)} D (M)) \underset{˙}{∙} 1_{A} = 1_{Scalar (A)} \underset{˙}{∙} 1_{A}$
54	26 6	unitcl	$⊢ D (M) \in V \to D (M) \in {Base}_{R}$
55	54	3ad2ant3	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to D (M) \in {Base}_{R}$
56	55 31	eleqtrd	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to D (M) \in {Base}_{Scalar (A)}$
57	4 11	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
58	19 57	syl	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to 1_{A} \in B$
59		eqid	$⊢ \cdot_{Scalar (A)} = \cdot_{Scalar (A)}$
60	4 36 9 37 59	lmodvsass	$⊢ (A \in LMod \land (H (D (M)) \in {Base}_{Scalar (A)} \land D (M) \in {Base}_{Scalar (A)} \land 1_{A} \in B)) \to (H (D (M)) \cdot_{Scalar (A)} D (M)) \underset{˙}{∙} 1_{A} = H (D (M)) \underset{˙}{∙} (D (M) \underset{˙}{∙} 1_{A})$
61	22 32 56 58 60	syl13anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (H (D (M)) \cdot_{Scalar (A)} D (M)) \underset{˙}{∙} 1_{A} = H (D (M)) \underset{˙}{∙} (D (M) \underset{˙}{∙} 1_{A})$
62		eqid	$⊢ 1_{Scalar (A)} = 1_{Scalar (A)}$
63	4 36 9 62	lmodvs1	$⊢ (A \in LMod \land 1_{A} \in B) \to 1_{Scalar (A)} \underset{˙}{∙} 1_{A} = 1_{A}$
64	22 58 63	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to 1_{Scalar (A)} \underset{˙}{∙} 1_{A} = 1_{A}$
65	53 61 64	3eqtr3d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \underset{˙}{∙} (D (M) \underset{˙}{∙} 1_{A}) = 1_{A}$
66	41 44 65	3eqtrd	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to M \cdot_{A} (H (D (M)) \underset{˙}{∙} J (M)) = 1_{A}$
67	4 36 37 9 10	assaass	$⊢ (A \in AssAlg \land (H (D (M)) \in {Base}_{Scalar (A)} \land J (M) \in B \land M \in B)) \to (H (D (M)) \underset{˙}{∙} J (M)) \cdot_{A} M = H (D (M)) \underset{˙}{∙} (J (M) \cdot_{A} M)$
68	17 32 35 20 67	syl13anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (H (D (M)) \underset{˙}{∙} J (M)) \cdot_{A} M = H (D (M)) \underset{˙}{∙} (J (M) \cdot_{A} M)$
69	1 4 2 3 11 10 9	madulid	$⊢ (M \in B \land R \in CRing) \to J (M) \cdot_{A} M = D (M) \underset{˙}{∙} 1_{A}$
70	20 15 69	syl2anc	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to J (M) \cdot_{A} M = D (M) \underset{˙}{∙} 1_{A}$
71	70	oveq2d	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to H (D (M)) \underset{˙}{∙} (J (M) \cdot_{A} M) = H (D (M)) \underset{˙}{∙} (D (M) \underset{˙}{∙} 1_{A})$
72	68 71 65	3eqtrd	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (H (D (M)) \underset{˙}{∙} J (M)) \cdot_{A} M = 1_{A}$
73	4 10 11 5 8 19 20 39 66 72	invrvald	$⊢ (R \in CRing \land M \in B \land D (M) \in V) \to (M \in U \land I (M) = H (D (M)) \underset{˙}{∙} J (M))$

Metamath Proof Explorer

Theorem matinv

Proof