Theorem mdetrsca 22497

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

Hypotheses

Ref	Expression
mdetrsca.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetrsca.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetrsca.b	⊢ 𝐵 = (Base‘𝐴)
mdetrsca.k	⊢ 𝐾 = (Base‘𝑅)
mdetrsca.t	⊢ · = (.r‘𝑅)
mdetrsca.r	⊢ (𝜑 → 𝑅 ∈ CRing)
mdetrsca.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
mdetrsca.y	⊢ (𝜑 → 𝑌 ∈ 𝐾)
mdetrsca.z	⊢ (𝜑 → 𝑍 ∈ 𝐵)
mdetrsca.i	⊢ (𝜑 → 𝐼 ∈ 𝑁)
mdetrsca.eq	⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁))))
mdetrsca.ne	⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))

Assertion

Ref	Expression
mdetrsca	⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍)))

Proof of Theorem mdetrsca

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

Step	Hyp	Ref	Expression
1		mdetrsca.eq	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁))))
2	1	oveqd 7407	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)))
3	2	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)))
4		mdetrsca.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
5	4	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ 𝑁)
6		snidg 4627	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼})
7	5, 6	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼})
8		eqid 2730	. . . . . . . . . . . . . . . . 17 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
9		eqid 2730	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
10	8, 9	symgbasf1o 19312	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁)
11	10	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁)
12		f1of 6803	. . . . . . . . . . . . . . 15 ⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁)
13	11, 12	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
14	13, 5	ffvelcdmd 7060	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁)
15		ovres 7558	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
16	7, 14, 15	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
17	7, 14	opelxpd 5680	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁))
18		snfi 9017	. . . . . . . . . . . . . . . 16 ⊢ {𝐼} ∈ Fin
19		mdetrsca.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
20		mdetrsca.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐴 = (𝑁 Mat 𝑅)
21		mdetrsca.b	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐵 = (Base‘𝐴)
22	20, 21	matrcl 22306	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
23	19, 22	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
24	23	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ Fin)
25	24	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
26		xpfi 9276	. . . . . . . . . . . . . . . 16 ⊢ (({𝐼} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ Fin)
27	18, 25, 26	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ Fin)
28		mdetrsca.y	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
29	28	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌 ∈ 𝐾)
30		mdetrsca.z	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
31		mdetrsca.k	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐾 = (Base‘𝑅)
32	20, 31, 21	matbas2i 22316	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
33		elmapi 8825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
34	30, 32, 33	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶𝐾)
35	34	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
36	35	ffnd 6692	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍 Fn (𝑁 × 𝑁))
37	5	snssd 4776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁)
38		xpss1 5660	. . . . . . . . . . . . . . . . 17 ⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
40	36, 39	fnssresd 6645	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
41		eqidd 2731	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁)) → ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩))
42	27, 29, 40, 41	ofc1 7684	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁)) → (((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
43	17, 42	mpdan 687	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
44		df-ov 7393	. . . . . . . . . . . . 13 ⊢ (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩)
45		df-ov 7393	. . . . . . . . . . . . . 14 ⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)
46	45	oveq2i 7401	. . . . . . . . . . . . 13 ⊢ (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩))
47	43, 44, 46	3eqtr4g 2790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
48	3, 16, 47	3eqtr3d 2773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
49		ovres 7558	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
50	7, 14, 49	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
51	50	oveq2d 7406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · (𝐼𝑍(𝑝‘𝐼))))
52	48, 51	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼𝑍(𝑝‘𝐼))))
53	52	oveq1d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
54		mdetrsca.r	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ CRing)
55	54	crngringd 20162	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Ring)
56	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
57	35, 5, 14	fovcdmd 7564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾)
58		eqid 2730	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
59	58, 31	mgpbas 20061	. . . . . . . . . . 11 ⊢ 𝐾 = (Base‘(mulGrp‘𝑅))
60	58	crngmgp 20157	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
61	54, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
62	61	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
63		difssd 4103	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁)
64	25, 63	ssfid 9219	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin)
65		eldifi 4097	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁)
66	34	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
67		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁)
68	13	ffvelcdmda 7059	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁)
69	66, 67, 68	fovcdmd 7564	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
70	65, 69	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
71	70	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
72	59, 62, 64, 71	gsummptcl 19904	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)
73		mdetrsca.t	. . . . . . . . . . 11 ⊢ · = (.r‘𝑅)
74	31, 73	ringass 20169	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
75	56, 29, 57, 72, 74	syl13anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
76	53, 75	eqtrd 2765	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
77	58, 73	mgpplusg 20060	. . . . . . . . . 10 ⊢ · = (+g‘(mulGrp‘𝑅))
78	20, 31, 21	matbas2i 22316	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
79		elmapi 8825	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
80	19, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶𝐾)
81	80	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
82	81, 67, 68	fovcdmd 7564	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ 𝐾)
83		disjdif 4438	. . . . . . . . . . 11 ⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅
84	83	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅)
85		undif 4448	. . . . . . . . . . . 12 ⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
86	37, 85	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
87	86	eqcomd 2736	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼})))
88	59, 77, 62, 25, 82, 84, 87	gsummptfidmsplit 19867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
89	62	cmnmndd 19741	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd)
90	80	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
91	90, 5, 14	fovcdmd 7564	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾)
92		id 22	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼)
93		fveq2 6861	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼))
94	92, 93	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼)))
95	59, 94	gsumsn 19891	. . . . . . . . . . 11 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
96	89, 5, 91, 95	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
97		mdetrsca.ne	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
98	97	oveqd 7407	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
99	98	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
100		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼}))
101	65, 68	sylan2 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁)
102		ovres 7558	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
103	100, 101, 102	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
104		ovres 7558	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
105	100, 101, 104	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
106	99, 103, 105	3eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
107	106	mpteq2dva 5203	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))
108	107	oveq2d 7406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))
109	96, 108	oveq12d 7408	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
110	88, 109	eqtrd 2765	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
111	59, 77, 62, 25, 69, 84, 87	gsummptfidmsplit 19867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
112	92, 93	oveq12d 7408	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼)))
113	59, 112	gsumsn 19891	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
114	89, 5, 57, 113	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
115	114	oveq1d 7405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
116	111, 115	eqtrd 2765	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
117	116	oveq2d 7406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
118	76, 110, 117	3eqtr4d 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝑌 · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
119	118	oveq2d 7406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
120	54	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ CRing)
121		zrhpsgnmhm 21500	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
122	55, 24, 121	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
123	9, 59	mhmf 18723	. . . . . . . . . . 11 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
124	122, 123	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
125	124	ffvelcdmda 7059	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾)
126	31, 73	crngcom 20167	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)))
127	120, 125, 29, 126	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)))
128	127	oveq1d 7405	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
129	69	ralrimiva 3126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
130	59, 62, 25, 129	gsummptcl 19904	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)
131	31, 73	ringass 20169	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
132	56, 125, 29, 130, 131	syl13anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
133	31, 73	ringass 20169	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
134	56, 29, 125, 130, 133	syl13anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
135	128, 132, 134	3eqtr3d 2773	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
136	119, 135	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
137	136	mpteq2dva 5203	. . . 4 ⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
138	137	oveq2d 7406	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
139		eqid 2730	. . . 4 ⊢ (0g‘𝑅) = (0g‘𝑅)
140	8, 9	symgbasfi 19316	. . . . 5 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
141	24, 140	syl 17	. . . 4 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
142	31, 73, 56, 125, 130	ringcld 20176	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ 𝐾)
143		eqid 2730	. . . . 5 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
144		ovexd 7425	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V)
145		fvexd 6876	. . . . 5 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
146	143, 141, 144, 145	fsuppmptdm 9334	. . . 4 ⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) finSupp (0g‘𝑅))
147	31, 139, 73, 55, 141, 28, 142, 146	gsummulc2 20233	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
148	138, 147	eqtrd 2765	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑌 · (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
149		mdetrsca.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
150		eqid 2730	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
151		eqid 2730	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
152	149, 20, 21, 9, 150, 151, 73, 58	mdetleib2 22482	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
153	54, 19, 152	syl2anc 584	. 2 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
154	149, 20, 21, 9, 150, 151, 73, 58	mdetleib2 22482	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
155	54, 30, 154	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
156	155	oveq2d 7406	. 2 ⊢ (𝜑 → (𝑌 · (𝐷‘𝑍)) = (𝑌 · (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
157	148, 153, 156	3eqtr4d 2775	1 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  {csn 4592  ⟨cop 4598   ↦ cmpt 5191   × cxp 5639   ↾ cres 5643   ∘ ccom 5645  ⟶wf 6510  –1-1-onto→wf1o 6513  ‘cfv 6514  (class class class)co 7390   ∘_f cof 7654   ↑_m cmap 8802  Fincfn 8921  Basecbs 17186  ._rcmulr 17228  0_gc0g 17409   Σ_g cgsu 17410  Mndcmnd 18668   MndHom cmhm 18715  SymGrpcsymg 19306  pmSgncpsgn 19426  CMndccmn 19717  mulGrpcmgp 20056  Ringcrg 20149  CRingccrg 20150  ℤRHomczrh 21416   Mat cmat 22301   maDet cmdat 22478

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-addf 11154  ax-mulf 11155

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-ot 4601  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-om 7846  df-1st 7971  df-2nd 7972  df-supp 8143  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8674  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9320  df-sup 9400  df-oi 9470  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-xnn0 12523  df-z 12537  df-dec 12657  df-uz 12801  df-rp 12959  df-fz 13476  df-fzo 13623  df-seq 13974  df-exp 14034  df-hash 14303  df-word 14486  df-lsw 14535  df-concat 14543  df-s1 14568  df-substr 14613  df-pfx 14643  df-splice 14722  df-reverse 14731  df-s2 14821  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-0g 17411  df-gsum 17412  df-prds 17417  df-pws 17419  df-mre 17554  df-mrc 17555  df-acs 17557  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-mhm 18717  df-submnd 18718  df-efmnd 18803  df-grp 18875  df-minusg 18876  df-mulg 19007  df-subg 19062  df-ghm 19152  df-gim 19198  df-cntz 19256  df-oppg 19285  df-symg 19307  df-pmtr 19379  df-psgn 19428  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-ring 20151  df-cring 20152  df-oppr 20253  df-dvdsr 20273  df-unit 20274  df-invr 20304  df-dvr 20317  df-rhm 20388  df-subrng 20462  df-subrg 20486  df-drng 20647  df-sra 21087  df-rgmod 21088  df-cnfld 21272  df-zring 21364  df-zrh 21420  df-dsmm 21648  df-frlm 21663  df-mat 22302  df-mdet 22479

This theorem is referenced by:  mdetrsca2  22498  mdetuni0  22515  mdetmul  22517  smadiadetg  22567