Theorem mdetfval1

Description: First substitution of an alternative determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by AV, 27-Dec-2018)

	Ref	Expression
Hypotheses	mdetfval1.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdetfval1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mdetfval1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mdetfval1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	mdetfval1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
	mdetfval1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	mdetfval1.t	⊢ · = ( .r ‘ 𝑅 )
	mdetfval1.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
Assertion	mdetfval1	⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetfval1.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetfval1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mdetfval1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mdetfval1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5		mdetfval1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
6		mdetfval1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
7		mdetfval1.t	⊢ · = ( .r ‘ 𝑅 )
8		mdetfval1.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
9	1 2 3 4 5 6 7 8	mdetfval	⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
10	4 6	cofipsgn	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) )
11	10	oveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) = ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) )
12	11	mpteq2dva	⊢ ( 𝑁 ∈ Fin → ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) )
13	12	oveq2d	⊢ ( 𝑁 ∈ Fin → ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
14	13	mpteq2dv	⊢ ( 𝑁 ∈ Fin → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
15	9 14	syl5eq	⊢ ( 𝑁 ∈ Fin → 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
16		df-nel	⊢ ( 𝑁 ∉ Fin ↔ ¬ 𝑁 ∈ Fin )
17	1	nfimdetndef	⊢ ( 𝑁 ∉ Fin → 𝐷 = ∅ )
18	2	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
19	3 18	eqtri	⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
20	16	biimpi	⊢ ( 𝑁 ∉ Fin → ¬ 𝑁 ∈ Fin )
21	20	intnanrd	⊢ ( 𝑁 ∉ Fin → ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
22		matbas0	⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
23	21 22	syl	⊢ ( 𝑁 ∉ Fin → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
24	19 23	syl5eq	⊢ ( 𝑁 ∉ Fin → 𝐵 = ∅ )
25	24	mpteq1d	⊢ ( 𝑁 ∉ Fin → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
26		mpt0	⊢ ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅
27	25 26	eqtrdi	⊢ ( 𝑁 ∉ Fin → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅ )
28	17 27	eqtr4d	⊢ ( 𝑁 ∉ Fin → 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
29	16 28	sylbir	⊢ ( ¬ 𝑁 ∈ Fin → 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
30	15 29	pm2.61i	⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )