Theorem madetsumid

Description: The identity summand in the Leibniz' formula of a determinant for a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018)

	Ref	Expression
Hypotheses	madetsumid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	madetsumid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	madetsumid.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
	madetsumid.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
	madetsumid.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	madetsumid.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	madetsumid	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		madetsumid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		madetsumid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		madetsumid.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
4		madetsumid.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
5		madetsumid.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
6		madetsumid.t	⊢ · = ( .r ‘ 𝑅 )
7		fveq2	⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) = ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) )
8		fveq1	⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( 𝑃 ‘ 𝑟 ) = ( ( I ↾ 𝑁 ) ‘ 𝑟 ) )
9	8	oveq1d	⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) = ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) )
10	9	mpteq2dv	⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) = ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) )
11	10	oveq2d	⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) )
12	7 11	oveq12d	⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) )
13	12	3ad2ant3	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) )
14	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
15	14	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
16	4 5	coeq12i	⊢ ( 𝑌 ∘ 𝑆 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) )
17	16	a1i	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑌 ∘ 𝑆 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) )
18		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
19	18	symgid	⊢ ( 𝑁 ∈ Fin → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
20	19	adantl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
21	17 20	fveq12d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) )
22		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
23		zrhpsgnmhm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
24	3	oveq2i	⊢ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) = ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) )
25	23 24	eleqtrrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) )
26	22 25	sylan	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) )
27		eqid	⊢ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) )
28		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
29	3 28	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑈 )
30	27 29	mhm0	⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( 1r ‘ 𝑅 ) )
31	26 30	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( 1r ‘ 𝑅 ) )
32	21 31	eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) = ( 1r ‘ 𝑅 ) )
33		fvresi	⊢ ( 𝑟 ∈ 𝑁 → ( ( I ↾ 𝑁 ) ‘ 𝑟 ) = 𝑟 )
34	33	adantl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑟 ∈ 𝑁 ) → ( ( I ↾ 𝑁 ) ‘ 𝑟 ) = 𝑟 )
35	34	oveq1d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑟 ∈ 𝑁 ) → ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) = ( 𝑟 𝑀 𝑟 ) )
36	35	mpteq2dva	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) = ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) )
37	36	oveq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
38	32 37	oveq12d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) )
39	15 38	sylan2	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) )
40	1 2 3	matgsumcl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) )
41		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42	41 6 28	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
43	22 40 42	syl2an2r	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
44	39 43	eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
45	44	3adant3	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
46	13 45	eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )