maduf

Description: Creating the adjunct of matrices is a function from the set of matrices into the set of matrices. (Contributed by Stefan O'Rear, 11-Jul-2018)

	Ref	Expression
Hypotheses	maduf.a	$⊢ A = N Mat R$
	maduf.j	$⊢ J = N maAdju R$
	maduf.b	$⊢ B = {Base}_{A}$
Assertion	maduf	$⊢ R \in CRing \to J : B ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		maduf.a	$⊢ A = N Mat R$
2		maduf.j	$⊢ J = N maAdju R$
3		maduf.b	$⊢ B = {Base}_{A}$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	1 3	matrcl	$⊢ m \in B \to (N \in Fin \land R \in V)$
6	5	adantl	$⊢ (R \in CRing \land m \in B) \to (N \in Fin \land R \in V)$
7	6	simpld	$⊢ (R \in CRing \land m \in B) \to N \in Fin$
8		simpl	$⊢ (R \in CRing \land m \in B) \to R \in CRing$
9		eqid	$⊢ N maDet R = N maDet R$
10	9 1 3 4	mdetf	$⊢ R \in CRing \to (N maDet R) : B ⟶ {Base}_{R}$
11	10	adantr	$⊢ (R \in CRing \land m \in B) \to (N maDet R) : B ⟶ {Base}_{R}$
12	11	3ad2ant1	$⊢ ((R \in CRing \land m \in B) \land i \in N \land j \in N) \to (N maDet R) : B ⟶ {Base}_{R}$
13	7	3ad2ant1	$⊢ ((R \in CRing \land m \in B) \land i \in N \land j \in N) \to N \in Fin$
14		simp1l	$⊢ ((R \in CRing \land m \in B) \land i \in N \land j \in N) \to R \in CRing$
15		simp11l	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to R \in CRing$
16		crngring	$⊢ R \in CRing \to R \in Ring$
17		eqid	$⊢ 1_{R} = 1_{R}$
18	4 17	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	4 19	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
21	18 20	ifcld	$⊢ R \in Ring \to if (l = i, 1_{R}, 0_{R}) \in {Base}_{R}$
22	15 16 21	3syl	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to if (l = i, 1_{R}, 0_{R}) \in {Base}_{R}$
23		simp2	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to k \in N$
24		simp3	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to l \in N$
25		simp11r	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to m \in B$
26	1 4 3 23 24 25	matecld	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to k m l \in {Base}_{R}$
27	22 26	ifcld	$⊢ (((R \in CRing \land m \in B) \land i \in N \land j \in N) \land k \in N \land l \in N) \to if (k = j, if (l = i, 1_{R}, 0_{R}), k m l) \in {Base}_{R}$
28	1 4 3 13 14 27	matbas2d	$⊢ ((R \in CRing \land m \in B) \land i \in N \land j \in N) \to (k \in N, l \in N ⟼ if (k = j, if (l = i, 1_{R}, 0_{R}), k m l)) \in B$
29	12 28	ffvelrnd	$⊢ ((R \in CRing \land m \in B) \land i \in N \land j \in N) \to (N maDet R) ((k \in N, l \in N ⟼ if (k = j, if (l = i, 1_{R}, 0_{R}), k m l))) \in {Base}_{R}$
30	1 4 3 7 8 29	matbas2d	$⊢ (R \in CRing \land m \in B) \to (i \in N, j \in N ⟼ (N maDet R) ((k \in N, l \in N ⟼ if (k = j, if (l = i, 1_{R}, 0_{R}), k m l)))) \in B$
31	1 9 2 3 17 19	madufval	$⊢ J = (m \in B ⟼ (i \in N, j \in N ⟼ (N maDet R) ((k \in N, l \in N ⟼ if (k = j, if (l = i, 1_{R}, 0_{R}), k m l)))))$
32	30 31	fmptd	$⊢ R \in CRing \to J : B ⟶ B$

Metamath Proof Explorer

Theorem maduf

Proof