Theorem mdetrlin 22567

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.)

Hypotheses

Ref	Expression
mdetrlin.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetrlin.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetrlin.b	⊢ 𝐵 = (Base‘𝐴)
mdetrlin.p	⊢ + = (+g‘𝑅)
mdetrlin.r	⊢ (𝜑 → 𝑅 ∈ CRing)
mdetrlin.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
mdetrlin.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
mdetrlin.z	⊢ (𝜑 → 𝑍 ∈ 𝐵)
mdetrlin.i	⊢ (𝜑 → 𝐼 ∈ 𝑁)
mdetrlin.eq	⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))
mdetrlin.ne1	⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
mdetrlin.ne2	⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))

Assertion

Ref	Expression
mdetrlin	⊢ (𝜑 → (𝐷‘𝑋) = ((𝐷‘𝑌) + (𝐷‘𝑍)))

Proof of Theorem mdetrlin

Dummy variables 𝑝 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6854	. . . . . 6 ⊢ (Base‘(SymGrp‘𝑁)) ∈ V
2		ovex 7400	. . . . . . 7 ⊢ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ V
3		eqid 2737	. . . . . . 7 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))
4	2, 3	fnmpti 6642	. . . . . 6 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁))
5		ovex 7400	. . . . . . 7 ⊢ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V
6		eqid 2737	. . . . . . 7 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
7	5, 6	fnmpti 6642	. . . . . 6 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁))
8		ofmpteq 7654	. . . . . 6 ⊢ (((Base‘(SymGrp‘𝑁)) ∈ V ∧ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁)) ∧ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁))) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
9	1, 4, 7, 8	mp3an 1464	. . . . 5 ⊢ ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
10		mdetrlin.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ CRing)
11		crngring 20226	. . . . . . . . . 10 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	10, 11	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
13	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
14		mdetrlin.y	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
15		mdetrlin.a	. . . . . . . . . . . . . 14 ⊢ 𝐴 = (𝑁 Mat 𝑅)
16		mdetrlin.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐴)
17	15, 16	matrcl 22377	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
18	14, 17	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
19	18	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ Fin)
20		zrhpsgnmhm 21564	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
21	12, 19, 20	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
22		eqid 2737	. . . . . . . . . . 11 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
23		eqid 2737	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
24		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
25	23, 24	mgpbas 20126	. . . . . . . . . . 11 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
26	22, 25	mhmf 18757	. . . . . . . . . 10 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
27	21, 26	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
28	27	ffvelcdmda 7037	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
29	23	crngmgp 20222	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
30	10, 29	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
31	30	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
32	19	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
33	15, 24, 16	matbas2i 22387	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
34		elmapi 8796	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
35	14, 33, 34	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
36	35	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
37		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁)
38		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
39	38, 22	symgbasf 19351	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁⟶𝑁)
40	39	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
41	40	ffvelcdmda 7037	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁)
42	36, 37, 41	fovcdmd 7539	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑌(𝑝‘𝑟)) ∈ (Base‘𝑅))
43	42	ralrimiva 3130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑌(𝑝‘𝑟)) ∈ (Base‘𝑅))
44	25, 31, 32, 43	gsummptcl 19942	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅))
45		mdetrlin.z	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
46	15, 24, 16	matbas2i 22387	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
47		elmapi 8796	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
48	45, 46, 47	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
49	48	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
50	49, 37, 41	fovcdmd 7539	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ (Base‘𝑅))
51	50	ralrimiva 3130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ (Base‘𝑅))
52	25, 31, 32, 51	gsummptcl 19942	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅))
53		mdetrlin.p	. . . . . . . . 9 ⊢ + = (+g‘𝑅)
54		eqid 2737	. . . . . . . . 9 ⊢ (.r‘𝑅) = (.r‘𝑅)
55	24, 53, 54	ringdi 20242	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
56	13, 28, 44, 52, 55	syl13anc 1375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
57		cmnmnd 19772	. . . . . . . . . . . . 13 ⊢ ((mulGrp‘𝑅) ∈ CMnd → (mulGrp‘𝑅) ∈ Mnd)
58	31, 57	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd)
59		mdetrlin.i	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
60	59	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ 𝑁)
61	35	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
62	40, 60	ffvelcdmd 7038	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁)
63	61, 60, 62	fovcdmd 7539	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑌(𝑝‘𝐼)) ∈ (Base‘𝑅))
64		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼)
65		fveq2 6841	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼))
66	64, 65	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑟𝑌(𝑝‘𝑟)) = (𝐼𝑌(𝑝‘𝐼)))
67	25, 66	gsumsn 19929	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑌(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) = (𝐼𝑌(𝑝‘𝐼)))
68	58, 60, 63, 67	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) = (𝐼𝑌(𝑝‘𝐼)))
69	68, 63	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅))
70	48	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
71	70, 60, 62	fovcdmd 7539	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ (Base‘𝑅))
72	64, 65	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼)))
73	25, 72	gsumsn 19929	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
74	58, 60, 71, 73	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
75	74, 71	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅))
76		difssd 4078	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁)
77	32, 76	ssfid 9179	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin)
78		eldifi 4072	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁)
79		mdetrlin.x	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
80	15, 24, 16	matbas2i 22387	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
81		elmapi 8796	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
82	79, 80, 81	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
83	82	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
84	83, 37, 41	fovcdmd 7539	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅))
85	78, 84	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅))
86	85	ralrimiva 3130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅))
87	25, 31, 77, 86	gsummptcl 19942	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) ∈ (Base‘𝑅))
88	24, 53, 54	ringdir 20243	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) ∈ (Base‘𝑅))) → ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))))
89	13, 69, 75, 87, 88	syl13anc 1375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))))
90	23, 54	mgpplusg 20125	. . . . . . . . . . 11 ⊢ (.r‘𝑅) = (+g‘(mulGrp‘𝑅))
91		disjdif 4413	. . . . . . . . . . . 12 ⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅
92	91	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅)
93	59	snssd 4731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐼} ⊆ 𝑁)
94	93	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁)
95		undif 4423	. . . . . . . . . . . . 13 ⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
96	94, 95	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
97	96	eqcomd 2743	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼})))
98	25, 90, 31, 32, 84, 92, 97	gsummptfidmsplit 19905	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
99		mdetrlin.eq	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))
100	99	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))
101	100	oveqd 7384	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)))
102		xpss1 5650	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
103	94, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
104	61, 103	fssresd 6708	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅))
105	104	ffnd 6670	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
106	70, 103	fssresd 6708	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅))
107	106	ffnd 6670	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
108		snex 5382	. . . . . . . . . . . . . . . . 17 ⊢ {𝐼} ∈ V
109		xpexg 7704	. . . . . . . . . . . . . . . . 17 ⊢ (({𝐼} ∈ V ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ V)
110	108, 32, 109	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ V)
111		snidg 4605	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼})
112	60, 111	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼})
113	112, 62	opelxpd 5670	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁))
114		fnfvof 7648	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁) ∧ (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) ∧ (({𝐼} × 𝑁) ∈ V ∧ ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
115	105, 107, 110, 113, 114	syl22anc 839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
116		df-ov 7370	. . . . . . . . . . . . . . 15 ⊢ (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩)
117		df-ov 7370	. . . . . . . . . . . . . . . 16 ⊢ (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)
118		df-ov 7370	. . . . . . . . . . . . . . . 16 ⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)
119	117, 118	oveq12i 7379	. . . . . . . . . . . . . . 15 ⊢ ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩))
120	115, 116, 119	3eqtr4g 2797	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
121	101, 120	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
122		ovres 7533	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
123	112, 62, 122	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
124		ovres 7533	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑌(𝑝‘𝐼)))
125	112, 62, 124	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑌(𝑝‘𝐼)))
126		ovres 7533	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
127	112, 62, 126	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
128	125, 127	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼))))
129	121, 123, 128	3eqtr3d 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼))))
130	82	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
131	130, 60, 62	fovcdmd 7539	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ (Base‘𝑅))
132	64, 65	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼)))
133	25, 132	gsumsn 19929	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
134	58, 60, 131, 133	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
135	68, 74	oveq12d 7385	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼))))
136	129, 134, 135	3eqtr4d 2782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))))
137	136	oveq1d 7382	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
138	98, 137	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
139	25, 90, 31, 32, 42, 92, 97	gsummptfidmsplit 19905	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))))))
140		mdetrlin.ne1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
141	140	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
142	141	oveqd 7384	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
143		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼}))
144	78, 41	sylan2 594	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁)
145		ovres 7533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
146	143, 144, 145	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
147		ovres 7533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑌(𝑝‘𝑟)))
148	143, 144, 147	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑌(𝑝‘𝑟)))
149	142, 146, 148	3eqtr3rd 2781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑌(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
150	149	mpteq2dva 5179	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))
151	150	oveq2d 7383	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))
152	151	oveq2d 7383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
153	139, 152	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
154	25, 90, 31, 32, 50, 92, 97	gsummptfidmsplit 19905	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
155		mdetrlin.ne2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
156	155	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
157	156	oveqd 7384	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
158		ovres 7533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
159	143, 144, 158	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
160	157, 146, 159	3eqtr3rd 2781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
161	160	mpteq2dva 5179	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))
162	161	oveq2d 7383	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))
163	162	oveq2d 7383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
164	154, 163	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
165	153, 164	oveq12d 7385	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))))
166	89, 138, 165	3eqtr4rd 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))
167	166	oveq2d 7383	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))
168	56, 167	eqtr3d 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))
169	168	mpteq2dva 5179	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))
170	9, 169	eqtrid 2784	. . . 4 ⊢ (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))
171	170	oveq2d 7383	. . 3 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
172		ringcmn 20263	. . . . 5 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
173	10, 11, 172	3syl 18	. . . 4 ⊢ (𝜑 → 𝑅 ∈ CMnd)
174	38, 22	symgbasfi 19354	. . . . 5 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
175	19, 174	syl 17	. . . 4 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
176	24, 54	ringcl 20231	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ (Base‘𝑅))
177	13, 28, 44, 176	syl3anc 1374	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ (Base‘𝑅))
178	24, 54	ringcl 20231	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ (Base‘𝑅))
179	13, 28, 52, 178	syl3anc 1374	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ (Base‘𝑅))
180	24, 53, 173, 175, 177, 179, 3, 6	gsummptfidmadd2 19901	. . 3 ⊢ (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
181	171, 180	eqtr3d 2774	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
182		mdetrlin.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
183		eqid 2737	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
184		eqid 2737	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
185	182, 15, 16, 22, 183, 184, 54, 23	mdetleib2 22553	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
186	10, 79, 185	syl2anc 585	. 2 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
187	182, 15, 16, 22, 183, 184, 54, 23	mdetleib2 22553	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∈ 𝐵) → (𝐷‘𝑌) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))))
188	10, 14, 187	syl2anc 585	. . 3 ⊢ (𝜑 → (𝐷‘𝑌) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))))
189	182, 15, 16, 22, 183, 184, 54, 23	mdetleib2 22553	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
190	10, 45, 189	syl2anc 585	. . 3 ⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
191	188, 190	oveq12d 7385	. 2 ⊢ (𝜑 → ((𝐷‘𝑌) + (𝐷‘𝑍)) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
192	181, 186, 191	3eqtr4d 2782	1 ⊢ (𝜑 → (𝐷‘𝑋) = ((𝐷‘𝑌) + (𝐷‘𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  ∅c0 4274  {csn 4568  ⟨cop 4574   ↦ cmpt 5167   × cxp 5629   ↾ cres 5633   ∘ ccom 5635   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499  (class class class)co 7367   ∘_f cof 7629   ↑_m cmap 8773  Fincfn 8893  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221   Σ_g cgsu 17403  Mndcmnd 18702   MndHom cmhm 18749  SymGrpcsymg 19344  pmSgncpsgn 19464  CMndccmn 19755  mulGrpcmgp 20121  Ringcrg 20214  CRingccrg 20215  ℤRHomczrh 21479   Mat cmat 22372   maDet cmdat 22549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-addf 11117  ax-mulf 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1514  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-ot 4577  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6266  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-tpos 8176  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-sup 9355  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-xnn0 12511  df-z 12525  df-dec 12645  df-uz 12789  df-rp 12943  df-fz 13462  df-fzo 13609  df-seq 13964  df-exp 14024  df-hash 14293  df-word 14476  df-lsw 14525  df-concat 14533  df-s1 14559  df-substr 14604  df-pfx 14634  df-splice 14712  df-reverse 14721  df-s2 14810  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mhm 18751  df-submnd 18752  df-efmnd 18837  df-grp 18912  df-minusg 18913  df-mulg 19044  df-subg 19099  df-ghm 19188  df-gim 19234  df-cntz 19292  df-oppg 19321  df-symg 19345  df-pmtr 19417  df-psgn 19466  df-cmn 19757  df-abl 19758  df-mgp 20122  df-rng 20134  df-ur 20163  df-ring 20216  df-cring 20217  df-oppr 20317  df-dvdsr 20337  df-unit 20338  df-invr 20368  df-dvr 20381  df-rhm 20452  df-subrng 20523  df-subrg 20547  df-drng 20708  df-sra 21168  df-rgmod 21169  df-cnfld 21353  df-zring 21427  df-zrh 21483  df-dsmm 21712  df-frlm 21727  df-mat 22373  df-mdet 22550

This theorem is referenced by:  mdetrlin2  22572  mdetuni0  22586  mdetmul  22588