Metamath Proof Explorer

Theorem cyc3conja

Description: All 3-cycles are conjugate in the alternating group A_n for n>= 5. Property (b) of Lang p. 32. (Contributed by Thierry Arnoux, 15-Oct-2023)

Ref Expression
Hypotheses cyc3conja.c 
|- C = ( M " ( `' # " { 3 } ) )
cyc3conja.a 
|- A = ( pmEven ` D )
cyc3conja.s 
|- S = ( SymGrp ` D )
cyc3conja.n 
|- N = ( # ` D )
cyc3conja.m 
|- M = ( toCyc ` D )
cyc3conja.p 
|- .+ = ( +g ` S )
cyc3conja.l 
|- .- = ( -g ` S )
cyc3conja.1 
|- ( ph -> 5 <_ N )
cyc3conja.d 
|- ( ph -> D e. Fin )
cyc3conja.q 
|- ( ph -> Q e. C )
cyc3conja.t 
|- ( ph -> T e. C )
Assertion cyc3conja 
|- ( ph -> E. p e. A Q = ( ( p .+ T ) .- p ) )

Proof

Step Hyp Ref Expression
1 cyc3conja.c 
 |-  C = ( M " ( `' # " { 3 } ) )
2 cyc3conja.a 
 |-  A = ( pmEven ` D )
3 cyc3conja.s 
 |-  S = ( SymGrp ` D )
4 cyc3conja.n 
 |-  N = ( # ` D )
5 cyc3conja.m 
 |-  M = ( toCyc ` D )
6 cyc3conja.p 
 |-  .+ = ( +g ` S )
7 cyc3conja.l 
 |-  .- = ( -g ` S )
8 cyc3conja.1 
 |-  ( ph -> 5 <_ N )
9 cyc3conja.d 
 |-  ( ph -> D e. Fin )
10 cyc3conja.q 
 |-  ( ph -> Q e. C )
11 cyc3conja.t 
 |-  ( ph -> T e. C )
12 simpr 
 |-  ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) -> g e. A )
13 simpr 
 |-  ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) /\ p = g ) -> p = g )
14 13 oveq1d 
 |-  ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) /\ p = g ) -> ( p .+ T ) = ( g .+ T ) )
15 14 13 oveq12d 
 |-  ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) /\ p = g ) -> ( ( p .+ T ) .- p ) = ( ( g .+ T ) .- g ) )
16 15 eqeq2d 
 |-  ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) /\ p = g ) -> ( Q = ( ( p .+ T ) .- p ) <-> Q = ( ( g .+ T ) .- g ) ) )
17 simplr 
 |-  ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) -> Q = ( ( g .+ T ) .- g ) )
18 12 16 17 rspcedvd 
 |-  ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ g e. A ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
19 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> D e. Fin )
20 19 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> D e. Fin )
21 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> g e. ( Base ` S ) )
22 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> -. g e. A )
23 21 22 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> g e. ( ( Base ` S ) \ A ) )
24 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> x e. ( D \ ran u ) )
25 24 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> x e. D )
26 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> y e. ( D \ ran u ) )
27 26 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> y e. D )
28 25 27 prssd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> { x , y } C_ D )
29 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> x =/= y )
30 enpr2 
 |-  ( ( x e. ( D \ ran u ) /\ y e. ( D \ ran u ) /\ x =/= y ) -> { x , y } ~~ 2o )
31 24 26 29 30 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> { x , y } ~~ 2o )
32 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
33 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
34 32 33 pmtrrn 
 |-  ( ( D e. Fin /\ { x , y } C_ D /\ { x , y } ~~ 2o ) -> ( ( pmTrsp ` D ) ` { x , y } ) e. ran ( pmTrsp ` D ) )
35 20 28 31 34 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( pmTrsp ` D ) ` { x , y } ) e. ran ( pmTrsp ` D ) )
36 eqid 
 |-  ( Base ` S ) = ( Base ` S )
37 3 36 33 pmtrodpm 
 |-  ( ( D e. Fin /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ran ( pmTrsp ` D ) ) -> ( ( pmTrsp ` D ) ` { x , y } ) e. ( ( Base ` S ) \ ( pmEven ` D ) ) )
38 20 35 37 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( pmTrsp ` D ) ` { x , y } ) e. ( ( Base ` S ) \ ( pmEven ` D ) ) )
39 2 difeq2i 
 |-  ( ( Base ` S ) \ A ) = ( ( Base ` S ) \ ( pmEven ` D ) )
40 38 39 eleqtrrdi 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( pmTrsp ` D ) ` { x , y } ) e. ( ( Base ` S ) \ A ) )
41 3 36 2 odpmco 
 |-  ( ( D e. Fin /\ g e. ( ( Base ` S ) \ A ) /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ( ( Base ` S ) \ A ) ) -> ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) e. A )
42 20 23 40 41 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) e. A )
43 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) /\ p = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) -> p = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
44 43 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) /\ p = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) -> ( p .+ T ) = ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) )
45 44 43 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) /\ p = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) -> ( ( p .+ T ) .- p ) = ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) .- ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) )
46 45 eqeq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) /\ p = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) -> ( Q = ( ( p .+ T ) .- p ) <-> Q = ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) .- ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) ) )
47 38 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) )
48 0zd 
 |-  ( ph -> 0 e. ZZ )
49 hashcl 
 |-  ( D e. Fin -> ( # ` D ) e. NN0 )
50 9 49 syl 
 |-  ( ph -> ( # ` D ) e. NN0 )
51 4 50 eqeltrid 
 |-  ( ph -> N e. NN0 )
52 51 nn0zd 
 |-  ( ph -> N e. ZZ )
53 3z 
 |-  3 e. ZZ
54 53 a1i 
 |-  ( ph -> 3 e. ZZ )
55 0red 
 |-  ( ph -> 0 e. RR )
56 54 zred 
 |-  ( ph -> 3 e. RR )
57 3pos 
 |-  0 < 3
58 57 a1i 
 |-  ( ph -> 0 < 3 )
59 55 56 58 ltled 
 |-  ( ph -> 0 <_ 3 )
60 5re 
 |-  5 e. RR
61 60 a1i 
 |-  ( ph -> 5 e. RR )
62 51 nn0red 
 |-  ( ph -> N e. RR )
63 3lt5 
 |-  3 < 5
64 63 a1i 
 |-  ( ph -> 3 < 5 )
65 56 61 64 ltled 
 |-  ( ph -> 3 <_ 5 )
66 56 61 62 65 8 letrd 
 |-  ( ph -> 3 <_ N )
67 48 52 54 59 66 elfzd 
 |-  ( ph -> 3 e. ( 0 ... N ) )
68 1 3 4 5 36 cycpmgcl 
 |-  ( ( D e. Fin /\ 3 e. ( 0 ... N ) ) -> C C_ ( Base ` S ) )
69 9 67 68 syl2anc 
 |-  ( ph -> C C_ ( Base ` S ) )
70 69 11 sseldd 
 |-  ( ph -> T e. ( Base ` S ) )
71 70 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> T e. ( Base ` S ) )
72 5 20 25 27 29 32 cycpm2tr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( M ` <" x y "> ) = ( ( pmTrsp ` D ) ` { x , y } ) )
73 72 reseq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( M ` <" x y "> ) |` ran u ) = ( ( ( pmTrsp ` D ) ` { x , y } ) |` ran u ) )
74 25 27 s2cld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> <" x y "> e. Word D )
75 25 27 29 s2f1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> <" x y "> : dom <" x y "> -1-1-> D )
76 5 20 74 75 tocycfvres2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( M ` <" x y "> ) |` ( D \ ran <" x y "> ) ) = ( _I |` ( D \ ran <" x y "> ) ) )
77 76 reseq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( M ` <" x y "> ) |` ( D \ ran <" x y "> ) ) |` ran u ) = ( ( _I |` ( D \ ran <" x y "> ) ) |` ran u ) )
78 simplr 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) )
79 78 elin1d 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> u e. { w e. Word D | w : dom w -1-1-> D } )
80 id 
 |-  ( w = u -> w = u )
81 dmeq 
 |-  ( w = u -> dom w = dom u )
82 eqidd 
 |-  ( w = u -> D = D )
83 80 81 82 f1eq123d 
 |-  ( w = u -> ( w : dom w -1-1-> D <-> u : dom u -1-1-> D ) )
84 83 elrab 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } <-> ( u e. Word D /\ u : dom u -1-1-> D ) )
85 79 84 sylib 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ( u e. Word D /\ u : dom u -1-1-> D ) )
86 85 simprd 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> u : dom u -1-1-> D )
87 f1f 
 |-  ( u : dom u -1-1-> D -> u : dom u --> D )
88 frn 
 |-  ( u : dom u --> D -> ran u C_ D )
89 86 87 88 3syl 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ran u C_ D )
90 89 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ran u C_ D )
91 24 26 prssd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> { x , y } C_ ( D \ ran u ) )
92 ssconb 
 |-  ( ( { x , y } C_ D /\ ran u C_ D ) -> ( { x , y } C_ ( D \ ran u ) <-> ran u C_ ( D \ { x , y } ) ) )
93 92 biimpa 
 |-  ( ( ( { x , y } C_ D /\ ran u C_ D ) /\ { x , y } C_ ( D \ ran u ) ) -> ran u C_ ( D \ { x , y } ) )
94 28 90 91 93 syl21anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ran u C_ ( D \ { x , y } ) )
95 24 26 s2rn 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ran <" x y "> = { x , y } )
96 95 difeq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( D \ ran <" x y "> ) = ( D \ { x , y } ) )
97 94 96 sseqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ran u C_ ( D \ ran <" x y "> ) )
98 97 resabs1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( M ` <" x y "> ) |` ( D \ ran <" x y "> ) ) |` ran u ) = ( ( M ` <" x y "> ) |` ran u ) )
99 97 resabs1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( _I |` ( D \ ran <" x y "> ) ) |` ran u ) = ( _I |` ran u ) )
100 77 98 99 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( M ` <" x y "> ) |` ran u ) = ( _I |` ran u ) )
101 73 100 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( pmTrsp ` D ) ` { x , y } ) |` ran u ) = ( _I |` ran u ) )
102 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( M ` u ) = T )
103 102 reseq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( M ` u ) |` ( D \ ran u ) ) = ( T |` ( D \ ran u ) ) )
104 85 simpld 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> u e. Word D )
105 104 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> u e. Word D )
106 86 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> u : dom u -1-1-> D )
107 5 20 105 106 tocycfvres2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( M ` u ) |` ( D \ ran u ) ) = ( _I |` ( D \ ran u ) ) )
108 103 107 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( T |` ( D \ ran u ) ) = ( _I |` ( D \ ran u ) ) )
109 disjdif 
 |-  ( ran u i^i ( D \ ran u ) ) = (/)
110 109 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ran u i^i ( D \ ran u ) ) = (/) )
111 undif 
 |-  ( ran u C_ D <-> ( ran u u. ( D \ ran u ) ) = D )
112 90 111 sylib 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ran u u. ( D \ ran u ) ) = D )
113 3 36 47 71 101 108 110 112 symgcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( pmTrsp ` D ) ` { x , y } ) o. T ) = ( T o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
114 113 coeq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. T ) ) = ( g o. ( T o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) )
115 3 36 6 symgov 
 |-  ( ( g e. ( Base ` S ) /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) ) -> ( g .+ ( ( pmTrsp ` D ) ` { x , y } ) ) = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
116 21 47 115 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g .+ ( ( pmTrsp ` D ) ` { x , y } ) ) = ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
117 3 36 6 symgcl 
 |-  ( ( g e. ( Base ` S ) /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) ) -> ( g .+ ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) )
