mdetrsca - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mdetrsca		Structured version Visualization version GIF version

Theorem mdetrsca 22584

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 7381	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)))
3	2	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)))
4		mdetrsca.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
5	4	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ 𝑁)
6		snidg 4605	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ 𝑁 → 𝐼 ∈ {𝐼})
7	5, 6	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼})
8		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
9		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
10	8, 9	symgbasf1o 19347	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁–1-1-onto→𝑁)
11	10	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁–1-1-onto→𝑁)
12		f1of 6778	. . . . . . . . . . . . . . 15 ⊢ (𝑝:𝑁–1-1-onto→𝑁 → 𝑝:𝑁⟶𝑁)
13	11, 12	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
14	13, 5	ffvelcdmd 7035	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝‘𝐼) ∈ 𝑁)
15		ovres 7530	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
16	7, 14, 15	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑋(𝑝‘𝐼)))
17	7, 14	opelxpd 5667	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁))
18		snfi 8987	. . . . . . . . . . . . . . . 16 ⊢ {𝐼} ∈ Fin
19		mdetrsca.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
20		mdetrsca.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐴 = (𝑁 Mat 𝑅)
21		mdetrsca.b	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐵 = (Base‘𝐴)
22	20, 21	matrcl 22393	. . . . . . . . . . . . . . . . . . 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 9227	. . . . . . . . . . . . . . . 16 ⊢ (({𝐼} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ Fin)
27	18, 25, 26	sylancr 588	. . . . . . . . . . . . . . 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 22403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ 𝐵 → 𝑍 ∈ (𝐾 ↑_m (𝑁 × 𝑁)))
33		elmapi 8793	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ (𝐾 ↑_m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
34	30, 32, 33	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶𝐾)
35	34	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
36	35	ffnd 6667	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍 Fn (𝑁 × 𝑁))
37	5	snssd 4753	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁)
38		xpss1 5647	. . . . . . . . . . . . . . . . 17 ⊢ ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
40	36, 39	fnssresd 6620	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
41		eqidd 2738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁)) → ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩))
42	27, 29, 40, 41	ofc1 7656	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ ⟨𝐼, (𝑝‘𝐼)⟩ ∈ ({𝐼} × 𝑁)) → (((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
43	17, 42	mpdan 688	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)))
44		df-ov 7367	. . . . . . . . . . . . 13 ⊢ (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝‘𝐼)⟩)
45		df-ov 7367	. . . . . . . . . . . . . 14 ⊢ (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩)
46	45	oveq2i 7375	. . . . . . . . . . . . 13 ⊢ (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝‘𝐼)⟩))
47	43, 44, 46	3eqtr4g 2797	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((({𝐼} × 𝑁) × {𝑌}) ∘_f · (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
48	3, 16, 47	3eqtr3d 2780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))))
49		ovres 7530	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ {𝐼} ∧ (𝑝‘𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
50	7, 14, 49	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼)) = (𝐼𝑍(𝑝‘𝐼)))
51	50	oveq2d 7380	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝‘𝐼))) = (𝑌 · (𝐼𝑍(𝑝‘𝐼))))
52	48, 51	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) = (𝑌 · (𝐼𝑍(𝑝‘𝐼))))
53	52	oveq1d 7379	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
54		mdetrsca.r	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ CRing)
55	54	crngringd 20224	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Ring)
56	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
57	35, 5, 14	fovcdmd 7536	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾)
58		eqid 2737	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
59	58, 31	mgpbas 20123	. . . . . . . . . . 11 ⊢ 𝐾 = (Base‘(mulGrp‘𝑅))
60	58	crngmgp 20219	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
61	54, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
62	61	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
63		difssd 4078	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁)
64	25, 63	ssfid 9176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin)
65		eldifi 4072	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟 ∈ 𝑁)
66	34	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐾)
67		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑟 ∈ 𝑁)
68	13	ffvelcdmda 7034	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑝‘𝑟) ∈ 𝑁)
69	66, 67, 68	fovcdmd 7536	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
70	65, 69	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
71	70	ralrimiva 3130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
72	59, 62, 64, 71	gsummptcl 19939	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)
73		mdetrsca.t	. . . . . . . . . . 11 ⊢ · = (._r‘𝑅)
74	31, 73	ringass 20231	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
75	56, 29, 57, 72, 74	syl13anc 1375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (𝐼𝑍(𝑝‘𝐼))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
76	53, 75	eqtrd 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
77	58, 73	mgpplusg 20122	. . . . . . . . . 10 ⊢ · = (+_g‘(mulGrp‘𝑅))
78	20, 31, 21	matbas2i 22403	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (𝐾 ↑_m (𝑁 × 𝑁)))
79		elmapi 8793	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ (𝐾 ↑_m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
80	19, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶𝐾)
81	80	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
82	81, 67, 68	fovcdmd 7536	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ 𝑁) → (𝑟𝑋(𝑝‘𝑟)) ∈ 𝐾)
83		disjdif 4413	. . . . . . . . . . 11 ⊢ ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅
84	83	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅)
85		undif 4423	. . . . . . . . . . . 12 ⊢ ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
86	37, 85	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
87	86	eqcomd 2743	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼})))
88	59, 77, 62, 25, 82, 84, 87	gsummptfidmsplit 19902	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))))
89	62	cmnmndd 19776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd)
90	80	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶𝐾)
91	90, 5, 14	fovcdmd 7536	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾)
92		id 22	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → 𝑟 = 𝐼)
93		fveq2 6838	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑝‘𝑟) = (𝑝‘𝐼))
94	92, 93	oveq12d 7382	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐼 → (𝑟𝑋(𝑝‘𝑟)) = (𝐼𝑋(𝑝‘𝐼)))
95	59, 94	gsumsn 19926	. . . . . . . . . . 11 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑋(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
96	89, 5, 91, 95	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝐼𝑋(𝑝‘𝐼)))
97		mdetrsca.ne	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
98	97	oveqd 7381	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
99	98	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)))
100		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼}))
101	65, 68	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝‘𝑟) ∈ 𝑁)
102		ovres 7530	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
103	100, 101, 102	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑋(𝑝‘𝑟)))
104		ovres 7530	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝‘𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
105	100, 101, 104	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
106	99, 103, 105	3eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝‘𝑟)) = (𝑟𝑍(𝑝‘𝑟)))
107	106	mpteq2dva 5179	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))
108	107	oveq2d 7380	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))
109	96, 108	oveq12d 7382	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
110	88, 109	eqtrd 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = ((𝐼𝑋(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
111	59, 77, 62, 25, 69, 84, 87	gsummptfidmsplit 19902	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = (((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
112	92, 93	oveq12d 7382	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐼 → (𝑟𝑍(𝑝‘𝑟)) = (𝐼𝑍(𝑝‘𝐼)))
113	59, 112	gsumsn 19926	. . . . . . . . . . . 12 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ (𝐼𝑍(𝑝‘𝐼)) ∈ 𝐾) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
114	89, 5, 57, 113	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) = (𝐼𝑍(𝑝‘𝐼)))
115	114	oveq1d 7379	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σ_g (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝‘𝑟)))) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
116	111, 115	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) = ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟))))))
117	116	oveq2d 7380	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((𝐼𝑍(𝑝‘𝐼)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝‘𝑟)))))))
118	76, 110, 117	3eqtr4d 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))) = (𝑌 · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
119	118	oveq2d 7380	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
120	54	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ CRing)
121		zrhpsgnmhm 21580	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
122	55, 24, 121	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
123	9, 59	mhmf 18754	. . . . . . . . . . 11 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
124	122, 123	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
125	124	ffvelcdmda 7034	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾)
126	31, 73	crngcom 20229	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)))
127	120, 125, 29, 126	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) = (𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)))
128	127	oveq1d 7379	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
129	69	ralrimiva 3130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ 𝑁 (𝑟𝑍(𝑝‘𝑟)) ∈ 𝐾)
130	59, 62, 25, 129	gsummptcl 19939	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)
131	31, 73	ringass 20231	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
132	56, 125, 29, 130, 131	syl13anc 1375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · 𝑌) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
133	31, 73	ringass 20231	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))) ∈ 𝐾)) → ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
134	56, 29, 125, 130, 133	syl13anc 1375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝑌 · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
135	128, 132, 134	3eqtr3d 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · (𝑌 · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
136	119, 135	eqtrd 2772	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))) = (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))
137	136	mpteq2dva 5179	. . . 4 ⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
138	137	oveq2d 7380	. . 3 ⊢ (𝜑 → (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
139		eqid 2737	. . . 4 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
140	8, 9	symgbasfi 19351	. . . . 5 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
141	24, 140	syl 17	. . . 4 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
142	31, 73, 56, 125, 130	ringcld 20238	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ 𝐾)
143		eqid 2737	. . . . 5 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))
144		ovexd 7399	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))) ∈ V)
145		fvexd 6853	. . . . 5 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
146	143, 141, 144, 145	fsuppmptdm 9286	. . . 4 ⊢ (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))) finSupp (0_g‘𝑅))
147	31, 139, 73, 55, 141, 28, 142, 146	gsummulc2 20293	. . 3 ⊢ (𝜑 → (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (𝑌 · ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))) = (𝑌 · (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
148	138, 147	eqtrd 2772	. 2 ⊢ (𝜑 → (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))) = (𝑌 · (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
149		mdetrsca.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
150		eqid 2737	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
151		eqid 2737	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
152	149, 20, 21, 9, 150, 151, 73, 58	mdetleib2 22569	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐷‘𝑋) = (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
153	54, 19, 152	syl2anc 585	. 2 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑋(𝑝‘𝑟))))))))
154	149, 20, 21, 9, 150, 151, 73, 58	mdetleib2 22569	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵) → (𝐷‘𝑍) = (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
155	54, 30, 154	syl2anc 585	. . 3 ⊢ (𝜑 → (𝐷‘𝑍) = (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟))))))))
156	155	oveq2d 7380	. 2 ⊢ (𝜑 → (𝑌 · (𝐷‘𝑍)) = (𝑌 · (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) · ((mulGrp‘𝑅) Σ_g (𝑟 ∈ 𝑁 ↦ (𝑟𝑍(𝑝‘𝑟)))))))))
157	148, 153, 156	3eqtr4d 2782	1 ⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍)))

