mdetrlin

Description: The determinant function is additive for each row: The matrices X, Y, Z are identical except for the I's row, and the I's row of the matrix X is the componentwise sum of the I's row of the matrices Y and Z. In this case the determinant of X is the sum of the determinants of Y and Z. (Contributed by SO, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	mdetrlin.d	$⊢ D = N maDet R$
	mdetrlin.a	$⊢ A = N Mat R$
	mdetrlin.b	$⊢ B = {Base}_{A}$
	mdetrlin.p	$⊢ \underset{˙}{+} = +_{R}$
	mdetrlin.r	$⊢ φ \to R \in CRing$
	mdetrlin.x	$⊢ φ \to X \in B$
	mdetrlin.y	$⊢ φ \to Y \in B$
	mdetrlin.z	$⊢ φ \to Z \in B$
	mdetrlin.i	$⊢ φ \to I \in N$
	mdetrlin.eq	$⊢ φ \to {X ↾}_{(\{I\} \times N)} = ({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})$
	mdetrlin.ne1	$⊢ φ \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Y ↾}_{((N ∖ \{I\}) \times N)}$
	mdetrlin.ne2	$⊢ φ \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Z ↾}_{((N ∖ \{I\}) \times N)}$
Assertion	mdetrlin	$⊢ φ \to D (X) = D (Y) \underset{˙}{+} D (Z)$

Proof