118 21 47 117 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g .+ ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) )
119 116 118 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) )
120 3 36 6 symgov 
 |-  ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) /\ T e. ( Base ` S ) ) -> ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) = ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. T ) )
121 119 71 120 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) = ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. T ) )
122 coass 
 |-  ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. T ) = ( g o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. T ) )
123 121 122 eqtrdi 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) = ( g o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. T ) ) )
124 coass 
 |-  ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) = ( g o. ( T o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
125 124 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) = ( g o. ( T o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) )
126 114 123 125 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) = ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
127 cnvco 
 |-  `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) = ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g )
128 127 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) = ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g ) )
129 126 128 coeq12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) o. `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) = ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g ) ) )
130 coass 
 |-  ( ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) o. `' g ) = ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g ) )
131 coass 
 |-  ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) = ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) )
132 131 coeq1i 
 |-  ( ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) o. `' g ) = ( ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) o. `' g )
133 130 132 eqtr3i 
 |-  ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g ) ) = ( ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) o. `' g )
134 133 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g ) ) = ( ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) o. `' g ) )
135 3 36 6 symgov 
 |-  ( ( g e. ( Base ` S ) /\ T e. ( Base ` S ) ) -> ( g .+ T ) = ( g o. T ) )
136 21 71 135 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g .+ T ) = ( g o. T ) )
137 3 36 6 symgcl 
 |-  ( ( g e. ( Base ` S ) /\ T e. ( Base ` S ) ) -> ( g .+ T ) e. ( Base ` S ) )
138 21 71 137 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g .+ T ) e. ( Base ` S ) )
139 136 138 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( g o. T ) e. ( Base ` S ) )
140 3 36 symgbasf 
 |-  ( ( g o. T ) e. ( Base ` S ) -> ( g o. T ) : D --> D )
141 fcoi1 
 |-  ( ( g o. T ) : D --> D -> ( ( g o. T ) o. ( _I |` D ) ) = ( g o. T ) )
142 139 140 141 3syl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. T ) o. ( _I |` D ) ) = ( g o. T ) )
143 3 36 elsymgbas 
 |-  ( D e. Fin -> ( ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) <-> ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D ) )
144 143 biimpa 
 |-  ( ( D e. Fin /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) ) -> ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D )
145 20 47 144 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D )
146 f1ococnv2 
 |-  ( ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D -> ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) = ( _I |` D ) )
147 145 146 syl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) = ( _I |` D ) )
148 147 coeq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) = ( ( g o. T ) o. ( _I |` D ) ) )
149 142 148 136 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) = ( g .+ T ) )
150 149 coeq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) o. `' g ) = ( ( g .+ T ) o. `' g ) )
151 3 36 7 symgsubg 
 |-  ( ( ( g .+ T ) e. ( Base ` S ) /\ g e. ( Base ` S ) ) -> ( ( g .+ T ) .- g ) = ( ( g .+ T ) o. `' g ) )
152 138 21 151 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g .+ T ) .- g ) = ( ( g .+ T ) o. `' g ) )
153 150 152 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( g o. T ) o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) ) o. `' g ) = ( ( g .+ T ) .- g ) )
154 129 134 153 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) o. `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) = ( ( g .+ T ) .- g ) )
155 3 symggrp 
 |-  ( D e. Fin -> S e. Grp )
156 9 155 syl 
 |-  ( ph -> S e. Grp )
157 156 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> S e. Grp )
158 36 6 grpcl 
 |-  ( ( S e. Grp /\ ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) /\ T e. ( Base ` S ) ) -> ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) e. ( Base ` S ) )
159 157 119 71 158 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) e. ( Base ` S ) )
160 3 36 7 symgsubg 
 |-  ( ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) e. ( Base ` S ) /\ ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) ) -> ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) .- ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) = ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) o. `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) )
161 159 119 160 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) .- ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) = ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) o. `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) )
162 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> Q = ( ( g .+ T ) .- g ) )
163 154 161 162 3eqtr4rd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> Q = ( ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) .+ T ) .- ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) ) )
164 42 46 163 rspcedvd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) /\ x e. ( D \ ran u ) ) /\ y e. ( D \ ran u ) ) /\ x =/= y ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
165 9 difexd 
 |-  ( ph -> ( D \ ran u ) e. _V )
