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

Proof

Step	Hyp	Ref	Expression
1		mdetfval1.d	$⊢ D = N maDet R$
2		mdetfval1.a	$⊢ A = N Mat R$
3		mdetfval1.b	$⊢ B = {Base}_{A}$
4		mdetfval1.p	$⊢ P = {Base}_{SymGrp (N)}$
5		mdetfval1.y	$⊢ Y = ℤRHom (R)$
6		mdetfval1.s	$⊢ S = pmSgn (N)$
7		mdetfval1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetfval1.u	$⊢ U = {mulGrp}_{R}$
9	1 2 3 4 5 6 7 8	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))))$
10	4 6	cofipsgn	$⊢ (N \in Fin \land p \in P) \to (Y \circ S) (p) = Y (S (p))$
11	10	oveq1d	$⊢ (N \in Fin \land p \in P) \to (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)) = Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))$
12	11	mpteq2dva	$⊢ N \in Fin \to (p \in P ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))) = (p \in P ⟼ Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))$
13	12	oveq2d	$⊢ N \in Fin \to \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))) = \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))$
14	13	mpteq2dv	$⊢ N \in Fin \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 B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
15	9 14	eqtrid	$⊢ N \in Fin \to D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
16		df-nel	$⊢ N \notin Fin \leftrightarrow \neg N \in Fin$
17	1	nfimdetndef	$⊢ N \notin Fin \to D = \emptyset$
18	2	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
19	3 18	eqtri	$⊢ B = {Base}_{(N Mat R)}$
20	16	biimpi	$⊢ N \notin Fin \to \neg N \in Fin$
21	20	intnanrd	$⊢ N \notin Fin \to \neg (N \in Fin \land R \in V)$
22		matbas0	$⊢ \neg (N \in Fin \land R \in V) \to {Base}_{(N Mat R)} = \emptyset$
23	21 22	syl	$⊢ N \notin Fin \to {Base}_{(N Mat R)} = \emptyset$
24	19 23	eqtrid	$⊢ N \notin Fin \to B = \emptyset$
25	24	mpteq1d	$⊢ N \notin Fin \to (m \in B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))) = (m \in \emptyset ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
26		mpt0	$⊢ (m \in \emptyset ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))) = \emptyset$
27	25 26	eqtrdi	$⊢ N \notin Fin \to (m \in B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)))) = \emptyset$
28	17 27	eqtr4d	$⊢ N \notin Fin \to D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
29	16 28	sylbir	$⊢ \neg N \in Fin \to D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
30	15 29	pm2.61i	$⊢ D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} (Y (S (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$

Metamath Proof Explorer

Theorem mdetfval1

Proof