Theorem mdetfval

Description: First substitution for the determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by SO, 9-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		mdetfval.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mdetfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mdetfval.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5		mdetfval.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
6		mdetfval.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
7		mdetfval.t	⊢ · = ( .r ‘ 𝑅 )
8		mdetfval.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
9		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
10	9 2	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = 𝐴 )
11	10	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ 𝐴 ) )
12	11 3	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
13		simpr	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
14		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
15	14	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( SymGrp ‘ 𝑛 ) = ( SymGrp ‘ 𝑁 ) )
16	15	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( SymGrp ‘ 𝑛 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
17	16 4	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( SymGrp ‘ 𝑛 ) ) = 𝑃 )
18		fveq2	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
19	18	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
20	19 7	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( .r ‘ 𝑟 ) = · )
21	13	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ℤRHom ‘ 𝑟 ) = ( ℤRHom ‘ 𝑅 ) )
22	21 5	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ℤRHom ‘ 𝑟 ) = 𝑌 )
23		fveq2	⊢ ( 𝑛 = 𝑁 → ( pmSgn ‘ 𝑛 ) = ( pmSgn ‘ 𝑁 ) )
24	23	adantr	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( pmSgn ‘ 𝑛 ) = ( pmSgn ‘ 𝑁 ) )
25	24 6	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( pmSgn ‘ 𝑛 ) = 𝑆 )
26	22 25	coeq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) = ( 𝑌 ∘ 𝑆 ) )
27	26	fveq1d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) )
28		fveq2	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
29	28	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
30	29 8	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( mulGrp ‘ 𝑟 ) = 𝑈 )
31	14	mpteq1d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) )
32	30 31	oveq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) = ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) )
33	20 27 32	oveq123d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r ‘ 𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) )
34	17 33	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r ‘ 𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) )
35	13 34	oveq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r ‘ 𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
36	12 35	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r ‘ 𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
37		df-mdet	⊢ maDet = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r ‘ 𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
38	3	fvexi	⊢ 𝐵 ∈ V
39	38	mptex	⊢ ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) ∈ V
40	36 37 39	ovmpoa	⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maDet 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
41	37	reldmmpo	⊢ Rel dom maDet
42	41	ovprc	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maDet 𝑅 ) = ∅ )
43		mpt0	⊢ ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅
44	42 43	eqtr4di	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maDet 𝑅 ) = ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
45		df-mat	⊢ Mat = ( 𝑦 ∈ Fin , 𝑧 ∈ V ↦ ( ( 𝑧 freeLMod ( 𝑦 × 𝑦 ) ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑧 maMul ⟨ 𝑦 , 𝑦 , 𝑦 ⟩ ) ⟩ ) )
46	45	reldmmpo	⊢ Rel dom Mat
47	46	ovprc	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ∅ )
48	2 47	syl5eq	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝐴 = ∅ )
49	48	fveq2d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ 𝐴 ) = ( Base ‘ ∅ ) )
50		base0	⊢ ∅ = ( Base ‘ ∅ )
51	49 3 50	3eqtr4g	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
52	51	mpteq1d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
53	44 52	eqtr4d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maDet 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
54	40 53	pm2.61i	⊢ ( 𝑁 maDet 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
55	1 54	eqtri	⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )