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

Metamath Proof Explorer

Theorem mdetralt

Description: The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in Lang p. 515. (Contributed by SO, 10-Jul-2018) (Proof shortened by AV, 23-Jul-2018)

Ref Expression
Hypotheses mdetralt.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetralt.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetralt.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetralt.z ⊢ 0 = ( 0g ‘ 𝑅 )
mdetralt.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mdetralt.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mdetralt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
mdetralt.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
mdetralt.ij ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
mdetralt.eq ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑁 ( 𝐼 𝑋 𝑎 ) = ( 𝐽 𝑋 𝑎 ) )
Assertion mdetralt ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 mdetralt.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetralt.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 mdetralt.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mdetralt.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 mdetralt.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 mdetralt.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 mdetralt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
8 mdetralt.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
9 mdetralt.ij ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
10 mdetralt.eq ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑁 ( 𝐼 𝑋 𝑎 ) = ( 𝐽 𝑋 𝑎 ) )
11 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
12 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
13 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
14 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
15 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
16 1 2 3 11 12 13 14 15 mdetleib ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐷 ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) )
17 6 16 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
20 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
21 5 20 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
22 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
23 21 22 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
24 2 3 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
25 6 24 syl ⊢ ( 𝜑 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
26 25 simpld ⊢ ( 𝜑 → 𝑁 ∈ Fin )
27 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
28 27 11 symgbasfi ⊢ ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
29 26 28 syl ⊢ ( 𝜑 → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
30 21 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
31 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
32 21 26 31 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
33 15 18 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
34 11 33 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ 𝑅 ) )
35 32 34 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ 𝑅 ) )
36 35 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) )
37 15 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
38 5 37 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
40 26 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑁 ∈ Fin )
41 2 18 3 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
42 6 41 syl ⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
43 elmapi ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
44 42 43 syl ⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
46 27 11 symgbasf1o ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → 𝑝 : 𝑁 –1-1-onto→ 𝑁 )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑝 : 𝑁 –1-1-onto→ 𝑁 )
48 f1of ⊢ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 → 𝑝 : 𝑁 ⟶ 𝑁 )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑝 : 𝑁 ⟶ 𝑁 )
50 49 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑐 ) ∈ 𝑁 )
51 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
52 45 50 51 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
53 52 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑐 ∈ 𝑁 ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
54 33 39 40 53 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) )
55 18 14 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
56 30 36 54 55 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
57 disjdif ⊢ ( ( pmEven ‘ 𝑁 ) ∩ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ∅
58 57 a1i ⊢ ( 𝜑 → ( ( pmEven ‘ 𝑁 ) ∩ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ∅ )
59 27 11 evpmss ⊢ ( pmEven ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
60 undif ⊢ ( ( pmEven ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ ( ( pmEven ‘ 𝑁 ) ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
61 59 60 mpbi ⊢ ( ( pmEven ‘ 𝑁 ) ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
62 61 eqcomi ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( ( pmEven ‘ 𝑁 ) ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
63 62 a1i ⊢ ( 𝜑 → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( ( pmEven ‘ 𝑁 ) ∪ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) )
64 eqid ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
65 18 19 23 29 56 58 63 64 gsummptfidmsplitres ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) = ( ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ) ) )
66 resmpt ⊢ ( ( pmEven ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
67 59 66 ax-mp ⊢ ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
68 21 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → 𝑅 ∈ Ring )
69 26 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → 𝑁 ∈ Fin )
70 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → 𝑝 ∈ ( pmEven ‘ 𝑁 ) )
71 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
72 12 13 71 zrhpsgnevpm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) = ( 1r ‘ 𝑅 ) )
73 68 69 70 72 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) = ( 1r ‘ 𝑅 ) )
74 73 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
75 59 sseli ⊢ ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
76 75 54 sylan2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) )
77 18 14 71 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
78 68 76 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
79 74 78 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
80 79 mpteq2dva ⊢ ( 𝜑 → ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
81 67 80 eqtrid ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
82 81 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
83 difss ⊢ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
84 resmpt ⊢ ( ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
85 83 84 ax-mp ⊢ ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
86 21 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
87 26 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → 𝑁 ∈ Fin )
88 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
89 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
90 12 13 71 11 89 zrhpsgnodpm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
91 86 87 88 90 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
92 91 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
93 eldifi ⊢ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
94 93 54 sylan2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) )
95 18 14 71 89 86 94 ringnegl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
96 92 95 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
97 96 mpteq2dva ⊢ ( 𝜑 → ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( invg ‘ 𝑅 ) ‘ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
98 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
99 21 98 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
100 18 89 grpinvf ⊢ ( 𝑅 ∈ Grp → ( invg ‘ 𝑅 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
101 99 100 syl ⊢ ( 𝜑 → ( invg ‘ 𝑅 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
102 101 94 cofmpt ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ∘ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( invg ‘ 𝑅 ) ‘ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
103 97 102 eqtr4d ⊢ ( 𝜑 → ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( ( invg ‘ 𝑅 ) ∘ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
104 85 103 eqtrid ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) = ( ( invg ‘ 𝑅 ) ∘ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
105 104 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ) = ( 𝑅 Σg ( ( invg ‘ 𝑅 ) ∘ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) )
106 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
107 21 106 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
108 difssd ⊢ ( 𝜑 → ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
109 29 108 ssfid ⊢ ( 𝜑 → ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ∈ Fin )
110 eqid ⊢ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
111 18 4 89 107 109 94 110 gsummptfidminv ⊢ ( 𝜑 → ( 𝑅 Σg ( ( invg ‘ 𝑅 ) ∘ ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) )
112 94 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) )
113 7 8 prssd ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ 𝑁 )
114 enpr2 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → { 𝐼 , 𝐽 } ≈ 2o )
115 7 8 9 114 syl3anc ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ≈ 2o )
116 eqid ⊢ ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
117 eqid ⊢ ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
118 116 117 pmtrrn ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝐼 , 𝐽 } ⊆ 𝑁 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝑁 ) )
119 26 113 115 118 syl3anc ⊢ ( 𝜑 → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝑁 ) )
120 27 11 117 pmtrodpm ⊢ ( ( 𝑁 ∈ Fin ∧ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
121 26 119 120 syl2anc ⊢ ( 𝜑 → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
122 27 11 evpmodpmf1o ⊢ ( ( 𝑁 ∈ Fin ∧ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) : ( pmEven ‘ 𝑁 ) –1-1-onto→ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
123 26 121 122 syl2anc ⊢ ( 𝜑 → ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) : ( pmEven ‘ 𝑁 ) –1-1-onto→ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
124 18 23 109 112 110 123 gsummptfif1o ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ∘ ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) ) ) )
125 eleq1w ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↔ 𝑞 ∈ ( pmEven ‘ 𝑁 ) ) )
126 125 anbi2d ⊢ ( 𝑝 = 𝑞 → ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑞 ∈ ( pmEven ‘ 𝑁 ) ) ) )
127 oveq2 ⊢ ( 𝑝 = 𝑞 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) )
128 127 eleq1d ⊢ ( 𝑝 = 𝑞 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↔ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) )
129 126 128 imbi12d ⊢ ( 𝑝 = 𝑞 → ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ↔ ( ( 𝜑 ∧ 𝑞 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ) )
130 27 symggrp ⊢ ( 𝑁 ∈ Fin → ( SymGrp ‘ 𝑁 ) ∈ Grp )
131 26 130 syl ⊢ ( 𝜑 → ( SymGrp ‘ 𝑁 ) ∈ Grp )
132 131 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( SymGrp ‘ 𝑁 ) ∈ Grp )
133 117 27 11 symgtrf ⊢ ran ( pmTrsp ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
134 119 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝑁 ) )
135 133 134 sselid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
136 75 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
137 eqid ⊢ ( +g ‘ ( SymGrp ‘ 𝑁 ) ) = ( +g ‘ ( SymGrp ‘ 𝑁 ) )
138 11 137 grpcl ⊢ ( ( ( SymGrp ‘ 𝑁 ) ∈ Grp ∧ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
139 132 135 136 138 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
140 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
141 27 13 140 psgnghm2 ⊢ ( 𝑁 ∈ Fin → ( pmSgn ‘ 𝑁 ) ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
142 26 141 syl ⊢ ( 𝜑 → ( pmSgn ‘ 𝑁 ) ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
143 142 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( pmSgn ‘ 𝑁 ) ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
144 prex ⊢ { 1 , - 1 } ∈ V
145 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
146 cnfldmul ⊢ · = ( .r ‘ ℂfld )
147 145 146 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
148 140 147 ressplusg ⊢ ( { 1 , - 1 } ∈ V → · = ( +g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
149 144 148 ax-mp ⊢ · = ( +g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
150 11 137 149 ghmlin ⊢ ( ( ( pmSgn ‘ 𝑁 ) ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( pmSgn ‘ 𝑁 ) ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ) · ( ( pmSgn ‘ 𝑁 ) ‘ 𝑝 ) ) )
151 143 135 136 150 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmSgn ‘ 𝑁 ) ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ) · ( ( pmSgn ‘ 𝑁 ) ‘ 𝑝 ) ) )
152 27 117 13 psgnpmtr ⊢ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝑁 ) → ( ( pmSgn ‘ 𝑁 ) ‘ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ) = - 1 )
153 134 152 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmSgn ‘ 𝑁 ) ‘ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ) = - 1 )
154 27 11 13 psgnevpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑝 ) = 1 )
155 26 154 sylan ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑝 ) = 1 )
156 153 155 oveq12d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmSgn ‘ 𝑁 ) ‘ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ) · ( ( pmSgn ‘ 𝑁 ) ‘ 𝑝 ) ) = ( - 1 · 1 ) )
157 neg1cn ⊢ - 1 ∈ ℂ
158 157 mulridi ⊢ ( - 1 · 1 ) = - 1
159 156 158 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmSgn ‘ 𝑁 ) ‘ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ) · ( ( pmSgn ‘ 𝑁 ) ‘ 𝑝 ) ) = - 1 )
160 151 159 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( pmSgn ‘ 𝑁 ) ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ) = - 1 )
161 27 11 13 psgnodpmr ⊢ ( ( 𝑁 ∈ Fin ∧ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ ( ( pmSgn ‘ 𝑁 ) ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ) = - 1 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
162 69 139 160 161 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
163 129 162 chvarvv ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
164 eqidd ⊢ ( 𝜑 → ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) = ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) )
165 eqidd ⊢ ( 𝜑 → ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
166 fveq1 ⊢ ( 𝑝 = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) → ( 𝑝 ‘ 𝑐 ) = ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) )
167 166 oveq1d ⊢ ( 𝑝 = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) → ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) = ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) )
168 167 mpteq2dv ⊢ ( 𝑝 = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) → ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) = ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) )
169 168 oveq2d ⊢ ( 𝑝 = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
170 163 164 165 169 fmptco ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ∘ ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) ) = ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
171 oveq2 ⊢ ( 𝑞 = 𝑝 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) )
172 171 fveq1d ⊢ ( 𝑞 = 𝑝 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) = ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) )
173 172 oveq1d ⊢ ( 𝑞 = 𝑝 → ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) = ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) )
174 173 mpteq2dv ⊢ ( 𝑞 = 𝑝 → ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) = ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) )
175 174 oveq2d ⊢ ( 𝑞 = 𝑝 → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
176 175 cbvmptv ⊢ ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
177 176 a1i ⊢ ( 𝜑 → ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
178 135 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
179 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
180 27 11 137 symgov ⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∘ 𝑝 ) )
181 178 179 180 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∘ 𝑝 ) )
182 181 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) = ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∘ 𝑝 ) ‘ 𝑐 ) )
183 75 49 sylan2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → 𝑝 : 𝑁 ⟶ 𝑁 )
184 fvco3 ⊢ ( ( 𝑝 : 𝑁 ⟶ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∘ 𝑝 ) ‘ 𝑐 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) )
185 183 184 sylan ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∘ 𝑝 ) ‘ 𝑐 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) )
186 182 185 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) )
187 186 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) = ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) )
188 116 pmtrprfv ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) = 𝐽 )
189 26 7 8 9 188 syl13anc ⊢ ( 𝜑 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) = 𝐽 )
190 189 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) = 𝐽 )
191 190 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) 𝑋 𝑐 ) = ( 𝐽 𝑋 𝑐 ) )
192 oveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐼 𝑋 𝑎 ) = ( 𝐼 𝑋 𝑐 ) )
193 oveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐽 𝑋 𝑎 ) = ( 𝐽 𝑋 𝑐 ) )
194 192 193 eqeq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝐼 𝑋 𝑎 ) = ( 𝐽 𝑋 𝑎 ) ↔ ( 𝐼 𝑋 𝑐 ) = ( 𝐽 𝑋 𝑐 ) ) )
195 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ∀ 𝑎 ∈ 𝑁 ( 𝐼 𝑋 𝑎 ) = ( 𝐽 𝑋 𝑎 ) )
196 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
197 194 195 196 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( 𝐼 𝑋 𝑐 ) = ( 𝐽 𝑋 𝑐 ) )
198 191 197 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) 𝑋 𝑐 ) = ( 𝐼 𝑋 𝑐 ) )
199 fveq2 ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐼 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) )
200 199 oveq1d ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐼 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) 𝑋 𝑐 ) )
201 oveq1 ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐼 → ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) = ( 𝐼 𝑋 𝑐 ) )
202 200 201 eqeq12d ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐼 → ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ↔ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐼 ) 𝑋 𝑐 ) = ( 𝐼 𝑋 𝑐 ) ) )
203 198 202 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) = 𝐼 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) )
204 prcom ⊢ { 𝐼 , 𝐽 } = { 𝐽 , 𝐼 }
205 204 fveq2i ⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐽 , 𝐼 } )
206 205 fveq1i ⊢ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐽 , 𝐼 } ) ‘ 𝐽 )
207 9 necomd ⊢ ( 𝜑 → 𝐽 ≠ 𝐼 )
208 116 pmtrprfv ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝐽 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ≠ 𝐼 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐽 , 𝐼 } ) ‘ 𝐽 ) = 𝐼 )
209 26 8 7 207 208 syl13anc ⊢ ( 𝜑 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐽 , 𝐼 } ) ‘ 𝐽 ) = 𝐼 )
210 206 209 eqtrid ⊢ ( 𝜑 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) = 𝐼 )
211 210 oveq1d ⊢ ( 𝜑 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) 𝑋 𝑐 ) = ( 𝐼 𝑋 𝑐 ) )
212 211 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) 𝑋 𝑐 ) = ( 𝐼 𝑋 𝑐 ) )
213 212 197 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) 𝑋 𝑐 ) = ( 𝐽 𝑋 𝑐 ) )
214 fveq2 ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐽 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) )
215 214 oveq1d ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐽 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) 𝑋 𝑐 ) )
216 oveq1 ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐽 → ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) = ( 𝐽 𝑋 𝑐 ) )
217 215 216 eqeq12d ⊢ ( ( 𝑝 ‘ 𝑐 ) = 𝐽 → ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ↔ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) 𝑋 𝑐 ) = ( 𝐽 𝑋 𝑐 ) ) )
218 213 217 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) = 𝐽 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) )
219 218 a1dd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) = 𝐽 → ( ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
220 neanior ⊢ ( ( ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) ↔ ¬ ( ( 𝑝 ‘ 𝑐 ) = 𝐽 ∨ ( 𝑝 ‘ 𝑐 ) = 𝐼 ) )
221 elpri ⊢ ( ( 𝑝 ‘ 𝑐 ) ∈ { 𝐼 , 𝐽 } → ( ( 𝑝 ‘ 𝑐 ) = 𝐼 ∨ ( 𝑝 ‘ 𝑐 ) = 𝐽 ) )
222 221 orcomd ⊢ ( ( 𝑝 ‘ 𝑐 ) ∈ { 𝐼 , 𝐽 } → ( ( 𝑝 ‘ 𝑐 ) = 𝐽 ∨ ( 𝑝 ‘ 𝑐 ) = 𝐼 ) )
223 222 con3i ⊢ ( ¬ ( ( 𝑝 ‘ 𝑐 ) = 𝐽 ∨ ( 𝑝 ‘ 𝑐 ) = 𝐼 ) → ¬ ( 𝑝 ‘ 𝑐 ) ∈ { 𝐼 , 𝐽 } )
224 220 223 sylbi ⊢ ( ( ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ¬ ( 𝑝 ‘ 𝑐 ) ∈ { 𝐼 , 𝐽 } )
225 224 3adant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ¬ ( 𝑝 ‘ 𝑐 ) ∈ { 𝐼 , 𝐽 } )
226 116 pmtrmvd ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝐼 , 𝐽 } ⊆ 𝑁 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
227 26 113 115 226 syl3anc ⊢ ( 𝜑 → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
228 227 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
229 228 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
230 225 229 neleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ¬ ( 𝑝 ‘ 𝑐 ) ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) )
231 116 pmtrf ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝐼 , 𝐽 } ⊆ 𝑁 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) : 𝑁 ⟶ 𝑁 )
232 26 113 115 231 syl3anc ⊢ ( 𝜑 → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) : 𝑁 ⟶ 𝑁 )
233 232 ffnd ⊢ ( 𝜑 → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) Fn 𝑁 )
234 233 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) Fn 𝑁 )
235 183 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑐 ) ∈ 𝑁 )
236 fnelnfp ⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) Fn 𝑁 ∧ ( 𝑝 ‘ 𝑐 ) ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) ↔ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) ≠ ( 𝑝 ‘ 𝑐 ) ) )
237 234 235 236 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) ↔ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) ≠ ( 𝑝 ‘ 𝑐 ) ) )
238 237 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ( ( 𝑝 ‘ 𝑐 ) ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) ↔ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) ≠ ( 𝑝 ‘ 𝑐 ) ) )
239 238 necon2bbid ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) = ( 𝑝 ‘ 𝑐 ) ↔ ¬ ( 𝑝 ‘ 𝑐 ) ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ∖ I ) ) )
240 230 239 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) = ( 𝑝 ‘ 𝑐 ) )
241 240 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 ∧ ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) )
242 241 3exp ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) ≠ 𝐽 → ( ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
243 219 242 pm2.61dne ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) ≠ 𝐼 → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) )
244 203 243 pm2.61dne ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝑝 ‘ 𝑐 ) ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) )
245 187 244 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) = ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) )
246 245 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) = ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) )
247 246 oveq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) )
248 247 mpteq2dva ⊢ ( 𝜑 → ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
249 170 177 248 3eqtrd ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ∘ ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) ) = ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) )
250 249 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ∘ ( 𝑞 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝐼 , 𝐽 } ) ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑞 ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
251 124 250 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) )
252 251 fveq2d ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) )
253 105 111 252 3eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) )
254 82 253 oveq12d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) ) )
255 59 a1i ⊢ ( 𝜑 → ( pmEven ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
256 29 255 ssfid ⊢ ( 𝜑 → ( pmEven ‘ 𝑁 ) ∈ Fin )
257 76 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( pmEven ‘ 𝑁 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) )
258 18 23 256 257 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
259 18 19 4 89 grprinv ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) ) = 0 )
260 99 258 259 syl2anc ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑝 ∈ ( pmEven ‘ 𝑁 ) ↦ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ) ) = 0 )
261 254 260 eqtrd ⊢ ( 𝜑 → ( ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( pmEven ‘ 𝑁 ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑋 𝑐 ) ) ) ) ) ↾ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) ) ) = 0 )
262 17 65 261 3eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 0 )