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