Step	Hyp	Ref	Expression
1		mdetrlin.d	$⊢ D = N maDet R$
2		mdetrlin.a	$⊢ A = N Mat R$
3		mdetrlin.b	$⊢ B = {Base}_{A}$
4		mdetrlin.p	$⊢ \underset{˙}{+} = +_{R}$
5		mdetrlin.r	$⊢ φ \to R \in CRing$
6		mdetrlin.x	$⊢ φ \to X \in B$
7		mdetrlin.y	$⊢ φ \to Y \in B$
8		mdetrlin.z	$⊢ φ \to Z \in B$
9		mdetrlin.i	$⊢ φ \to I \in N$
10		mdetrlin.eq	$⊢ φ \to {X ↾}_{(\{I\} \times N)} = ({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})$
11		mdetrlin.ne1	$⊢ φ \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Y ↾}_{((N ∖ \{I\}) \times N)}$
12		mdetrlin.ne2	$⊢ φ \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Z ↾}_{((N ∖ \{I\}) \times N)}$
13		fvex	$⊢ {Base}_{SymGrp (N)} \in V$
14		ovex	$⊢ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \in V$
15		eqid	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))))$
16	14 15	fnmpti	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) Fn {Base}_{SymGrp (N)}$
17		ovex	$⊢ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \in V$
18		eqid	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
19	17 18	fnmpti	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) Fn {Base}_{SymGrp (N)}$
20		ofmpteq	$⊢ ({Base}_{SymGrp (N)} \in V \land (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) Fn {Base}_{SymGrp (N)} \land (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) Fn {Base}_{SymGrp (N)}) \to (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) {\underset{˙}{+}}_{f} (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) \underset{˙}{+} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
21	13 16 19 20	mp3an	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) {\underset{˙}{+}}_{f} (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) \underset{˙}{+} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
22		crngring	$⊢ R \in CRing \to R \in Ring$
23	5 22	syl	$⊢ φ \to R \in Ring$
24	23	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to R \in Ring$
25	2 3	matrcl	$⊢ Y \in B \to (N \in Fin \land R \in V)$
26	7 25	syl	$⊢ φ \to (N \in Fin \land R \in V)$
27	26	simpld	$⊢ φ \to N \in Fin$
28		zrhpsgnmhm	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
29	23 27 28	syl2anc	$⊢ φ \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
30		eqid	$⊢ {Base}_{SymGrp (N)} = {Base}_{SymGrp (N)}$
31		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
32		eqid	$⊢ {Base}_{R} = {Base}_{R}$
33	31 32	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
34	30 33	mhmf	$⊢ ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R}) \to (ℤRHom (R) \circ pmSgn (N)) : {Base}_{SymGrp (N)} ⟶ {Base}_{R}$
35	29 34	syl	$⊢ φ \to (ℤRHom (R) \circ pmSgn (N)) : {Base}_{SymGrp (N)} ⟶ {Base}_{R}$
36	35	ffvelrnda	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \in {Base}_{R}$
37	31	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
38	5 37	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
39	38	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {mulGrp}_{R} \in CMnd$
40	27	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N \in Fin$
41	2 32 3	matbas2i	$⊢ Y \in B \to Y \in ({Base}_{R}^{(N \times N)})$
42		elmapi	$⊢ Y \in ({Base}_{R}^{(N \times N)}) \to Y : N \times N ⟶ {Base}_{R}$
43	7 41 42	3syl	$⊢ φ \to Y : N \times N ⟶ {Base}_{R}$
44	43	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to Y : N \times N ⟶ {Base}_{R}$
45		simpr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r \in N$
46		eqid	$⊢ SymGrp (N) = SymGrp (N)$
47	46 30	symgbasf	$⊢ p \in {Base}_{SymGrp (N)} \to p : N ⟶ N$
48	47	adantl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to p : N ⟶ N$
49	48	ffvelrnda	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to p (r) \in N$
50	44 45 49	fovrnd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r Y p (r) \in {Base}_{R}$
51	50	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in N r Y p (r) \in {Base}_{R}$
52	33 39 40 51	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Y p (r)) \in {Base}_{R}$
53	2 32 3	matbas2i	$⊢ Z \in B \to Z \in ({Base}_{R}^{(N \times N)})$
54		elmapi	$⊢ Z \in ({Base}_{R}^{(N \times N)}) \to Z : N \times N ⟶ {Base}_{R}$
55	8 53 54	3syl	$⊢ φ \to Z : N \times N ⟶ {Base}_{R}$
56	55	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to Z : N \times N ⟶ {Base}_{R}$
57	56 45 49	fovrnd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r Z p (r) \in {Base}_{R}$
58	57	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in N r Z p (r) \in {Base}_{R}$
59	33 39 40 58	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in {Base}_{R}$
60		eqid	$⊢ \cdot_{R} = \cdot_{R}$
61	32 4 60	ringdi	$⊢ (R \in Ring \land ((ℤRHom (R) \circ pmSgn (N)) (p) \in {Base}_{R} \land \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Y p (r)) \in {Base}_{R} \land \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in {Base}_{R})) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} ((\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) \underset{˙}{+} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
62	24 36 52 59 61	syl13anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} ((\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) \underset{˙}{+} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
63		cmnmnd	$⊢ {mulGrp}_{R} \in CMnd \to {mulGrp}_{R} \in Mnd$
64	39 63	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {mulGrp}_{R} \in Mnd$
65	9	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I \in N$
66	43	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Y : N \times N ⟶ {Base}_{R}$
67	48 65	ffvelrnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to p (I) \in N$
68	66 65 67	fovrnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I Y p (I) \in {Base}_{R}$
69		id	$⊢ r = I \to r = I$
70		fveq2	$⊢ r = I \to p (r) = p (I)$
71	69 70	oveq12d	$⊢ r = I \to r Y p (r) = I Y p (I)$
72	33 71	gsumsn	$⊢ ({mulGrp}_{R} \in Mnd \land I \in N \land I Y p (I) \in {Base}_{R}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Y p (r)) = I Y p (I)$
73	64 65 68 72	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Y p (r)) = I Y p (I)$
74	73 68	eqeltrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Y p (r)) \in {Base}_{R}$
75	55	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to Z : N \times N ⟶ {Base}_{R}$
76	75 65 67	fovrnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I Z p (I) \in {Base}_{R}$
77	69 70	oveq12d	$⊢ r = I \to r Z p (r) = I Z p (I)$
78	33 77	gsumsn	$⊢ ({mulGrp}_{R} \in Mnd \land I \in N \land I Z p (I) \in {Base}_{R}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = I Z p (I)$
79	64 65 76 78	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = I Z p (I)$
80	79 76	eqeltrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in {Base}_{R}$
81		difssd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N ∖ \{I\} \subseteq N$
82	40 81	ssfid	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N ∖ \{I\} \in Fin$
83		eldifi	$⊢ r \in (N ∖ \{I\}) \to r \in N$
84	2 32 3	matbas2i	$⊢ X \in B \to X \in ({Base}_{R}^{(N \times N)})$
85		elmapi	$⊢ X \in ({Base}_{R}^{(N \times N)}) \to X : N \times N ⟶ {Base}_{R}$
86	6 84 85	3syl	$⊢ φ \to X : N \times N ⟶ {Base}_{R}$
87	86	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to X : N \times N ⟶ {Base}_{R}$
88	87 45 49	fovrnd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in N) \to r X p (r) \in {Base}_{R}$
89	83 88	sylan2	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r X p (r) \in {Base}_{R}$
90	89	ralrimiva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \forall r \in (N ∖ \{I\}) r X p (r) \in {Base}_{R}$
91	33 39 82 90	gsummptcl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) \in {Base}_{R}$
92	32 4 60	ringdir	$⊢ (R \in Ring \land (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Y p (r)) \in {Base}_{R} \land \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in {Base}_{R} \land \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) \in {Base}_{R})) \to ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) = ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) \underset{˙}{+} ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
93	24 74 80 91 92	syl13anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) = ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) \underset{˙}{+} ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
94	31 60	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
95		disjdif	$⊢ \{I\} \cap (N ∖ \{I\}) = \emptyset$
96	95	a1i	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \cap (N ∖ \{I\}) = \emptyset$
97	9	snssd	$⊢ φ \to \{I\} \subseteq N$
98	97	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \subseteq N$
99		undif	$⊢ \{I\} \subseteq N \leftrightarrow \{I\} \cup (N ∖ \{I\}) = N$
100	98 99	sylib	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \cup (N ∖ \{I\}) = N$
101	100	eqcomd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to N = \{I\} \cup (N ∖ \{I\})$
102	33 94 39 40 88 96 101	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))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
103	10	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to {X ↾}_{(\{I\} \times N)} = ({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})$
104	103	oveqd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I (({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I)$
105		xpss1	$⊢ \{I\} \subseteq N \to \{I\} \times N \subseteq N \times N$
106	98 105	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \times N \subseteq N \times N$
107	66 106	fssresd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ({Y ↾}_{(\{I\} \times N)}) : \{I\} \times N ⟶ {Base}_{R}$
108	107	ffnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ({Y ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N)$
109	75 106	fssresd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ({Z ↾}_{(\{I\} \times N)}) : \{I\} \times N ⟶ {Base}_{R}$
110	109	ffnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ({Z ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N)$
111		snex	$⊢ \{I\} \in V$
112		xpexg	$⊢ (\{I\} \in V \land N \in Fin) \to \{I\} \times N \in V$
113	111 40 112	sylancr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \{I\} \times N \in V$
114		snidg	$⊢ I \in N \to I \in \{I\}$
115	65 114	syl	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I \in \{I\}$
116	115 67	opelxpd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ⟨I, p (I)⟩ \in (\{I\} \times N)$
117		fnfvof	$⊢ ((({Y ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N) \land ({Z ↾}_{(\{I\} \times N)}) Fn (\{I\} \times N)) \land (\{I\} \times N \in V \land ⟨I, p (I)⟩ \in (\{I\} \times N))) \to (({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})) (⟨I, p (I)⟩) = ({Y ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩) \underset{˙}{+} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
118	108 110 113 116 117	syl22anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})) (⟨I, p (I)⟩) = ({Y ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩) \underset{˙}{+} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
119		df-ov	$⊢ I (({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I) = (({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})) (⟨I, p (I)⟩)$
120		df-ov	$⊢ I ({Y ↾}_{(\{I\} \times N)}) p (I) = ({Y ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
121		df-ov	$⊢ I ({Z ↾}_{(\{I\} \times N)}) p (I) = ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
122	120 121	oveq12i	$⊢ (I ({Y ↾}_{(\{I\} \times N)}) p (I)) \underset{˙}{+} (I ({Z ↾}_{(\{I\} \times N)}) p (I)) = ({Y ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩) \underset{˙}{+} ({Z ↾}_{(\{I\} \times N)}) (⟨I, p (I)⟩)$
123	118 119 122	3eqtr4g	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I (({Y ↾}_{(\{I\} \times N)}) {\underset{˙}{+}}_{f} ({Z ↾}_{(\{I\} \times N)})) p (I) = (I ({Y ↾}_{(\{I\} \times N)}) p (I)) \underset{˙}{+} (I ({Z ↾}_{(\{I\} \times N)}) p (I))$
124	104 123	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = (I ({Y ↾}_{(\{I\} \times N)}) p (I)) \underset{˙}{+} (I ({Z ↾}_{(\{I\} \times N)}) p (I))$
125		ovres	$⊢ (I \in \{I\} \land p (I) \in N) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I X p (I)$
126	115 67 125	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({X ↾}_{(\{I\} \times N)}) p (I) = I X p (I)$
127		ovres	$⊢ (I \in \{I\} \land p (I) \in N) \to I ({Y ↾}_{(\{I\} \times N)}) p (I) = I Y p (I)$
128	115 67 127	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({Y ↾}_{(\{I\} \times N)}) p (I) = I Y p (I)$
129		ovres	$⊢ (I \in \{I\} \land p (I) \in N) \to I ({Z ↾}_{(\{I\} \times N)}) p (I) = I Z p (I)$
130	115 67 129	syl2anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I ({Z ↾}_{(\{I\} \times N)}) p (I) = I Z p (I)$
131	128 130	oveq12d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (I ({Y ↾}_{(\{I\} \times N)}) p (I)) \underset{˙}{+} (I ({Z ↾}_{(\{I\} \times N)}) p (I)) = (I Y p (I)) \underset{˙}{+} (I Z p (I))$
132	124 126 131	3eqtr3d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) = (I Y p (I)) \underset{˙}{+} (I Z p (I))$
133	86	adantr	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to X : N \times N ⟶ {Base}_{R}$
134	133 65 67	fovrnd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to I X p (I) \in {Base}_{R}$
135	69 70	oveq12d	$⊢ r = I \to r X p (r) = I X p (I)$
136	33 135	gsumsn	$⊢ ({mulGrp}_{R} \in Mnd \land I \in N \land I X p (I) \in {Base}_{R}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = I X p (I)$
137	64 65 134 136	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = I X p (I)$
138	73 79	oveq12d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (I Y p (I)) \underset{˙}{+} (I Z p (I))$
139	132 137 138	3eqtr4d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r)) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
140	139	oveq1d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))) = ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
141	102 140	eqtrd	$⊢ (φ \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 Y p (r))) \underset{˙}{+} (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
142	33 94 39 40 50 96 101	gsummptfidmsplit	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Y p (r)) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))$
143	11	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Y ↾}_{((N ∖ \{I\}) \times N)}$
144	143	oveqd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r ({Y ↾}_{((N ∖ \{I\}) \times N)}) p (r)$
145		simpr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r \in (N ∖ \{I\})$
146	83 49	sylan2	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to p (r) \in N$
147		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({X ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r X p (r)$
148	145 146 147	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)$
149		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({Y ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r Y p (r)$
150	145 146 149	syl2anc	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r ({Y ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r Y p (r)$
151	144 148 150	3eqtr3rd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r Y p (r) = r X p (r)$
152	151	mpteq2dva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (r \in (N ∖ \{I\}) ⟼ r Y p (r)) = (r \in (N ∖ \{I\}) ⟼ r X p (r))$
153	152	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r Y p (r)) = \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r))$
154	153	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
155	142 154	eqtrd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Y p (r)) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
156	33 94 39 40 57 96 101	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))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))$
157	12	ad2antrr	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to {X ↾}_{((N ∖ \{I\}) \times N)} = {Z ↾}_{((N ∖ \{I\}) \times N)}$
158	157	oveqd	$⊢ ((φ \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)$
159		ovres	$⊢ (r \in (N ∖ \{I\}) \land p (r) \in N) \to r ({Z ↾}_{((N ∖ \{I\}) \times N)}) p (r) = r Z p (r)$
160	145 146 159	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)$
161	158 148 160	3eqtr3rd	$⊢ ((φ \land p \in {Base}_{SymGrp (N)}) \land r \in (N ∖ \{I\})) \to r Z p (r) = r X p (r)$
162	161	mpteq2dva	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (r \in (N ∖ \{I\}) ⟼ r Z p (r)) = (r \in (N ∖ \{I\}) ⟼ r X p (r))$
163	162	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r Z p (r)) = \underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}} (r X p (r))$
164	163	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = (\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
165	156 164	eqtrd	$⊢ (φ \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))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
166	155 165	oveq12d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) \underset{˙}{+} ((\underset{r \in \{I\}}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \cdot_{R} (\underset{r \in N ∖ \{I\}}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
167	93 141 166	3eqtr4rd	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) = \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r X p (r))$
168	167	oveq2d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} ((\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \underset{˙}{+} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
169	62 168	eqtr3d	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) \underset{˙}{+} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r)))$
170	169	mpteq2dva	$⊢ φ \to (p \in {Base}_{SymGrp (N)} ⟼ ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) \underset{˙}{+} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))) = (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
171	21 170	eqtrid	$⊢ φ \to (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) {\underset{˙}{+}}_{f} (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))) = (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
172	171	oveq2d	$⊢ φ \to \sum_{R} ((p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) {\underset{˙}{+}}_{f} (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
173		ringcmn	$⊢ R \in Ring \to R \in CMnd$
174	5 22 173	3syl	$⊢ φ \to R \in CMnd$
175	46 30	symgbasfi	$⊢ N \in Fin \to {Base}_{SymGrp (N)} \in Fin$
176	27 175	syl	$⊢ φ \to {Base}_{SymGrp (N)} \in Fin$
177	32 60	ringcl	$⊢ (R \in Ring \land (ℤRHom (R) \circ pmSgn (N)) (p) \in {Base}_{R} \land \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Y p (r)) \in {Base}_{R}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \in {Base}_{R}$
178	24 36 52 177	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))) \in {Base}_{R}$
179	32 60	ringcl	$⊢ (R \in Ring \land (ℤRHom (R) \circ pmSgn (N)) (p) \in {Base}_{R} \land \underset{r \in N}{\sum_{{mulGrp}_{R}}} (r Z p (r)) \in {Base}_{R}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \in {Base}_{R}$
180	24 36 59 179	syl3anc	$⊢ (φ \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))) \in {Base}_{R}$
181	32 4 174 176 178 180 15 18	gsummptfidmadd2	$⊢ φ \to \sum_{R} ((p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r)))) {\underset{˙}{+}}_{f} (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))) = (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))))) \underset{˙}{+} (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
182	172 181	eqtr3d	$⊢ φ \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r)))) = (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))))) \underset{˙}{+} (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
183		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
184		eqid	$⊢ pmSgn (N) = pmSgn (N)$
185	1 2 3 30 183 184 60 31	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) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
186	5 6 185	syl2anc	$⊢ φ \to D (X) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r X p (r))))$
187	1 2 3 30 183 184 60 31	mdetleib2	$⊢ (R \in CRing \land Y \in B) \to D (Y) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))))$
188	5 7 187	syl2anc	$⊢ φ \to D (Y) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))))$
189	1 2 3 30 183 184 60 31	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) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
190	5 8 189	syl2anc	$⊢ φ \to D (Z) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r))))$
191	188 190	oveq12d	$⊢ φ \to D (Y) \underset{˙}{+} D (Z) = (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Y p (r))))) \underset{˙}{+} (\underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}}, ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{r \in N}{\sum_{{mulGrp}_{R}}}, (r Z p (r)))))$
192	182 186 191	3eqtr4d	$⊢ φ \to D (X) = D (Y) \underset{˙}{+} D (Z)$

Metamath Proof Explorer

Theorem mdetrlin

Proof