Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 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 fnssres ⊢ ( ( 𝑍 Fn ( 𝑁 × 𝑁 ) ∧ ( { 𝐼 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) ) → ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) Fn ( { 𝐼 } × 𝑁 ) )
45 40 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) Fn ( { 𝐼 } × 𝑁 ) )
46 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ∈ ( { 𝐼 } × 𝑁 ) ) → ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) = ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) )
47 34 35 45 46 ofc1 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ∈ ( { 𝐼 } × 𝑁 ) ) → ( ( ( ( { 𝐼 } × 𝑁 ) × { 𝑌 } ) ∘f · ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) = ( 𝑌 · ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) ) )
48 27 47 mpdan ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( { 𝐼 } × 𝑁 ) × { 𝑌 } ) ∘f · ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) = ( 𝑌 · ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) ) )
49 df-ov ⊢ ( 𝐼 ( ( ( { 𝐼 } × 𝑁 ) × { 𝑌 } ) ∘f · ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( ( ( { 𝐼 } × 𝑁 ) × { 𝑌 } ) ∘f · ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ )
50 df-ov ⊢ ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ )
51 50 oveq2i ⊢ ( 𝑌 · ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) = ( 𝑌 · ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) )
52 48 49 51 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( ( ( { 𝐼 } × 𝑁 ) × { 𝑌 } ) ∘f · ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝑌 · ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) )
53 14 26 52 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) = ( 𝑌 · ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) )
54 ovres ⊢ ( ( 𝐼 ∈ { 𝐼 } ∧ ( 𝑝 ‘ 𝐼 ) ∈ 𝑁 ) → ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
55 17 24 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
56 55 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑌 · ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) = ( 𝑌 · ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) )
57 53 56 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) = ( 𝑌 · ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) )
58 57 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( 𝑌 · ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
59 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
60 6 59 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
62 39 15 24 fovrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ∈ 𝐾 )
63 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
64 63 4 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
65 63 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
66 6 65 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
68 difssd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁 )
69 32 68 ssfid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
70 eldifi ⊢ ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑟 ∈ 𝑁 )
71 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
72 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑟 ∈ 𝑁 )
73 23 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 )
74 71 72 73 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ∈ 𝐾 )
75 70 74 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ∈ 𝐾 )
76 75 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ∈ 𝐾 )
77 64 67 69 76 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ 𝐾 )
78 4 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ∈ 𝐾 ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ 𝐾 ) ) → ( ( 𝑌 · ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
79 61 35 62 77 78 syl13anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝑌 · ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
80 58 79 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
81 63 5 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
82 2 4 3 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
83 elmapi ⊢ ( 𝑋 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
84 7 82 83 3syl ⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
85 84 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
86 85 72 73 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ∈ 𝐾 )
87 disjdif ⊢ ( { 𝐼 } ∩ ( 𝑁 ∖ { 𝐼 } ) ) = ∅
88 87 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( { 𝐼 } ∩ ( 𝑁 ∖ { 𝐼 } ) ) = ∅ )
89 undif ⊢ ( { 𝐼 } ⊆ 𝑁 ↔ ( { 𝐼 } ∪ ( 𝑁 ∖ { 𝐼 } ) ) = 𝑁 )
90 41 89 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( { 𝐼 } ∪ ( 𝑁 ∖ { 𝐼 } ) ) = 𝑁 )
91 90 eqcomd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑁 = ( { 𝐼 } ∪ ( 𝑁 ∖ { 𝐼 } ) ) )
92 64 81 67 32 86 88 91 gsummptfidmsplit ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
93 cmnmnd ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ CMnd → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
94 67 93 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
95 84 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
96 95 15 24 fovrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) ∈ 𝐾 )
97 id ⊢ ( 𝑟 = 𝐼 → 𝑟 = 𝐼 )
98 fveq2 ⊢ ( 𝑟 = 𝐼 → ( 𝑝 ‘ 𝑟 ) = ( 𝑝 ‘ 𝐼 ) )
99 97 98 oveq12d ⊢ ( 𝑟 = 𝐼 → ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
100 64 99 gsumsn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) ∈ 𝐾 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
101 94 15 96 100 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
102 12 oveqd ⊢ ( 𝜑 → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) )
103 102 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) )
104 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) )
105 70 73 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 )
106 ovres ⊢ ( ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) )
107 104 105 106 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) )
108 ovres ⊢ ( ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 ) → ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) )
109 104 105 108 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) )
110 103 107 109 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) )
111 110 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) = ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) )
112 111 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) )
113 101 112 oveq12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
114 92 113 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
115 64 81 67 32 74 88 91 gsummptfidmsplit ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
116 97 98 oveq12d ⊢ ( 𝑟 = 𝐼 → ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
117 64 116 gsumsn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ∈ 𝐾 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
118 94 15 62 117 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
119 118 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
120 115 119 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
121 120 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑌 · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
122 80 114 121 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝑌 · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
123 122 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( 𝑌 · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
124 6 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ CRing )
125 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
126 60 31 125 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
127 19 64 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
128 126 127 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
129 128 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 )
130 4 5 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · 𝑌 ) = ( 𝑌 · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ) )
131 124 129 35 130 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · 𝑌 ) = ( 𝑌 · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ) )
132 131 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · 𝑌 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( 𝑌 · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
133 74 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑟 ∈ 𝑁 ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ∈ 𝐾 )
134 64 67 32 133 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ 𝐾 )
135 4 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ 𝐾 ) ) → ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · 𝑌 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( 𝑌 · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
136 61 129 35 134 135 syl13anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · 𝑌 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( 𝑌 · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
137 4 5 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ 𝐾 ) ) → ( ( 𝑌 · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
138 61 35 129 134 137 syl13anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝑌 · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
139 132 136 138 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( 𝑌 · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
140 123 139 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
141 140 mpteq2dva ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
142 141 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
143 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
144 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
145 18 19 symgbasfi ⊢ ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
146 31 145 syl ⊢ ( 𝜑 → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
147 4 5 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ 𝐾 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ 𝐾 )
148 61 129 134 147 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ 𝐾 )
149 eqid ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
150 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ V )
151 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
152 149 146 150 151 fsuppmptdm ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
153 4 143 144 5 60 146 8 148 152 gsummulc2 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( 𝑌 · ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
154 142 153 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
155 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
156 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
157 1 2 3 19 155 156 5 63 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
158 6 7 157 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
159 1 2 3 19 155 156 5 63 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑍 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
160 6 9 159 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑍 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
161 160 oveq2d ⊢ ( 𝜑 → ( 𝑌 · ( 𝐷 ‘ 𝑍 ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
162 154 158 161 3eqtr4d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝑌 · ( 𝐷 ‘ 𝑍 ) ) )