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	$⊢ D = N maDet R$
	mdetfval.a	$⊢ A = N Mat R$
	mdetfval.b	$⊢ B = {Base}_{A}$
	mdetfval.p	$⊢ P = {Base}_{SymGrp (N)}$
	mdetfval.y	$⊢ Y = ℤRHom (R)$
	mdetfval.s	$⊢ S = pmSgn (N)$
	mdetfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetfval.u	$⊢ U = {mulGrp}_{R}$
Assertion	mdetfval	$⊢ D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$

Proof

Step	Hyp	Ref	Expression
1		mdetfval.d	$⊢ D = N maDet R$
2		mdetfval.a	$⊢ A = N Mat R$
3		mdetfval.b	$⊢ B = {Base}_{A}$
4		mdetfval.p	$⊢ P = {Base}_{SymGrp (N)}$
5		mdetfval.y	$⊢ Y = ℤRHom (R)$
6		mdetfval.s	$⊢ S = pmSgn (N)$
7		mdetfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetfval.u	$⊢ U = {mulGrp}_{R}$
9		oveq12	$⊢ (n = N \land r = R) \to n Mat r = N Mat R$
10	9 2	eqtr4di	$⊢ (n = N \land r = R) \to n Mat r = A$
11	10	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = {Base}_{A}$
12	11 3	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = B$
13		simpr	$⊢ (n = N \land r = R) \to r = R$
14		simpl	$⊢ (n = N \land r = R) \to n = N$
15	14	fveq2d	$⊢ (n = N \land r = R) \to SymGrp (n) = SymGrp (N)$
16	15	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{SymGrp (n)} = {Base}_{SymGrp (N)}$
17	16 4	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{SymGrp (n)} = P$
18		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
19	18	adantl	$⊢ (n = N \land r = R) \to \cdot_{r} = \cdot_{R}$
20	19 7	eqtr4di	$⊢ (n = N \land r = R) \to \cdot_{r} = \underset{˙}{\cdot}$
21	13	fveq2d	$⊢ (n = N \land r = R) \to ℤRHom (r) = ℤRHom (R)$
22	21 5	eqtr4di	$⊢ (n = N \land r = R) \to ℤRHom (r) = Y$
23		fveq2	$⊢ n = N \to pmSgn (n) = pmSgn (N)$
24	23	adantr	$⊢ (n = N \land r = R) \to pmSgn (n) = pmSgn (N)$
25	24 6	eqtr4di	$⊢ (n = N \land r = R) \to pmSgn (n) = S$
26	22 25	coeq12d	$⊢ (n = N \land r = R) \to ℤRHom (r) \circ pmSgn (n) = Y \circ S$
27	26	fveq1d	$⊢ (n = N \land r = R) \to (ℤRHom (r) \circ pmSgn (n)) (p) = (Y \circ S) (p)$
28		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
29	28	adantl	$⊢ (n = N \land r = R) \to {mulGrp}_{r} = {mulGrp}_{R}$
30	29 8	eqtr4di	$⊢ (n = N \land r = R) \to {mulGrp}_{r} = U$
31	14	mpteq1d	$⊢ (n = N \land r = R) \to (x \in n ⟼ p (x) m x) = (x \in N ⟼ p (x) m x)$
32	30 31	oveq12d	$⊢ (n = N \land r = R) \to \underset{x \in n}{\sum_{{mulGrp}_{r}}} (p (x) m x) = \underset{x \in N}{\sum_{U}} (p (x) m x)$
33	20 27 32	oveq123d	$⊢ (n = N \land r = R) \to (ℤRHom (r) \circ pmSgn (n)) (p) \cdot_{r} (\underset{x \in n}{\sum_{{mulGrp}_{r}}}, (p (x) m x)) = (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))$
34	17 33	mpteq12dv	$⊢ (n = N \land r = R) \to (p \in {Base}_{SymGrp (n)} ⟼ (ℤRHom (r) \circ pmSgn (n)) (p) \cdot_{r} (\underset{x \in n}{\sum_{{mulGrp}_{r}}}, (p (x) m x))) = (p \in P ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))$
35	13 34	oveq12d	$⊢ (n = N \land r = R) \to \underset{p \in {Base}_{SymGrp (n)}}{\sum_{r}} ((ℤRHom (r) \circ pmSgn (n)) (p) \cdot_{r} (\underset{x \in n}{\sum_{{mulGrp}_{r}}}, (p (x) m x))) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))$
36	12 35	mpteq12dv	$⊢ (n = N \land r = R) \to (m \in {Base}_{(n Mat r)} ⟼ \underset{p \in {Base}_{SymGrp (n)}}{\sum_{r}} ((ℤRHom (r) \circ pmSgn (n)) (p) \cdot_{r} (\underset{x \in n}{\sum_{{mulGrp}_{r}}}, (p (x) m x)))) = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
37		df-mdet	$⊢ maDet = (n \in V, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ \underset{p \in {Base}_{SymGrp (n)}}{\sum_{r}} ((ℤRHom (r) \circ pmSgn (n)) (p) \cdot_{r} (\underset{x \in n}{\sum_{{mulGrp}_{r}}}, (p (x) m x)))))$
38	3	fvexi	$⊢ B \in V$
39	38	mptex	$⊢ (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))) \in V$
40	36 37 39	ovmpoa	$⊢ (N \in V \land R \in V) \to N maDet R = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
41	37	reldmmpo	$⊢ Rel dom maDet$
42	41	ovprc	$⊢ \neg (N \in V \land R \in V) \to N maDet R = \emptyset$
43		mpt0	$⊢ (m \in \emptyset ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))) = \emptyset$
44	42 43	eqtr4di	$⊢ \neg (N \in V \land R \in V) \to N maDet R = (m \in \emptyset ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
45		df-mat	$⊢ Mat = (y \in Fin, z \in V ⟼ (z freeLMod (y \times y)) sSet ⟨\cdot_{ndx}, z maMul ⟨y, y, y⟩⟩)$
46	45	reldmmpo	$⊢ Rel dom Mat$
47	46	ovprc	$⊢ \neg (N \in V \land R \in V) \to N Mat R = \emptyset$
48	2 47	syl5eq	$⊢ \neg (N \in V \land R \in V) \to A = \emptyset$
49	48	fveq2d	$⊢ \neg (N \in V \land R \in V) \to {Base}_{A} = {Base}_{\emptyset}$
50		base0	$⊢ \emptyset = {Base}_{\emptyset}$
51	49 3 50	3eqtr4g	$⊢ \neg (N \in V \land R \in V) \to B = \emptyset$
52	51	mpteq1d	$⊢ \neg (N \in V \land R \in V) \to (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))) = (m \in \emptyset ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
53	44 52	eqtr4d	$⊢ \neg (N \in V \land R \in V) \to N maDet R = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
54	40 53	pm2.61i	$⊢ N maDet R = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
55	1 54	eqtri	$⊢ D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$

Metamath Proof Explorer

Theorem mdetfval

Proof