mdetrsca

Description: The determinant function is homogeneous for each row: If the matrices X and Z are identical except for the I -th row, and the I -th row of the matrix X is the componentwise product of the I -th row of the matrix Z and the scalar Y , then the determinant of X is the determinant of Z multiplied by Y . (Contributed by SO, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	mdetrsca.d	$⊢ D = N maDet R$
	mdetrsca.a	$⊢ A = N Mat R$
	mdetrsca.b	$⊢ B = {Base}_{A}$
	mdetrsca.k	$⊢ K = {Base}_{R}$
	mdetrsca.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetrsca.r	$⊢ φ \to R \in CRing$
	mdetrsca.x	$⊢ φ \to X \in B$
	mdetrsca.y	$⊢ φ \to Y \in K$
	mdetrsca.z	$⊢ φ \to Z \in B$
	mdetrsca.i	$⊢ φ \to I \in N$
	mdetrsca.eq	$⊢ φ \to {X ↾}_{(\{I\} \times N)} = ((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})$
	mdetrsca.ne	$⊢ φ \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Z ↾}_{((N ∖ \{I\}) \times N)}$
Assertion	mdetrsca	$⊢ φ \to D (X) = Y \underset{˙}{\cdot} D (Z)$

Proof

Step	Hyp	Ref	Expression
1		mdetrsca.d	$⊢ D = N maDet R$
2		mdetrsca.a	$⊢ A = N Mat R$
3		mdetrsca.b	$⊢ B = {Base}_{A}$
4		mdetrsca.k	$⊢ K = {Base}_{R}$
5		mdetrsca.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		mdetrsca.r	$⊢ φ \to R \in CRing$
7		mdetrsca.x	$⊢ φ \to X \in B$
8		mdetrsca.y	$⊢ φ \to Y \in K$
9		mdetrsca.z	$⊢ φ \to Z \in B$
10		mdetrsca.i	$⊢ φ \to I \in N$
11		mdetrsca.eq	$⊢ φ \to {X ↾}_{(\{I\} \times N)} = ((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})$
12		mdetrsca.ne	$⊢ φ \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Z ↾}_{((N ∖ \{I\}) \times N)}$
13	11	oveqd	$⊢ φ \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I)$
14	13	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I)$
15	10	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I \in N$
16		snidg	$⊢ I \in N \to I \in \{I\}$
17	15 16	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I \in \{I\}$
18		eqid	$⊢ SymGrp (N) = SymGrp (N)$
19		eqid	$⊢ {Base}_{SymGrp (N)} = {Base}_{SymGrp (N)}$
20	18 19	symgbasf1o	$⊢ p \in {Base}_{SymGrp (N)} \to p : N \underset{1-1 onto}{⟶} N$
21	20	adantl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to p : N \underset{1-1 onto}{⟶} N$
22		f1of	$⊢ p : N \underset{1-1 onto}{⟶} N \to p : N ⟶ N$
23	21 22	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to p : N ⟶ N$
24	23 15	ffvelcdmd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to p (I) \in N$
25		ovres	$⊢ (I \in \{I\} \land p (I) \in N) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I X p (I)$
26	17 24 25	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I X p (I)$
27	17 24	opelxpd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ⟨I, p (I)⟩ \in (\{I\} \times N)$
28		snfi	$⊢ \{I\} \in Fin$
29	2 3	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
30	7 29	syl	$⊢ φ \to (N \in Fin \land R \in V)$
31	30	simpld	$⊢ φ \to N \in Fin$
32	31	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N \in Fin$
33		xpfi	$⊢ (\{I\} \in Fin \land N \in Fin) \to \{I\} \times N \in Fin$
34	28 32 33	sylancr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \times N \in Fin$
35	8	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Y \in K$
36	2 4 3	matbas2i	$⊢ Z \in B \to Z \in (K^{(N \times N)})$
37		elmapi	$⊢ Z \in (K^{(N \times N)}) \to Z : N \times N ⟶ K$
38	9 36 37	3syl	$⊢ φ \to Z : N \times N ⟶ K$
39	38	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Z : N \times N ⟶ K$
40	39	ffnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Z Fn (N \times N)$
41	15	snssd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \subseteq N$
42		xpss1	$⊢ \{I\} \subseteq N \to \{I\} \times N \subseteq N \times N$
43	41 42	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \times N \subseteq N \times N$
44	40 43	fnssresd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ({Z ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N)$
45		eqidd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land ⟨I, p (I)⟩ \in (\{I\} \times N)) \to ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩) = ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
46	34 35 44 45	ofc1	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land ⟨I, p (I)⟩ \in (\{I\} \times N)) \to (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) (⟨I, p (I)⟩) = Y \underset{˙}{\cdot} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
47	27 46	mpdan	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) (⟨I, p (I)⟩) = Y \underset{˙}{\cdot} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
48		df-ov	$⊢ I (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I) = (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) (⟨I, p (I)⟩)$
49		df-ov	$⊢ I ({Z ↾}_{(\{I\} \times N)}) p (I) = ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
50	49	oveq2i	$⊢ Y \underset{˙}{\cdot} (I ({Z ↾}_{(\{I\} \times N)}) p (I)) = Y \underset{˙}{\cdot} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
51	47 48 50	3eqtr4g	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I (((\{I\} \times N) \times \{Y\}) {\underset{˙}{\cdot}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I) = Y \underset{˙}{\cdot} (I ({Z ↾}_{(\{I\} \times N)}) p (I))$
52	14 26 51	3eqtr3d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) = Y \underset{˙}{\cdot} (I ({Z ↾}_{(\{I\} \times N)}) p (I))$
53		ovres	$⊢ (I \in \{I\} \land p (I) \in N) \to I ({Z ↾}_{(\{I\} \times N)}) p (I) = I Z p (I)$
54	17 24 53	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({Z ↾}_{(\{I\} \times N)}) p (I) = I Z p (I)$
55	54	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Y \underset{˙}{\cdot} (I ({Z ↾}_{(\{I\} \times N)}) p (I)) = Y \underset{˙}{\cdot} (I Z p (I))$
56	52 55	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) = Y \underset{˙}{\cdot} (I Z p (I))$
57	56	oveq1d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (I X p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (Y \underset{˙}{\cdot} (I Z p (I))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
58	6	crngringd	$⊢ φ \to R \in Ring$
59	58	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to R \in Ring$
60	39 15 24	fovcdmd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I Z p (I) \in K$
61		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
62	61 4	mgpbas	$⊢ K = {Base}_{{mulGrp}_{R}}$
63	61	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
64	6 63	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
65	64	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {mulGrp}_{R} \in CMnd$
66		difssd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N ∖ \{I\} \subseteq N$
67	32 66	ssfid	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N ∖ \{I\} \in Fin$
68		eldifi	$⊢ r \in (N ∖ \{I\}) \to r \in N$
69	38	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to Z : N \times N ⟶ K$
70		simpr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r \in N$
71	23	ffvelcdmda	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to p (r) \in N$
72	69 70 71	fovcdmd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r Z p (r) \in K$
73	68 72	sylan2	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r Z p (r) \in K$
74	73	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in (N ∖ \{I\}) r Z p (r) \in K$
75	62 65 67 74	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K$
76	4 5	ringass	$⊢ (R \in Ring \land (Y \in K \land I Z p (I) \in K \land \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K)) \to (Y \underset{˙}{\cdot} (I Z p (I))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = Y \underset{˙}{\cdot} ((I Z p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
77	59 35 60 75 76	syl13anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (Y \underset{˙}{\cdot} (I Z p (I))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = Y \underset{˙}{\cdot} ((I Z p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
78	57 77	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (I X p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = Y \underset{˙}{\cdot} ((I Z p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
79	61 5	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
80	2 4 3	matbas2i	$⊢ X \in B \to X \in (K^{(N \times N)})$
81		elmapi	$⊢ X \in (K^{(N \times N)}) \to X : N \times N ⟶ K$
82	7 80 81	3syl	$⊢ φ \to X : N \times N ⟶ K$
83	82	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to X : N \times N ⟶ K$
84	83 70 71	fovcdmd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r X p (r) \in K$
85		disjdif	$⊢ \{I\} \cap (N ∖ \{I\}) = \emptyset$
86	85	a1i	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \cap (N ∖ \{I\}) = \emptyset$
87		undif	$⊢ \{I\} \subseteq N \leftrightarrow \{I\} \cup (N ∖ \{I\}) = N$
88	41 87	sylib	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \cup (N ∖ \{I\}) = N$
89	88	eqcomd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N = \{I\} \cup (N ∖ \{I\})$
90	62 79 65 32 84 86 89	gsummptfidmsplit	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r X p (r)) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
91	65	cmnmndd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {mulGrp}_{R} \in Mnd$
92	82	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to X : N \times N ⟶ K$
93	92 15 24	fovcdmd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) \in K$
94		id	$⊢ r = I \to r = I$
95		fveq2	$⊢ r = I \to p (r) = p (I)$
96	94 95	oveq12d	$⊢ r = I \to r X p (r) = I X p (I)$
97	62 96	gsumsn	$⊢ ({mulGrp}_{R} \in Mnd \land I \in N \land I X p (I) \in K) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = I X p (I)$
98	91 15 93 97	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = I X p (I)$
99	12	oveqd	$⊢ φ \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r)$
100	99	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r)$
101		simpr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r \in (N ∖ \{I\})$
102	68 71	sylan2	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to p (r) \in N$
103		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r X p (r)$
104	101 102 103	syl2anc	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r X p (r)$
105		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r Z p (r)$
106	101 102 105	syl2anc	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r Z p (r)$
107	100 104 106	3eqtr3d	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r X p (r) = r Z p (r)$
108	107	mpteq2dva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (r \in (N ∖ \{I\}) ⟼ r X p (r)) = (r \in (N ∖ \{I\}) ⟼ r Z p (r))$
109	108	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r))$
110	98 109	oveq12d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) = (I X p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
111	90 110	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r X p (r)) = (I X p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
112	62 79 65 32 72 86 89	gsummptfidmsplit	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
113	94 95	oveq12d	$⊢ r = I \to r Z p (r) = I Z p (I)$
114	62 113	gsumsn	$⊢ ({mulGrp}_{R} \in Mnd \land I \in N \land I Z p (I) \in K) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = I Z p (I)$
115	91 15 60 114	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = I Z p (I)$
116	115	oveq1d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (I Z p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
117	112 116	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = (I Z p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
118	117	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Y \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = Y \underset{˙}{\cdot} ((I Z p (I)) \underset{˙}{\cdot} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
119	78 111 118	3eqtr4d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r X p (r)) = Y \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
120	119	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))) = (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
121	6	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to R \in CRing$
122		zrhpsgnmhm	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
123	58 31 122	syl2anc	$⊢ φ \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
124	19 62	mhmf	$⊢ ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R}) \to (ℤRHom (R) \circ pmSgn (N)) : {Base}_{SymGrp (N)} ⟶ K$
125	123 124	syl	$⊢ φ \to (ℤRHom (R) \circ pmSgn (N)) : {Base}_{SymGrp (N)} ⟶ K$
126	125	ffvelcdmda	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \in K$
127	4 5	crngcom	$⊢ (R \in CRing \land (ℤRHom (R) \circ pmSgn (N)) (p) \in K \land Y \in K) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} (ℤRHom (R) \circ pmSgn (N)) (p)$
128	121 126 35 127	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} (ℤRHom (R) \circ pmSgn (N)) (p)$
129	128	oveq1d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} Y) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (Y \underset{˙}{\cdot} (ℤRHom (R) \circ pmSgn (N)) (p)) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
130	72	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in N r Z p (r) \in K$
131	62 65 32 130	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K$
132	4 5	ringass	$⊢ (R \in Ring \land ((ℤRHom (R) \circ pmSgn (N)) (p) \in K \land Y \in K \land \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K)) \to ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} Y) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
133	59 126 35 131 132	syl13anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} Y) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
134	4 5	ringass	$⊢ (R \in Ring \land (Y \in K \land (ℤRHom (R) \circ pmSgn (N)) (p) \in K \land \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K)) \to (Y \underset{˙}{\cdot} (ℤRHom (R) \circ pmSgn (N)) (p)) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
135	59 35 126 131 134	syl13anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (Y \underset{˙}{\cdot} (ℤRHom (R) \circ pmSgn (N)) (p)) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
136	129 133 135	3eqtr3d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
137	120 136	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))) = Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
138	137	mpteq2dva	$⊢ φ \to (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
139	138	oveq2d	$⊢ φ \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} (Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
140		eqid	$⊢ 0_{R} = 0_{R}$
141	18 19	symgbasfi	$⊢ N \in Fin \to {Base}_{SymGrp (N)} \in Fin$
142	31 141	syl	$⊢ φ \to {Base}_{SymGrp (N)} \in Fin$
143	4 5 59 126 131	ringcld	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \in K$
144		eqid	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
145		ovexd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \in V$
146		fvexd	$⊢ φ \to 0_{R} \in V$
147	144 142 145 146	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{R}} ((p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
148	4 140 5 58 142 8 143 147	gsummulc2	$⊢ φ \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} (Y \underset{˙}{\cdot} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))) = Y \underset{˙}{\cdot} (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
149	139 148	eqtrd	$⊢ φ \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) = Y \underset{˙}{\cdot} (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
150		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
151		eqid	$⊢ pmSgn (N) = pmSgn (N)$
152	1 2 3 19 150 151 5 61	mdetleib2	$⊢ (R \in CRing \land X \in B) \to D (X) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
153	6 7 152	syl2anc	$⊢ φ \to D (X) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
154	1 2 3 19 150 151 5 61	mdetleib2	$⊢ (R \in CRing \land Z \in B) \to D (Z) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
155	6 9 154	syl2anc	$⊢ φ \to D (Z) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
156	155	oveq2d	$⊢ φ \to Y \underset{˙}{\cdot} D (Z) = Y \underset{˙}{\cdot} (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
157	149 153 156	3eqtr4d	$⊢ φ \to D (X) = Y \underset{˙}{\cdot} D (Z)$

Metamath Proof Explorer

Theorem mdetrsca

Proof