Colors of variables: wff setvar class

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 5626 ↾ cres 5630 ∘ ccom 5632 ⟶wf 6492 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7364 ∘_f cof 7626 ↑_m cmap 8770 Fincfn 8890 Basecbs 17176 ._rcmulr 17218 0_gc0g 17399 Σ_g cgsu 17400 Mndcmnd 18699 MndHom cmhm 18746 SymGrpcsymg 19341 pmSgncpsgn 19461 CMndccmn 19752 mulGrpcmgp 20118 Ringcrg 20211 CRingccrg 20212 ℤRHomczrh 21495 Mat cmat 22388 maDet cmdat 22565

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 5306 ax-pr 5374 ax-un 7686 ax-cnex 11091 ax-resscn 11092 ax-1cn 11093 ax-icn 11094 ax-addcl 11095 ax-addrcl 11096 ax-mulcl 11097 ax-mulrcl 11098 ax-mulcom 11099 ax-addass 11100 ax-mulass 11101 ax-distr 11102 ax-i2m1 11103 ax-1ne0 11104 ax-1rid 11105 ax-rnegex 11106 ax-rrecex 11107 ax-cnre 11108 ax-pre-lttri 11109 ax-pre-lttrn 11110 ax-pre-ltadd 11111 ax-pre-mulgt0 11112 ax-addf 11114 ax-mulf 11115

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 5523 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5581 df-se 5582 df-we 5583 df-xp 5634 df-rel 5635 df-cnv 5636 df-co 5637 df-dm 5638 df-rn 5639 df-res 5640 df-ima 5641 df-pred 6263 df-ord 6324 df-on 6325 df-lim 6326 df-suc 6327 df-iota 6452 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7321 df-ov 7367 df-oprab 7368 df-mpo 7369 df-of 7628 df-om 7815 df-1st 7939 df-2nd 7940 df-supp 8108 df-tpos 8173 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-sup 9352 df-oi 9422 df-card 9860 df-pnf 11178 df-mnf 11179 df-xr 11180 df-ltxr 11181 df-le 11182 df-sub 11376 df-neg 11377 df-div 11805 df-nn 12172 df-2 12241 df-3 12242 df-4 12243 df-5 12244 df-6 12245 df-7 12246 df-8 12247 df-9 12248 df-n0 12435 df-xnn0 12508 df-z 12522 df-dec 12642 df-uz 12786 df-rp 12940 df-fz 13459 df-fzo 13606 df-seq 13961 df-exp 14021 df-hash 14290 df-word 14473 df-lsw 14522 df-concat 14530 df-s1 14556 df-substr 14601 df-pfx 14631 df-splice 14709 df-reverse 14718 df-s2 14807 df-struct 17114 df-sets 17131 df-slot 17149 df-ndx 17161 df-base 17177 df-ress 17198 df-plusg 17230 df-mulr 17231 df-starv 17232 df-sca 17233 df-vsca 17234 df-ip 17235 df-tset 17236 df-ple 17237 df-ds 17239 df-unif 17240 df-hom 17241 df-cco 17242 df-0g 17401 df-gsum 17402 df-prds 17407 df-pws 17409 df-mre 17545 df-mrc 17546 df-acs 17548 df-mgm 18605 df-sgrp 18684 df-mnd 18700 df-mhm 18748 df-submnd 18749 df-efmnd 18834 df-grp 18909 df-minusg 18910 df-mulg 19041 df-subg 19096 df-ghm 19185 df-gim 19231 df-cntz 19289 df-oppg 19318 df-symg 19342 df-pmtr 19414 df-psgn 19463 df-cmn 19754 df-abl 19755 df-mgp 20119 df-rng 20131 df-ur 20160 df-ring 20213 df-cring 20214 df-oppr 20314 df-dvdsr 20334 df-unit 20335 df-invr 20365 df-dvr 20378 df-rhm 20449 df-subrng 20520 df-subrg 20544 df-drng 20705 df-sra 21166 df-rgmod 21167 df-cnfld 21351 df-zring 21443 df-zrh 21499 df-dsmm 21728 df-frlm 21743 df-mat 22389 df-mdet 22566

This theorem is referenced by: mdetrsca2 22585 mdetuni0 22602 mdetmul 22604 smadiadetg 22654

W3C validator