Theorem mdetrsca

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

	Ref	Expression
Hypotheses	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	mdetrsca	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝑌 · ( 𝐷 ‘ 𝑍 ) ) )

Proof

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