madurid

Description: Multiplying a matrix with its adjunct results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in Lang p. 518. (Contributed by Stefan O'Rear, 16-Jul-2018)

	Ref	Expression
Hypotheses	madurid.a	$⊢ A = N Mat R$
	madurid.b	$⊢ B = {Base}_{A}$
	madurid.j	$⊢ J = N maAdju R$
	madurid.d	$⊢ D = N maDet R$
	madurid.i	$⊢ \underset{˙}{1} = 1_{A}$
	madurid.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	madurid.s	$⊢ \underset{˙}{∙} = \cdot_{A}$
Assertion	madurid	$⊢ (M \in B \land R \in CRing) \to M \underset{˙}{\cdot} J (M) = D (M) \underset{˙}{∙} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		madurid.a	$⊢ A = N Mat R$
2		madurid.b	$⊢ B = {Base}_{A}$
3		madurid.j	$⊢ J = N maAdju R$
4		madurid.d	$⊢ D = N maDet R$
5		madurid.i	$⊢ \underset{˙}{1} = 1_{A}$
6		madurid.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
7		madurid.s	$⊢ \underset{˙}{∙} = \cdot_{A}$
8		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11		simpr	$⊢ (M \in B \land R \in CRing) \to R \in CRing$
12	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
13	12	simpld	$⊢ M \in B \to N \in Fin$
14	13	adantr	$⊢ (M \in B \land R \in CRing) \to N \in Fin$
15	1 9 2	matbas2i	$⊢ M \in B \to M \in ({Base}_{R}^{(N \times N)})$
16	15	adantr	$⊢ (M \in B \land R \in CRing) \to M \in ({Base}_{R}^{(N \times N)})$
17	1 3 2	maduf	$⊢ R \in CRing \to J : B ⟶ B$
18	17	adantl	$⊢ (M \in B \land R \in CRing) \to J : B ⟶ B$
19		simpl	$⊢ (M \in B \land R \in CRing) \to M \in B$
20	18 19	ffvelrnd	$⊢ (M \in B \land R \in CRing) \to J (M) \in B$
21	1 9 2	matbas2i	$⊢ J (M) \in B \to J (M) \in ({Base}_{R}^{(N \times N)})$
22	20 21	syl	$⊢ (M \in B \land R \in CRing) \to J (M) \in ({Base}_{R}^{(N \times N)})$
23	8 9 10 11 14 14 14 16 22	mamuval	$⊢ (M \in B \land R \in CRing) \to M (R maMul ⟨N, N, N⟩) J (M) = (a \in N, b \in N ⟼ \underset{c \in N}{\sum_{R}} ((a M c) \cdot_{R} (c J (M) b)))$
24	1 8	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
25	13 24	sylan	$⊢ (M \in B \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
26	25 6	eqtr4di	$⊢ (M \in B \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \underset{˙}{\cdot}$
27	26	oveqd	$⊢ (M \in B \land R \in CRing) \to M (R maMul ⟨N, N, N⟩) J (M) = M \underset{˙}{\cdot} J (M)$
28		simp1l	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to M \in B$
29		simp1r	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to R \in CRing$
30		elmapi	$⊢ M \in ({Base}_{R}^{(N \times N)}) \to M : N \times N ⟶ {Base}_{R}$
31	16 30	syl	$⊢ (M \in B \land R \in CRing) \to M : N \times N ⟶ {Base}_{R}$
32	31	3ad2ant1	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to M : N \times N ⟶ {Base}_{R}$
33	32	adantr	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land c \in N) \to M : N \times N ⟶ {Base}_{R}$
34		simpl2	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land c \in N) \to a \in N$
35		simpr	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land c \in N) \to c \in N$
36	33 34 35	fovrnd	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land c \in N) \to a M c \in {Base}_{R}$
37		simp3	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to b \in N$
38	1 3 2 4 10 9 28 29 36 37	madugsum	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to \underset{c \in N}{\sum_{R}} ((a M c) \cdot_{R} (c J (M) b)) = D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c)))$
39		iftrue	$⊢ a = b \to if (a = b, D (M), 0_{R}) = D (M)$
40	39	adantl	$⊢ ((M \in B \land R \in CRing) \land a = b) \to if (a = b, D (M), 0_{R}) = D (M)$
41	31	ffnd	$⊢ (M \in B \land R \in CRing) \to M Fn (N \times N)$
42		fnov	$⊢ M Fn (N \times N) \leftrightarrow M = (d \in N, c \in N ⟼ d M c)$
43	41 42	sylib	$⊢ (M \in B \land R \in CRing) \to M = (d \in N, c \in N ⟼ d M c)$
44	43	adantr	$⊢ ((M \in B \land R \in CRing) \land a = b) \to M = (d \in N, c \in N ⟼ d M c)$
45		equtr2	$⊢ (a = b \land d = b) \to a = d$
46	45	oveq1d	$⊢ (a = b \land d = b) \to a M c = d M c$
47	46	ifeq1da	$⊢ a = b \to if (d = b, a M c, d M c) = if (d = b, d M c, d M c)$
48		ifid	$⊢ if (d = b, d M c, d M c) = d M c$
49	47 48	eqtrdi	$⊢ a = b \to if (d = b, a M c, d M c) = d M c$
50	49	adantl	$⊢ ((M \in B \land R \in CRing) \land a = b) \to if (d = b, a M c, d M c) = d M c$
51	50	mpoeq3dv	$⊢ ((M \in B \land R \in CRing) \land a = b) \to (d \in N, c \in N ⟼ if (d = b, a M c, d M c)) = (d \in N, c \in N ⟼ d M c)$
52	44 51	eqtr4d	$⊢ ((M \in B \land R \in CRing) \land a = b) \to M = (d \in N, c \in N ⟼ if (d = b, a M c, d M c))$
53	52	fveq2d	$⊢ ((M \in B \land R \in CRing) \land a = b) \to D (M) = D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c)))$
54	40 53	eqtr2d	$⊢ ((M \in B \land R \in CRing) \land a = b) \to D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c))) = if (a = b, D (M), 0_{R})$
55	54	3ad2antl1	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land a = b) \to D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c))) = if (a = b, D (M), 0_{R})$
56		eqid	$⊢ 0_{R} = 0_{R}$
57		simpl1r	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to R \in CRing$
58	14	3ad2ant1	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to N \in Fin$
59	58	adantr	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to N \in Fin$
60	32	ad2antrr	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land c \in N) \to M : N \times N ⟶ {Base}_{R}$
61		simpll2	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land c \in N) \to a \in N$
62		simpr	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land c \in N) \to c \in N$
63	60 61 62	fovrnd	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land c \in N) \to a M c \in {Base}_{R}$
64	32	adantr	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to M : N \times N ⟶ {Base}_{R}$
65	64	fovrnda	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land (d \in N \land c \in N)) \to d M c \in {Base}_{R}$
66	65	3impb	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land d \in N \land c \in N) \to d M c \in {Base}_{R}$
67		simpl3	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to b \in N$
68		simpl2	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to a \in N$
69		neqne	$⊢ \neg a = b \to a \neq b$
70	69	necomd	$⊢ \neg a = b \to b \neq a$
71	70	adantl	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to b \neq a$
72	4 9 56 57 59 63 66 67 68 71	mdetralt2	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to D ((d \in N, c \in N ⟼ if (d = b, a M c, if (d = a, a M c, d M c)))) = 0_{R}$
73		ifid	$⊢ if (d = a, d M c, d M c) = d M c$
74		oveq1	$⊢ d = a \to d M c = a M c$
75	74	adantl	$⊢ ((((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \land d = a) \to d M c = a M c$
76	75	ifeq1da	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to if (d = a, d M c, d M c) = if (d = a, a M c, d M c)$
77	73 76	eqtr3id	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to d M c = if (d = a, a M c, d M c)$
78	77	ifeq2d	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to if (d = b, a M c, d M c) = if (d = b, a M c, if (d = a, a M c, d M c))$
79	78	mpoeq3dv	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to (d \in N, c \in N ⟼ if (d = b, a M c, d M c)) = (d \in N, c \in N ⟼ if (d = b, a M c, if (d = a, a M c, d M c)))$
80	79	fveq2d	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c))) = D ((d \in N, c \in N ⟼ if (d = b, a M c, if (d = a, a M c, d M c))))$
81		iffalse	$⊢ \neg a = b \to if (a = b, D (M), 0_{R}) = 0_{R}$
82	81	adantl	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to if (a = b, D (M), 0_{R}) = 0_{R}$
83	72 80 82	3eqtr4d	$⊢ (((M \in B \land R \in CRing) \land a \in N \land b \in N) \land \neg a = b) \to D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c))) = if (a = b, D (M), 0_{R})$
84	55 83	pm2.61dan	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to D ((d \in N, c \in N ⟼ if (d = b, a M c, d M c))) = if (a = b, D (M), 0_{R})$
85	38 84	eqtrd	$⊢ ((M \in B \land R \in CRing) \land a \in N \land b \in N) \to \underset{c \in N}{\sum_{R}} ((a M c) \cdot_{R} (c J (M) b)) = if (a = b, D (M), 0_{R})$
86	85	mpoeq3dva	$⊢ (M \in B \land R \in CRing) \to (a \in N, b \in N ⟼ \underset{c \in N}{\sum_{R}} ((a M c) \cdot_{R} (c J (M) b))) = (a \in N, b \in N ⟼ if (a = b, D (M), 0_{R}))$
87	5	oveq2i	$⊢ D (M) \underset{˙}{∙} \underset{˙}{1} = D (M) \underset{˙}{∙} 1_{A}$
88		crngring	$⊢ R \in CRing \to R \in Ring$
89	88	adantl	$⊢ (M \in B \land R \in CRing) \to R \in Ring$
90	4 1 2 9	mdetf	$⊢ R \in CRing \to D : B ⟶ {Base}_{R}$
91	90	adantl	$⊢ (M \in B \land R \in CRing) \to D : B ⟶ {Base}_{R}$
92	91 19	ffvelrnd	$⊢ (M \in B \land R \in CRing) \to D (M) \in {Base}_{R}$
93	1 9 7 56	matsc	$⊢ (N \in Fin \land R \in Ring \land D (M) \in {Base}_{R}) \to D (M) \underset{˙}{∙} 1_{A} = (a \in N, b \in N ⟼ if (a = b, D (M), 0_{R}))$
94	14 89 92 93	syl3anc	$⊢ (M \in B \land R \in CRing) \to D (M) \underset{˙}{∙} 1_{A} = (a \in N, b \in N ⟼ if (a = b, D (M), 0_{R}))$
95	87 94	eqtrid	$⊢ (M \in B \land R \in CRing) \to D (M) \underset{˙}{∙} \underset{˙}{1} = (a \in N, b \in N ⟼ if (a = b, D (M), 0_{R}))$
96	86 95	eqtr4d	$⊢ (M \in B \land R \in CRing) \to (a \in N, b \in N ⟼ \underset{c \in N}{\sum_{R}} ((a M c) \cdot_{R} (c J (M) b))) = D (M) \underset{˙}{∙} \underset{˙}{1}$
97	23 27 96	3eqtr3d	$⊢ (M \in B \land R \in CRing) \to M \underset{˙}{\cdot} J (M) = D (M) \underset{˙}{∙} \underset{˙}{1}$

Metamath Proof Explorer

Theorem madurid

Proof