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 ⊢ D = N maDet R
mdetralt.a ⊢ A = N Mat R
mdetralt.b ⊢ B = Base A
mdetralt.z ⊢ 0 ˙ = 0 R
mdetralt.r ⊢ φ → R ∈ CRing
mdetralt.x ⊢ φ → X ∈ B
mdetralt.i ⊢ φ → I ∈ N
mdetralt.j ⊢ φ → J ∈ N
mdetralt.ij ⊢ φ → I ≠ J
mdetralt.eq ⊢ φ → ∀ a ∈ N I X a = J X a
Assertion mdetralt ⊢ φ → D ⁡ X = 0 ˙

Proof

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