Metamath Proof Explorer

Theorem mdetrlin

Description: The determinant function is additive for each row: The matrices X, Y, Z are identical except for the I's row, and the I's row of the matrix X is the componentwise sum of the I's row of the matrices Y and Z. In this case the determinant of X is the sum of the determinants of Y and Z. (Contributed by SO, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mdetrlin.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetrlin.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetrlin.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetrlin.p ⊢ + = ( +g ‘ 𝑅 )
mdetrlin.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mdetrlin.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mdetrlin.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
mdetrlin.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
mdetrlin.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
mdetrlin.eq ⊢ ( 𝜑 → ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) = ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) )
mdetrlin.ne1 ⊢ ( 𝜑 → ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑌 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
mdetrlin.ne2 ⊢ ( 𝜑 → ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
Assertion mdetrlin ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( ( 𝐷 ‘ 𝑌 ) + ( 𝐷 ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 mdetrlin.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetrlin.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 mdetrlin.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mdetrlin.p ⊢ + = ( +g ‘ 𝑅 )
5 mdetrlin.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 mdetrlin.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 mdetrlin.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 mdetrlin.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 mdetrlin.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
10 mdetrlin.eq ⊢ ( 𝜑 → ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) = ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) )
11 mdetrlin.ne1 ⊢ ( 𝜑 → ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑌 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
12 mdetrlin.ne2 ⊢ ( 𝜑 → ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
13 fvex ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ V
14 ovex ⊢ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ V
15 eqid ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
16 14 15 fnmpti ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) Fn ( Base ‘ ( SymGrp ‘ 𝑁 ) )
17 ovex ⊢ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ V
18 eqid ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
19 17 18 fnmpti ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) Fn ( Base ‘ ( SymGrp ‘ 𝑁 ) )
20 ofmpteq ⊢ ( ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ V ∧ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) Fn ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) Fn ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ∘f + ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
21 13 16 19 20 mp3an ⊢ ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ∘f + ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
22 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
23 5 22 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
25 2 3 matrcl ⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
26 7 25 syl ⊢ ( 𝜑 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
27 26 simpld ⊢ ( 𝜑 → 𝑁 ∈ Fin )
28 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
29 23 27 28 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
30 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
31 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
32 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33 31 32 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
34 30 33 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ 𝑅 ) )
35 29 34 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ 𝑅 ) )
36 35 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) )
37 31 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
38 5 37 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
40 27 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑁 ∈ Fin )
41 2 32 3 matbas2i ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
42 elmapi ⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑌 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
43 7 41 42 3syl ⊢ ( 𝜑 → 𝑌 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑌 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑟 ∈ 𝑁 )
46 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
47 46 30 symgbasf ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → 𝑝 : 𝑁 ⟶ 𝑁 )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑝 : 𝑁 ⟶ 𝑁 )
49 48 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 )
50 44 45 49 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
51 50 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑟 ∈ 𝑁 ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
52 33 39 40 51 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
53 2 32 3 matbas2i ⊢ ( 𝑍 ∈ 𝐵 → 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
54 elmapi ⊢ ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
55 8 53 54 3syl ⊢ ( 𝜑 → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
57 56 45 49 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
58 57 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑟 ∈ 𝑁 ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
59 33 39 40 58 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
60 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
61 32 4 60 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
62 24 36 52 59 61 syl13anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
63 cmnmnd ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ CMnd → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
64 39 63 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
65 9 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝐼 ∈ 𝑁 )
66 43 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑌 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
67 48 65 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑝 ‘ 𝐼 ) ∈ 𝑁 )
68 66 65 67 fovrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑅 ) )
69 id ⊢ ( 𝑟 = 𝐼 → 𝑟 = 𝐼 )
70 fveq2 ⊢ ( 𝑟 = 𝐼 → ( 𝑝 ‘ 𝑟 ) = ( 𝑝 ‘ 𝐼 ) )
71 69 70 oveq12d ⊢ ( 𝑟 = 𝐼 → ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) = ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) )
72 33 71 gsumsn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) )
73 64 65 68 72 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) )
74 73 68 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
75 55 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
76 75 65 67 fovrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑅 ) )
77 69 70 oveq12d ⊢ ( 𝑟 = 𝐼 → ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
78 33 77 gsumsn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
79 64 65 76 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
80 79 76 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
81 difssd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁 )
82 40 81 ssfid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
83 eldifi ⊢ ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑟 ∈ 𝑁 )
84 2 32 3 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
85 elmapi ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
86 6 84 85 3syl ⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
87 86 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
88 87 45 49 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
89 83 88 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
90 89 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ∈ ( Base ‘ 𝑅 ) )
91 33 39 82 90 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
92 32 4 60 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
93 24 74 80 91 92 syl13anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
94 31 60 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
95 disjdif ⊢ ( { 𝐼 } ∩ ( 𝑁 ∖ { 𝐼 } ) ) = ∅
96 95 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( { 𝐼 } ∩ ( 𝑁 ∖ { 𝐼 } ) ) = ∅ )
97 9 snssd ⊢ ( 𝜑 → { 𝐼 } ⊆ 𝑁 )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → { 𝐼 } ⊆ 𝑁 )
99 undif ⊢ ( { 𝐼 } ⊆ 𝑁 ↔ ( { 𝐼 } ∪ ( 𝑁 ∖ { 𝐼 } ) ) = 𝑁 )
100 98 99 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( { 𝐼 } ∪ ( 𝑁 ∖ { 𝐼 } ) ) = 𝑁 )
101 100 eqcomd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑁 = ( { 𝐼 } ∪ ( 𝑁 ∖ { 𝐼 } ) ) )
102 33 94 39 40 88 96 101 gsummptfidmsplit ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
103 10 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) = ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) )
104 103 oveqd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ( 𝑝 ‘ 𝐼 ) ) )
105 xpss1 ⊢ ( { 𝐼 } ⊆ 𝑁 → ( { 𝐼 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) )
106 98 105 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( { 𝐼 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) )
107 66 106 fssresd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) : ( { 𝐼 } × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
108 107 ffnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) Fn ( { 𝐼 } × 𝑁 ) )
109 75 106 fssresd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) : ( { 𝐼 } × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
110 109 ffnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) Fn ( { 𝐼 } × 𝑁 ) )
111 snex ⊢ { 𝐼 } ∈ V
112 xpexg ⊢ ( ( { 𝐼 } ∈ V ∧ 𝑁 ∈ Fin ) → ( { 𝐼 } × 𝑁 ) ∈ V )
113 111 40 112 sylancr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( { 𝐼 } × 𝑁 ) ∈ V )
114 snidg ⊢ ( 𝐼 ∈ 𝑁 → 𝐼 ∈ { 𝐼 } )
115 65 114 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝐼 ∈ { 𝐼 } )
116 115 67 opelxpd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ∈ ( { 𝐼 } × 𝑁 ) )
117 fnfvof ⊢ ( ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) Fn ( { 𝐼 } × 𝑁 ) ∧ ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) Fn ( { 𝐼 } × 𝑁 ) ) ∧ ( ( { 𝐼 } × 𝑁 ) ∈ V ∧ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ∈ ( { 𝐼 } × 𝑁 ) ) ) → ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) = ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) + ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) ) )
118 108 110 113 116 117 syl22anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) = ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) + ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) ) )
119 df-ov ⊢ ( 𝐼 ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ )
120 df-ov ⊢ ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ )
121 df-ov ⊢ ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ )
122 120 121 oveq12i ⊢ ( ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) = ( ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) + ( ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ‘ ⟨ 𝐼 , ( 𝑝 ‘ 𝐼 ) ⟩ ) )
123 118 119 122 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) )
124 104 123 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) )
125 ovres ⊢ ( ( 𝐼 ∈ { 𝐼 } ∧ ( 𝑝 ‘ 𝐼 ) ∈ 𝑁 ) → ( 𝐼 ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
126 115 67 125 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( 𝑋 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
127 ovres ⊢ ( ( 𝐼 ∈ { 𝐼 } ∧ ( 𝑝 ‘ 𝐼 ) ∈ 𝑁 ) → ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) )
128 115 67 127 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) )
129 ovres ⊢ ( ( 𝐼 ∈ { 𝐼 } ∧ ( 𝑝 ‘ 𝐼 ) ∈ 𝑁 ) → ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
130 115 67 129 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) = ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) )
131 128 130 oveq12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝐼 ( 𝑌 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 ( 𝑍 ↾ ( { 𝐼 } × 𝑁 ) ) ( 𝑝 ‘ 𝐼 ) ) ) = ( ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) )
132 124 126 131 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) = ( ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) )
133 86 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
134 133 65 67 fovrnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑅 ) )
135 69 70 oveq12d ⊢ ( 𝑟 = 𝐼 → ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
136 33 135 gsumsn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑁 ∧ ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
137 64 65 134 136 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( 𝐼 𝑋 ( 𝑝 ‘ 𝐼 ) ) )
138 73 79 oveq12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( 𝐼 𝑌 ( 𝑝 ‘ 𝐼 ) ) + ( 𝐼 𝑍 ( 𝑝 ‘ 𝐼 ) ) ) )
139 132 137 138 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
140 139 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
141 102 140 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
142 33 94 39 40 50 96 101 gsummptfidmsplit ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
143 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑌 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
144 143 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 ( 𝑌 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) )
145 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) )
146 83 49 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 )
147 ovres ⊢ ( ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) )
148 145 146 147 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) )
149 ovres ⊢ ( ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 ) → ( 𝑟 ( 𝑌 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) )
150 145 146 149 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑌 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) )
151 144 148 150 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) )
152 151 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) = ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) )
153 152 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) )
154 153 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
155 142 154 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
156 33 94 39 40 57 96 101 gsummptfidmsplit ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
157 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
158 157 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑋 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) )
159 ovres ⊢ ( ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ ( 𝑝 ‘ 𝑟 ) ∈ 𝑁 ) → ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) )
160 145 146 159 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 ( 𝑍 ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) )
161 158 148 160 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) = ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) )
162 161 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) = ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) )
163 162 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) )
164 163 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
165 156 164 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) = ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
166 155 165 oveq12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ { 𝐼 } ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
167 93 141 166 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) )
168 167 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) + ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
169 62 168 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) )
170 169 mpteq2dva ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) + ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
171 21 170 eqtrid ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ∘f + ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) )
172 171 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ∘f + ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
173 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
174 5 22 173 3syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
175 46 30 symgbasfi ⊢ ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
176 27 175 syl ⊢ ( 𝜑 → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
177 32 60 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
178 24 36 52 177 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
179 32 60 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
180 24 36 59 179 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
181 32 4 174 176 178 180 15 18 gsummptfidmadd2 ⊢ ( 𝜑 → ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ∘f + ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) + ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
182 172 181 eqtr3d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) + ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
183 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
184 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
185 1 2 3 30 183 184 60 31 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
186 5 6 185 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑋 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
187 1 2 3 30 183 184 60 31 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
188 5 7 187 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
189 1 2 3 30 183 184 60 31 mdetleib2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑍 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑍 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
190 5 8 189 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑍 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) )
191 188 190 oveq12d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑌 ) + ( 𝐷 ‘ 𝑍 ) ) = ( ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑌 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) + ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑍 ( 𝑝 ‘ 𝑟 ) ) ) ) ) ) ) ) )
192 182 186 191 3eqtr4d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( ( 𝐷 ‘ 𝑌 ) + ( 𝐷 ‘ 𝑍 ) ) )