Theorem mdetero

Description: The determinant function is multilinear (additive and homogeneous for each row (matrices are given explicitly by their entries). Corollary 4.9 in Lang p. 515. (Contributed by SO, 16-Jul-2018)

	Ref	Expression
Hypotheses	mdetero.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdetero.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mdetero.p	⊢ + = ( +g ‘ 𝑅 )
	mdetero.t	⊢ · = ( .r ‘ 𝑅 )
	mdetero.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mdetero.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mdetero.x	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
	mdetero.y	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
	mdetero.z	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ 𝐾 )
	mdetero.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐾 )
	mdetero.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	mdetero.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
	mdetero.ij	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
Assertion	mdetero	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + ( 𝑊 · 𝑌 ) ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetero.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetero.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		mdetero.p	⊢ + = ( +g ‘ 𝑅 )
4		mdetero.t	⊢ · = ( .r ‘ 𝑅 )
5		mdetero.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		mdetero.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mdetero.x	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
8		mdetero.y	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
9		mdetero.z	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ 𝐾 )
10		mdetero.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐾 )
11		mdetero.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
12		mdetero.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
13		mdetero.ij	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
14	7	3adant2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
15		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16	5 15	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
17	16	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
18	10	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑊 ∈ 𝐾 )
19	8	3adant2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
20	2 4	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑊 · 𝑌 ) ∈ 𝐾 )
21	17 18 19 20	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑊 · 𝑌 ) ∈ 𝐾 )
22	19 9	ifcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ∈ 𝐾 )
23	1 2 3 5 6 14 21 22 11	mdetrlin2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + ( 𝑊 · 𝑌 ) ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) )
24	1 2 4 5 6 19 22 10 11	mdetrsca2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 𝑊 · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) )
25		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26	1 2 25 5 6 8 9 11 12 13	mdetralt2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 0g ‘ 𝑅 ) )
27	26	oveq2d	⊢ ( 𝜑 → ( 𝑊 · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) = ( 𝑊 · ( 0g ‘ 𝑅 ) ) )
28	2 4 25	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐾 ) → ( 𝑊 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
29	16 10 28	syl2anc	⊢ ( 𝜑 → ( 𝑊 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
30	24 27 29	3eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 0g ‘ 𝑅 ) )
31	30	oveq2d	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) = ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 0g ‘ 𝑅 ) ) )
32		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
33	16 32	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
34		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
35		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
36	1 34 35 2	mdetf	⊢ ( 𝑅 ∈ CRing → 𝐷 : ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ⟶ 𝐾 )
37	5 36	syl	⊢ ( 𝜑 → 𝐷 : ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ⟶ 𝐾 )
38	14 22	ifcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ∈ 𝐾 )
39	34 2 35 6 5 38	matbas2d	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
40	37 39	ffvelrnd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ∈ 𝐾 )
41	2 3 25	grprid	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 0g ‘ 𝑅 ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )
42	33 40 41	syl2anc	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 0g ‘ 𝑅 ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )
43	23 31 42	3eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + ( 𝑊 · 𝑌 ) ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )