Theorem mdetrlin 22540

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 6889	. . . . . 6 ⊢ (Base‘(SymGrp‘𝑁)) ∈ V
2		ovex 7438	. . . . . . 7 ⊢ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ V
3		eqid 2735	. . . . . . 7 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))
4	2, 3	fnmpti 6681	. . . . . 6 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁))
5		ovex 7438	. . . . . . 7 ⊢ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V
6		eqid 2735	. . . . . . 7 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
7	5, 6	fnmpti 6681	. . . . . 6 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) Fn (Base‘(SymGrp‘𝑁))
8		ofmpteq 7694	. . . . . 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 1463	. . . . 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 20205	. . . . . . . . . 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 22350	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
18	14, 17	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
19	18	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ Fin)
20		zrhpsgnmhm 21544	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
21	12, 19, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
22		eqid 2735	. . . . . . . . . . 11 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
23		eqid 2735	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
24		eqid 2735	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
25	23, 24	mgpbas 20105	. . . . . . . . . . 11 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
26	22, 25	mhmf 18767	. . . . . . . . . 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 7074	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
29	23	crngmgp 20201	. . . . . . . . . . 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 22360	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
34		elmapi 8863	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
35	14, 33, 34	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
36	35	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
37		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁)
38		eqid 2735	. . . . . . . . . . . . . 14 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
39	38, 22	symgbasf 19357	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁⟶𝑁)
40	39	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
41	40	ffvelcdmda 7074	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁)
42	36, 37, 41	fovcdmd 7579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑌(𝑝‘𝑟)) ∈ (Base‘𝑅))
43	42	ralrimiva 3132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑌(𝑝‘𝑟)) ∈ (Base‘𝑅))
44	25, 31, 32, 43	gsummptcl 19948	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅))
45		mdetrlin.z	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
46	15, 24, 16	matbas2i 22360	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
47		elmapi 8863	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
48	45, 46, 47	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
49	48	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
50	49, 37, 41	fovcdmd 7579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ (Base‘𝑅))
51	50	ralrimiva 3132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ (Base‘𝑅))
52	25, 31, 32, 51	gsummptcl 19948	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅))
53		mdetrlin.p	. . . . . . . . 9 ⊢ + = (+g‘𝑅)
54		eqid 2735	. . . . . . . . 9 ⊢ (.r‘𝑅) = (.r‘𝑅)
55	24, 53, 54	ringdi 20221	. . . . . . . 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 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
57		cmnmnd 19778	. . . . . . . . . . . . 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 7075	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁)
63	61, 60, 62	fovcdmd 7579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑌(𝑝‘𝐼)) ∈ (Base‘𝑅))
64		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼)
65		fveq2 6876	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼))
66	64, 65	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑟𝑌(𝑝‘𝑟)) = (𝐼𝑌(𝑝‘𝐼)))
67	25, 66	gsumsn 19935	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑌(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) = (𝐼𝑌(𝑝‘𝐼)))
68	58, 60, 63, 67	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) = (𝐼𝑌(𝑝‘𝐼)))
69	68, 63	eqeltrd 2834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅))
70	48	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
71	70, 60, 62	fovcdmd 7579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ (Base‘𝑅))
72	64, 65	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼)))
73	25, 72	gsumsn 19935	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
74	58, 60, 71, 73	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
75	74, 71	eqeltrd 2834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅))
76		difssd 4112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁)
77	32, 76	ssfid 9273	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin)
78		eldifi 4106	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁)
79		mdetrlin.x	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
80	15, 24, 16	matbas2i 22360	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
81		elmapi 8863	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
82	79, 80, 81	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
83	82	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
84	83, 37, 41	fovcdmd 7579	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅))
85	78, 84	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅))
86	85	ralrimiva 3132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑋(𝑝‘𝑟)) ∈ (Base‘𝑅))
87	25, 31, 77, 86	gsummptcl 19948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) ∈ (Base‘𝑅))
88	24, 53, 54	ringdir 20222	. . . . . . . . . 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 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))))
90	23, 54	mgpplusg 20104	. . . . . . . . . . 11 ⊢ (.r‘𝑅) = (+g‘(mulGrp‘𝑅))
91		disjdif 4447	. . . . . . . . . . . 12 ⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅
92	91	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅)
93	59	snssd 4785	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐼} ⊆ 𝑁)
94	93	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁)
95		undif 4457	. . . . . . . . . . . . 13 ⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
96	94, 95	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
97	96	eqcomd 2741	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼})))
98	25, 90, 31, 32, 84, 92, 97	gsummptfidmsplit 19911	. . . . . . . . . 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 7422	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)))
102		xpss1 5673	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
103	94, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
104	61, 103	fssresd 6745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅))
105	104	ffnd 6707	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
106	70, 103	fssresd 6745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅))
107	106	ffnd 6707	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
108		snex 5406	. . . . . . . . . . . . . . . . 17 ⊢ {𝐼} ∈ V
109		xpexg 7744	. . . . . . . . . . . . . . . . 17 ⊢ (({𝐼} ∈ V ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ V)
110	108, 32, 109	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ V)
111		snidg 4636	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼})
112	60, 111	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼})
113	112, 62	opelxpd 5693	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁))
114		fnfvof 7688	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁) ∧ (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) ∧ (({𝐼} × 𝑁) ∈ V ∧ ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
115	105, 107, 110, 113, 114	syl22anc 838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
116		df-ov 7408	. . . . . . . . . . . . . . 15 ⊢ (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩)
117		df-ov 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)
118		df-ov 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)
119	117, 118	oveq12i 7417	. . . . . . . . . . . . . . 15 ⊢ ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩))
120	115, 116, 119	3eqtr4g 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
121	101, 120	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
122		ovres 7573	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
123	112, 62, 122	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
124		ovres 7573	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑌(𝑝‘𝐼)))
125	112, 62, 124	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑌(𝑝‘𝐼)))
126		ovres 7573	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
127	112, 62, 126	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
128	125, 127	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼))))
129	121, 123, 128	3eqtr3d 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼))))
130	82	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
131	130, 60, 62	fovcdmd 7579	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ (Base‘𝑅))
132	64, 65	oveq12d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼)))
133	25, 132	gsumsn 19935	. . . . . . . . . . . . 13 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
134	58, 60, 131, 133	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
135	68, 74	oveq12d 7423	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑌(𝑝‘𝐼)) + (𝐼𝑍(𝑝‘𝐼))))
136	129, 134, 135	3eqtr4d 2780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))))
137	136	oveq1d 7420	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
138	98, 137	eqtrd 2770	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
139	25, 90, 31, 32, 42, 92, 97	gsummptfidmsplit 19911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))))))
140		mdetrlin.ne1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
141	140	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
142	141	oveqd 7422	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
143		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼}))
144	78, 41	sylan2 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁)
145		ovres 7573	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
146	143, 144, 145	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
147		ovres 7573	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑌(𝑝‘𝑟)))
148	143, 144, 147	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑌(𝑝‘𝑟)))
149	142, 146, 148	3eqtr3rd 2779	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑌(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
150	149	mpteq2dva 5214	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))
151	150	oveq2d 7421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))
152	151	oveq2d 7421	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝‘𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
153	139, 152	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
154	25, 90, 31, 32, 50, 92, 97	gsummptfidmsplit 19911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
155		mdetrlin.ne2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
156	155	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
157	156	oveqd 7422	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
158		ovres 7573	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
159	143, 144, 158	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
160	157, 146, 159	3eqtr3rd 2779	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
161	160	mpteq2dva 5214	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))
162	161	oveq2d 7421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))
163	162	oveq2d 7421	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
164	154, 163	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
165	153, 164	oveq12d 7423	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟))))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))))))
166	89, 138, 165	3eqtr4rd 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))
167	166	oveq2d 7421	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)(((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))
168	56, 167	eqtr3d 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))
169	168	mpteq2dva 5214	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))))
170	9, 169	eqtrid 2782	. . . 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 7421	. . 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 20242	. . . . 5 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
173	10, 11, 172	3syl 18	. . . 4 ⊢ (𝜑 → 𝑅 ∈ CMnd)
174	38, 22	symgbasfi 19360	. . . . 5 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
175	19, 174	syl 17	. . . 4 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
176	24, 54	ringcl 20210	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ (Base‘𝑅))
177	13, 28, 44, 176	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))) ∈ (Base‘𝑅))
178	24, 54	ringcl 20210	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ (Base‘𝑅))
179	13, 28, 52, 178	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ (Base‘𝑅))
180	24, 53, 173, 175, 177, 179, 3, 6	gsummptfidmadd2 19907	. . 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 2772	. 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 2735	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
184		eqid 2735	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
185	182, 15, 16, 22, 183, 184, 54, 23	mdetleib2 22526	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
186	10, 79, 185	syl2anc 584	. 2 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
187	182, 15, 16, 22, 183, 184, 54, 23	mdetleib2 22526	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑌 ∈ 𝐵) → (𝐷‘𝑌) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))))
188	10, 14, 187	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐷‘𝑌) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))))
189	182, 15, 16, 22, 183, 184, 54, 23	mdetleib2 22526	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
190	10, 45, 189	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
191	188, 190	oveq12d 7423	. 2 ⊢ (𝜑 → ((𝐷‘𝑌) + (𝐷‘𝑍)) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑌(𝑝‘𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
192	181, 186, 191	3eqtr4d 2780	1 ⊢ (𝜑 → (𝐷‘𝑋) = ((𝐷‘𝑌) + (𝐷‘𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925   ⊆ wss 3926  ∅c0 4308  {csn 4601  ⟨cop 4607   ↦ cmpt 5201   × cxp 5652   ↾ cres 5656   ∘ ccom 5658   Fn wfn 6526  ⟶wf 6527  ‘cfv 6531  (class class class)co 7405   ∘_f cof 7669   ↑_m cmap 8840  Fincfn 8959  Basecbs 17228  +_gcplusg 17271  ._rcmulr 17272   Σ_g cgsu 17454  Mndcmnd 18712   MndHom cmhm 18759  SymGrpcsymg 19350  pmSgncpsgn 19470  CMndccmn 19761  mulGrpcmgp 20100  Ringcrg 20193  CRingccrg 20194  ℤRHomczrh 21460   Mat cmat 22345   maDet cmdat 22522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206  ax-addf 11208  ax-mulf 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-ot 4610  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7671  df-om 7862  df-1st 7988  df-2nd 7989  df-supp 8160  df-tpos 8225  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8719  df-map 8842  df-pm 8843  df-ixp 8912  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fsupp 9374  df-sup 9454  df-oi 9524  df-card 9953  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310  df-n0 12502  df-xnn0 12575  df-z 12589  df-dec 12709  df-uz 12853  df-rp 13009  df-fz 13525  df-fzo 13672  df-seq 14020  df-exp 14080  df-hash 14349  df-word 14532  df-lsw 14581  df-concat 14589  df-s1 14614  df-substr 14659  df-pfx 14689  df-splice 14768  df-reverse 14777  df-s2 14867  df-struct 17166  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17252  df-plusg 17284  df-mulr 17285  df-starv 17286  df-sca 17287  df-vsca 17288  df-ip 17289  df-tset 17290  df-ple 17291  df-ds 17293  df-unif 17294  df-hom 17295  df-cco 17296  df-0g 17455  df-gsum 17456  df-prds 17461  df-pws 17463  df-mre 17598  df-mrc 17599  df-acs 17601  df-mgm 18618  df-sgrp 18697  df-mnd 18713  df-mhm 18761  df-submnd 18762  df-efmnd 18847  df-grp 18919  df-minusg 18920  df-mulg 19051  df-subg 19106  df-ghm 19196  df-gim 19242  df-cntz 19300  df-oppg 19329  df-symg 19351  df-pmtr 19423  df-psgn 19472  df-cmn 19763  df-abl 19764  df-mgp 20101  df-rng 20113  df-ur 20142  df-ring 20195  df-cring 20196  df-oppr 20297  df-dvdsr 20317  df-unit 20318  df-invr 20348  df-dvr 20361  df-rhm 20432  df-subrng 20506  df-subrg 20530  df-drng 20691  df-sra 21131  df-rgmod 21132  df-cnfld 21316  df-zring 21408  df-zrh 21464  df-dsmm 21692  df-frlm 21707  df-mat 22346  df-mdet 22523

This theorem is referenced by:  mdetrlin2  22545  mdetuni0  22559  mdetmul  22561