mdet1

Description: The determinant of the identity matrix is 1, i.e. the determinant function is normalized, see also definition in Lang p. 513. (Contributed by SO, 10-Jul-2018) (Proof shortened by AV, 25-Nov-2019)

	Ref	Expression
Hypotheses	mdet1.d	$⊢ D = N maDet R$
	mdet1.a	$⊢ A = N Mat R$
	mdet1.n	$⊢ I = 1_{A}$
	mdet1.o	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	mdet1	$⊢ (R \in CRing \land N \in Fin) \to D (I) = \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		mdet1.d	$⊢ D = N maDet R$
2		mdet1.a	$⊢ A = N Mat R$
3		mdet1.n	$⊢ I = 1_{A}$
4		mdet1.o	$⊢ \underset{˙}{1} = 1_{R}$
5		id	$⊢ (R \in CRing \land N \in Fin) \to (R \in CRing \land N \in Fin)$
6		crngring	$⊢ R \in CRing \to R \in Ring$
7	6	anim1ci	$⊢ (R \in CRing \land N \in Fin) \to (N \in Fin \land R \in Ring)$
8	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
9		eqid	$⊢ {Base}_{A} = {Base}_{A}$
10	9 3	ringidcl	$⊢ A \in Ring \to I \in {Base}_{A}$
11	7 8 10	3syl	$⊢ (R \in CRing \land N \in Fin) \to I \in {Base}_{A}$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	12 4	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
14	6 13	syl	$⊢ R \in CRing \to \underset{˙}{1} \in {Base}_{R}$
15	14	adantr	$⊢ (R \in CRing \land N \in Fin) \to \underset{˙}{1} \in {Base}_{R}$
16	5 11 15	jca32	$⊢ (R \in CRing \land N \in Fin) \to ((R \in CRing \land N \in Fin) \land (I \in {Base}_{A} \land \underset{˙}{1} \in {Base}_{R}))$
17		eqid	$⊢ 0_{R} = 0_{R}$
18		simplr	$⊢ ((R \in CRing \land N \in Fin) \land (i \in N \land j \in N)) \to N \in Fin$
19	6	adantr	$⊢ (R \in CRing \land N \in Fin) \to R \in Ring$
20	19	adantr	$⊢ ((R \in CRing \land N \in Fin) \land (i \in N \land j \in N)) \to R \in Ring$
21		simprl	$⊢ ((R \in CRing \land N \in Fin) \land (i \in N \land j \in N)) \to i \in N$
22		simprr	$⊢ ((R \in CRing \land N \in Fin) \land (i \in N \land j \in N)) \to j \in N$
23	2 4 17 18 20 21 22 3	mat1ov	$⊢ ((R \in CRing \land N \in Fin) \land (i \in N \land j \in N)) \to i I j = if (i = j, \underset{˙}{1}, 0_{R})$
24	23	ralrimivva	$⊢ (R \in CRing \land N \in Fin) \to \forall i \in N \forall j \in N i I j = if (i = j, \underset{˙}{1}, 0_{R})$
25		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
26		eqid	$⊢ \cdot_{{mulGrp}_{R}} = \cdot_{{mulGrp}_{R}}$
27	1 2 9 25 17 12 26	mdetdiagid	$⊢ ((R \in CRing \land N \in Fin) \land (I \in {Base}_{A} \land \underset{˙}{1} \in {Base}_{R})) \to (\forall i \in N \forall j \in N i I j = if (i = j, \underset{˙}{1}, 0_{R}) \to D (I) = \|N\| \cdot_{{mulGrp}_{R}} \underset{˙}{1})$
28	16 24 27	sylc	$⊢ (R \in CRing \land N \in Fin) \to D (I) = \|N\| \cdot_{{mulGrp}_{R}} \underset{˙}{1}$
29		ringsrg	$⊢ R \in Ring \to R \in SRing$
30	6 29	syl	$⊢ R \in CRing \to R \in SRing$
31		hashcl	$⊢ N \in Fin \to \|N\| \in ℕ_{0}$
32	25 26 4	srg1expzeq1	$⊢ (R \in SRing \land \|N\| \in ℕ_{0}) \to \|N\| \cdot_{{mulGrp}_{R}} \underset{˙}{1} = \underset{˙}{1}$
33	30 31 32	syl2an	$⊢ (R \in CRing \land N \in Fin) \to \|N\| \cdot_{{mulGrp}_{R}} \underset{˙}{1} = \underset{˙}{1}$
34	28 33	eqtrd	$⊢ (R \in CRing \land N \in Fin) \to D (I) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem mdet1

Proof