This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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