mdetlap

Description: Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020)

	Ref	Expression
Hypotheses	madjusmdet.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	madjusmdet.a	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
	madjusmdet.d	⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
	madjusmdet.k	⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
	madjusmdet.t	⊢ · = ( ._r ‘ 𝑅 )
	madjusmdet.z	⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
	madjusmdet.e	⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
	madjusmdet.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	madjusmdet.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	madjusmdet.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
	madjusmdet.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
	madjusmdet.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
Assertion	mdetlap	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
2		madjusmdet.a	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
3		madjusmdet.d	⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
4		madjusmdet.k	⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
5		madjusmdet.t	⊢ · = ( ._r ‘ 𝑅 )
6		madjusmdet.z	⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
7		madjusmdet.e	⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
8		madjusmdet.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9		madjusmdet.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
10		madjusmdet.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
11		madjusmdet.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
12		madjusmdet.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
13	2 1 3 4 5	mdetlap1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )
14	9 12 10 13	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
16	9	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ CRing )
17	10	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
19	12	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ 𝐵 )
20	1 2 3 4 5 6 7 15 16 17 18 19	madjusmdet	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) )
21	20	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
22		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23	2 22 1 17 18 19	matecld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
24		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
25	9 24	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
26	6	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ ( ℤ_ring RingHom 𝑅 ) )
27		zringbas	⊢ ℤ = ( Base ‘ ℤ_ring )
28	27 22	rhmf	⊢ ( 𝑍 ∈ ( ℤ_ring RingHom 𝑅 ) → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
29	25 26 28	3syl	⊢ ( 𝜑 → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑍 : ℤ ⟶ ( Base ‘ 𝑅 ) )
31		1zzd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℤ )
32	31	znegcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → - 1 ∈ ℤ )
33		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
34	33 17	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐼 ∈ ℕ )
35	33 18	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ℕ )
36	34 35	nnaddcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 + 𝑗 ) ∈ ℕ )
37	36	nnnn0d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 + 𝑗 ) ∈ ℕ₀ )
38		zexpcl	⊢ ( ( - 1 ∈ ℤ ∧ ( 𝐼 + 𝑗 ) ∈ ℕ₀ ) → ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ∈ ℤ )
39	32 37 38	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ∈ ℤ )
40	30 39	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
41	22 5	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) )
42	16 23 40 41	syl3anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) )
43	42	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) )
44	16 24	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ Ring )
45		eqid	⊢ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
46		eqid	⊢ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) = ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 )
47	2 1 45 46 15 17 18 19	smatcl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
48		eqid	⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
49	7 48 45 22	mdetcl	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ) → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
50	16 47 49	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
51	22 5	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
52	44 23 40 50 51	syl13anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐼 𝑀 𝑗 ) · ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
53	22 5	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
54	44 40 23 50 53	syl13anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐼 𝑀 𝑗 ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
55	43 52 54	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
56	21 55	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) )
57	56	mpteq2dva	⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) )
58	57	oveq2d	⊢ ( 𝜑 → ( 𝑅 Σ_g ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) = ( 𝑅 Σ_g ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )
59	14 58	eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝑗 ) ) ) · ( ( 𝐼 𝑀 𝑗 ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝑗 ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem mdetlap

Proof