166 165 ad5antr 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ( D \ ran u ) e. _V )
167 3p2e5 
 |-  ( 3 + 2 ) = 5
168 167 8 eqbrtrid 
 |-  ( ph -> ( 3 + 2 ) <_ N )
169 2re 
 |-  2 e. RR
170 169 a1i 
 |-  ( ph -> 2 e. RR )
171 56 170 62 leaddsub2d 
 |-  ( ph -> ( ( 3 + 2 ) <_ N <-> 2 <_ ( N - 3 ) ) )
172 168 171 mpbid 
 |-  ( ph -> 2 <_ ( N - 3 ) )
173 172 ad5antr 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> 2 <_ ( N - 3 ) )
174 4 a1i 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> N = ( # ` D ) )
175 78 elin2d 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> u e. ( `' # " { 3 } ) )
176 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
177 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
178 fniniseg 
 |-  ( # Fn _V -> ( u e. ( `' # " { 3 } ) <-> ( u e. _V /\ ( # ` u ) = 3 ) ) )
179 176 177 178 mp2b 
 |-  ( u e. ( `' # " { 3 } ) <-> ( u e. _V /\ ( # ` u ) = 3 ) )
180 179 simprbi 
 |-  ( u e. ( `' # " { 3 } ) -> ( # ` u ) = 3 )
181 175 180 syl 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ( # ` u ) = 3 )
182 vex 
 |-  u e. _V
183 182 dmex 
 |-  dom u e. _V
184 hashf1rn 
 |-  ( ( dom u e. _V /\ u : dom u -1-1-> D ) -> ( # ` u ) = ( # ` ran u ) )
185 183 86 184 sylancr 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ( # ` u ) = ( # ` ran u ) )
186 181 185 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> 3 = ( # ` ran u ) )
187 174 186 oveq12d 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ( N - 3 ) = ( ( # ` D ) - ( # ` ran u ) ) )
188 173 187 breqtrd 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> 2 <_ ( ( # ` D ) - ( # ` ran u ) ) )
189 hashssdif 
 |-  ( ( D e. Fin /\ ran u C_ D ) -> ( # ` ( D \ ran u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
190 19 89 189 syl2anc 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> ( # ` ( D \ ran u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
191 188 190 breqtrrd 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> 2 <_ ( # ` ( D \ ran u ) ) )
192 hashge2el2dif 
 |-  ( ( ( D \ ran u ) e. _V /\ 2 <_ ( # ` ( D \ ran u ) ) ) -> E. x e. ( D \ ran u ) E. y e. ( D \ ran u ) x =/= y )
193 166 191 192 syl2anc 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> E. x e. ( D \ ran u ) E. y e. ( D \ ran u ) x =/= y )
194 164 193 r19.29vva 
 |-  ( ( ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( M ` u ) = T ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
195 nfcv 
 |-  F/_ u M
196 5 3 36 tocycf 
 |-  ( D e. Fin -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
197 ffn 
 |-  ( M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) -> M Fn { w e. Word D | w : dom w -1-1-> D } )
198 9 196 197 3syl 
 |-  ( ph -> M Fn { w e. Word D | w : dom w -1-1-> D } )
199 11 1 eleqtrdi 
 |-  ( ph -> T e. ( M " ( `' # " { 3 } ) ) )
200 195 198 199 fvelimad 
 |-  ( ph -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ( M ` u ) = T )
201 200 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ( M ` u ) = T )
202 194 201 r19.29a 
 |-  ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
203 18 202 pm2.61dan 
 |-  ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
204 1 3 4 5 36 6 7 67 9 10 11 cycpmconjs 
 |-  ( ph -> E. g e. ( Base ` S ) Q = ( ( g .+ T ) .- g ) )
205 203 204 r19.29a 
 |-  ( ph -> E. p e. A Q = ( ( p .+ T ) .- p ) )