mdetrsca

Description: The determinant function is homogeneous for each row: The matrices X and Z are identical except for the I's row, and the I's row of the matrix X is the componentwise product of the I's row of the matrix Z and the scalar Y. In this case 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	ffvelrnd	$⊢ (φ \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		fnssres	$⊢ (Z Fn (N \times N) \land \{I\} \times N \subseteq N \times N) \to ({Z ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N)$
45	40 43 44	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ({Z ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N)$
46		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)⟩)$
47	34 35 45 46	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)⟩)$
48	27 47	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)⟩)$
49		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)⟩)$
50		df-ov	$⊢ I ({Z ↾}_{(\{I\} \times N)}) p (I) = ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
51	50	oveq2i	$⊢ Y \underset{˙}{\cdot} (I ({Z ↾}_{(\{I\} \times N)}) p (I)) = Y \underset{˙}{\cdot} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
52	48 49 51	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))$
53	14 26 52	3eqtr3d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) = Y \underset{˙}{\cdot} (I ({Z ↾}_{(\{I\} \times N)}) p (I))$
54		ovres	$⊢ (I \in \{I\} \land p (I) \in N) \to I ({Z ↾}_{(\{I\} \times N)}) p (I) = I Z p (I)$
55	17 24 54	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({Z ↾}_{(\{I\} \times N)}) p (I) = I Z p (I)$
56	55	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))$
57	53 56	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) = Y \underset{˙}{\cdot} (I Z p (I))$
58	57	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)))$
59		crngring	$⊢ R \in CRing \to R \in Ring$
60	6 59	syl	$⊢ φ \to R \in Ring$
61	60	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to R \in Ring$
62	39 15 24	fovrnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I Z p (I) \in K$
63		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
64	63 4	mgpbas	$⊢ K = {Base}_{{mulGrp}_{R}}$
65	63	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
66	6 65	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
67	66	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {mulGrp}_{R} \in CMnd$
68		difssd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N ∖ \{I\} \subseteq N$
69	32 68	ssfid	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N ∖ \{I\} \in Fin$
70		eldifi	$⊢ r \in (N ∖ \{I\}) \to r \in N$
71	38	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to Z : N \times N ⟶ K$
72		simpr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r \in N$
73	23	ffvelrnda	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to p (r) \in N$
74	71 72 73	fovrnd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r Z p (r) \in K$
75	70 74	sylan2	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r Z p (r) \in K$
76	75	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in (N ∖ \{I\}) r Z p (r) \in K$
77	64 67 69 76	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K$
78	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))))$
79	61 35 62 77 78	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))))$
80	58 79	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))))$
81	63 5	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
82	2 4 3	matbas2i	$⊢ X \in B \to X \in (K^{(N \times N)})$
83		elmapi	$⊢ X \in (K^{(N \times N)}) \to X : N \times N ⟶ K$
84	7 82 83	3syl	$⊢ φ \to X : N \times N ⟶ K$
85	84	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to X : N \times N ⟶ K$
86	85 72 73	fovrnd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r X p (r) \in K$
87		disjdif	$⊢ \{I\} \cap (N ∖ \{I\}) = \emptyset$
88	87	a1i	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \cap (N ∖ \{I\}) = \emptyset$
89		undif	$⊢ \{I\} \subseteq N \leftrightarrow \{I\} \cup (N ∖ \{I\}) = N$
90	41 89	sylib	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \cup (N ∖ \{I\}) = N$
91	90	eqcomd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N = \{I\} \cup (N ∖ \{I\})$
92	64 81 67 32 86 88 91	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)))$
93		cmnmnd	$⊢ {mulGrp}_{R} \in CMnd \to {mulGrp}_{R} \in Mnd$
94	67 93	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {mulGrp}_{R} \in Mnd$
95	84	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to X : N \times N ⟶ K$
96	95 15 24	fovrnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) \in K$
97		id	$⊢ r = I \to r = I$
98		fveq2	$⊢ r = I \to p (r) = p (I)$
99	97 98	oveq12d	$⊢ r = I \to r X p (r) = I X p (I)$
100	64 99	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)$
101	94 15 96 100	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = I X p (I)$
102	12	oveqd	$⊢ φ \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r)$
103	102	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)$
104		simpr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r \in (N ∖ \{I\})$
105	70 73	sylan2	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to p (r) \in N$
106		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r X p (r)$
107	104 105 106	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)$
108		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r Z p (r)$
109	104 105 108	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)$
110	103 107 109	3eqtr3d	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r X p (r) = r Z p (r)$
111	110	mpteq2dva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (r \in (N ∖ \{I\}) ⟼ r X p (r)) = (r \in (N ∖ \{I\}) ⟼ r Z p (r))$
112	111	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))$
113	101 112	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)))$
114	92 113	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)))$
115	64 81 67 32 74 88 91	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)))$
116	97 98	oveq12d	$⊢ r = I \to r Z p (r) = I Z p (I)$
117	64 116	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)$
118	94 15 62 117	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = I Z p (I)$
119	118	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)))$
120	115 119	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)))$
121	120	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))))$
122	80 114 121	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)))$
123	122	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))))$
124	6	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to R \in CRing$
125		zrhpsgnmhm	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
126	60 31 125	syl2anc	$⊢ φ \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
127	19 64	mhmf	$⊢ ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R}) \to (ℤRHom (R) \circ pmSgn (N)) : {Base}_{SymGrp (N)} ⟶ K$
128	126 127	syl	$⊢ φ \to (ℤRHom (R) \circ pmSgn (N)) : {Base}_{SymGrp (N)} ⟶ K$
129	128	ffvelrnda	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \in K$
130	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)$
131	124 129 35 130	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)$
132	131	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)))$
133	74	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in N r Z p (r) \in K$
134	64 67 32 133	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in K$
135	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))))$
136	61 129 35 134 135	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))))$
137	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))))$
138	61 35 129 134 137	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))))$
139	132 136 138	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))))$
140	123 139	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))))$
141	140	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)))))$
142	141	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)))))$
143		eqid	$⊢ 0_{R} = 0_{R}$
144		eqid	$⊢ +_{R} = +_{R}$
145	18 19	symgbasfi	$⊢ N \in Fin \to {Base}_{SymGrp (N)} \in Fin$
146	31 145	syl	$⊢ φ \to {Base}_{SymGrp (N)} \in Fin$
147	4 5	ringcl	$⊢ (R \in Ring \land (ℤRHom (R) \circ pmSgn (N)) (p) \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} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \in K$
148	61 129 134 147	syl3anc	$⊢ (φ \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$
149		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))))$
150		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$
151		fvexd	$⊢ φ \to 0_{R} \in V$
152	149 146 150 151	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)))))$
153	4 143 144 5 60 146 8 148 152	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)))))$
154	142 153	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)))))$
155		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
156		eqid	$⊢ pmSgn (N) = pmSgn (N)$
157	1 2 3 19 155 156 5 63	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))))$
158	6 7 157	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))))$
159	1 2 3 19 155 156 5 63	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))))$
160	6 9 159	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))))$
161	160	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)))))$
162	154 158 161	3eqtr4d	$⊢ φ \to D (X) = Y \underset{˙}{\cdot} D (Z)$

Metamath Proof Explorer

Theorem mdetrsca

Proof