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 pr2nelem 
 |-  ( ( 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 elfz4 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ /\ 3 e. ZZ ) /\ ( 0 <_ 3 /\ 3 <_ N ) ) -> 3 e. ( 0 ... N ) )
68 48 52 54 59 66 67 syl32anc 
 |-  ( ph -> 3 e. ( 0 ... N ) )
69 1 3 4 5 36 cycpmgcl 
 |-  ( ( D e. Fin /\ 3 e. ( 0 ... N ) ) -> C C_ ( Base ` S ) )
70 9 68 69 syl2anc 
 |-  ( ph -> C C_ ( Base ` S ) )
71 70 11 sseldd 
 |-  ( ph -> T e. ( Base ` S ) )
72 71 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 ) )
73 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 } ) )
74 73 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 ) )
75 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 )
76 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 )
77 5 20 75 76 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 "> ) ) )
78 77 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 ) )
79 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 } ) ) )
80 79 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 } )
81 id 
 |-  ( w = u -> w = u )
82 dmeq 
 |-  ( w = u -> dom w = dom u )
83 eqidd 
 |-  ( w = u -> D = D )
84 81 82 83 f1eq123d 
 |-  ( w = u -> ( w : dom w -1-1-> D <-> u : dom u -1-1-> D ) )
85 84 elrab 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } <-> ( u e. Word D /\ u : dom u -1-1-> D ) )
86 80 85 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 ) )
87 86 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 )
88 f1f 
 |-  ( u : dom u -1-1-> D -> u : dom u --> D )
89 frn 
 |-  ( u : dom u --> D -> ran u C_ D )
90 87 88 89 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 )
91 90 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 )
92 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 ) )
93 ssconb 
 |-  ( ( { x , y } C_ D /\ ran u C_ D ) -> ( { x , y } C_ ( D \ ran u ) <-> ran u C_ ( D \ { x , y } ) ) )
94 93 biimpa 
 |-  ( ( ( { x , y } C_ D /\ ran u C_ D ) /\ { x , y } C_ ( D \ ran u ) ) -> ran u C_ ( D \ { x , y } ) )
95 28 91 92 94 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 } ) )
96 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 } )
97 96 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 } ) )
98 95 97 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 "> ) )
99 98 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 ) )
100 98 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 ) )
101 78 99 100 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 ) )
102 74 101 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 ) )
103 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 )
104 103 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 ) ) )
105 86 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 )
106 105 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 )
107 87 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 )
108 5 20 106 107 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 ) ) )
109 104 108 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 ) ) )
110 disjdif 
 |-  ( ran u i^i ( D \ ran u ) ) = (/)
111 110 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 ) ) = (/) )
112 undif 
 |-  ( ran u C_ D <-> ( ran u u. ( D \ ran u ) ) = D )
113 91 112 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 )
114 3 36 47 72 102 109 111 113 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 } ) ) )
115 114 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 } ) ) ) )
116 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 } ) ) )
117 21 47 116 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 } ) ) )
118 3 36 6 symgcl 
 |-  ( ( g e. ( Base ` S ) /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) ) -> ( g .+ ( ( pmTrsp ` D ) ` { x , y } ) ) e. ( Base ` S ) )
119 21 47 118 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 ) )
120 117 119 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 ) )
121 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 ) )
122 120 72 121 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 ) )
123 coass 
 |-  ( ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) o. T ) = ( g o. ( ( ( pmTrsp ` D ) ` { x , y } ) o. T ) )
124 122 123 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 ) ) )
125 coass 
 |-  ( ( g o. T ) o. ( ( pmTrsp ` D ) ` { x , y } ) ) = ( g o. ( T o. ( ( pmTrsp ` D ) ` { x , y } ) ) )
126 125 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 } ) ) ) )
127 115 124 126 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 } ) ) )
128 cnvco 
 |-  `' ( g o. ( ( pmTrsp ` D ) ` { x , y } ) ) = ( `' ( ( pmTrsp ` D ) ` { x , y } ) o. `' g )
129 128 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 ) )
130 127 129 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 ) ) )
131 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 ) )
132 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 } ) ) )
133 132 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 )
134 131 133 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 )
135 134 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 ) )
136 3 36 6 symgov 
 |-  ( ( g e. ( Base ` S ) /\ T e. ( Base ` S ) ) -> ( g .+ T ) = ( g o. T ) )
137 21 72 136 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 ) )
138 3 36 6 symgcl 
 |-  ( ( g e. ( Base ` S ) /\ T e. ( Base ` S ) ) -> ( g .+ T ) e. ( Base ` S ) )
139 21 72 138 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 ) )
140 137 139 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 ) )
141 3 36 symgbasf 
 |-  ( ( g o. T ) e. ( Base ` S ) -> ( g o. T ) : D --> D )
142 fcoi1 
 |-  ( ( g o. T ) : D --> D -> ( ( g o. T ) o. ( _I |` D ) ) = ( g o. T ) )
143 140 141 142 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 ) )
144 3 36 elsymgbas 
 |-  ( D e. Fin -> ( ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) <-> ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D ) )
145 144 biimpa 
 |-  ( ( D e. Fin /\ ( ( pmTrsp ` D ) ` { x , y } ) e. ( Base ` S ) ) -> ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D )
146 20 47 145 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 )
147 f1ococnv2 
 |-  ( ( ( pmTrsp ` D ) ` { x , y } ) : D -1-1-onto-> D -> ( ( ( pmTrsp ` D ) ` { x , y } ) o. `' ( ( pmTrsp ` D ) ` { x , y } ) ) = ( _I |` D ) )
148 146 147 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 ) )
149 148 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 ) ) )
150 143 149 137 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 ) )
151 150 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 ) )
152 3 36 7 symgsubg 
 |-  ( ( ( g .+ T ) e. ( Base ` S ) /\ g e. ( Base ` S ) ) -> ( ( g .+ T ) .- g ) = ( ( g .+ T ) o. `' g ) )
153 139 21 152 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 ) )
154 151 153 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 ) )
155 130 135 154 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 ) )
156 3 symggrp 
 |-  ( D e. Fin -> S e. Grp )
157 9 156 syl 
 |-  ( ph -> S e. Grp )
158 157 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 )
159 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 ) )
160 158 120 72 159 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 ) )
161 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 } ) ) ) )
162 160 120 161 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 } ) ) ) )
163 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 ) )
164 155 162 163 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 } ) ) ) )
165 42 46 164 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 ) )
166 difexg 
 |-  ( D e. Fin -> ( D \ ran u ) e. _V )
167 9 166 syl 
 |-  ( ph -> ( D \ ran u ) e. _V )
168 167 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 )
169 3p2e5 
 |-  ( 3 + 2 ) = 5
170 169 8 eqbrtrid 
 |-  ( ph -> ( 3 + 2 ) <_ N )
171 2re 
 |-  2 e. RR
172 171 a1i 
 |-  ( ph -> 2 e. RR )
173 56 172 62 leaddsub2d 
 |-  ( ph -> ( ( 3 + 2 ) <_ N <-> 2 <_ ( N - 3 ) ) )
174 170 173 mpbid 
 |-  ( ph -> 2 <_ ( N - 3 ) )
175 174 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 ) )
176 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 ) )
177 79 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 } ) )
178 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
179 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
180 fniniseg 
 |-  ( # Fn _V -> ( u e. ( `' # " { 3 } ) <-> ( u e. _V /\ ( # ` u ) = 3 ) ) )
181 178 179 180 mp2b 
 |-  ( u e. ( `' # " { 3 } ) <-> ( u e. _V /\ ( # ` u ) = 3 ) )
182 181 simprbi 
 |-  ( u e. ( `' # " { 3 } ) -> ( # ` u ) = 3 )
183 177 182 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 )
184 vex 
 |-  u e. _V
185 184 dmex 
 |-  dom u e. _V
186 hashf1rn 
 |-  ( ( dom u e. _V /\ u : dom u -1-1-> D ) -> ( # ` u ) = ( # ` ran u ) )
187 185 87 186 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 ) )
188 183 187 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 ) )
189 176 188 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 ) ) )
190 175 189 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 ) ) )
191 hashssdif 
 |-  ( ( D e. Fin /\ ran u C_ D ) -> ( # ` ( D \ ran u ) ) = ( ( # ` D ) - ( # ` ran u ) ) )
192 19 90 191 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 ) ) )
193 190 192 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 ) ) )
194 hashge2el2dif 
 |-  ( ( ( D \ ran u ) e. _V /\ 2 <_ ( # ` ( D \ ran u ) ) ) -> E. x e. ( D \ ran u ) E. y e. ( D \ ran u ) x =/= y )
195 168 193 194 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 )
196 165 195 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 ) )
197 nfcv 
 |-  F/_ u M
198 5 3 36 tocycf 
 |-  ( D e. Fin -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
199 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 } )
200 9 198 199 3syl 
 |-  ( ph -> M Fn { w e. Word D | w : dom w -1-1-> D } )
201 11 1 eleqtrdi 
 |-  ( ph -> T e. ( M " ( `' # " { 3 } ) ) )
202 197 200 201 fvelimad 
 |-  ( ph -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ( M ` u ) = T )
203 202 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 )
204 196 203 r19.29a 
 |-  ( ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) /\ -. g e. A ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
205 18 204 pm2.61dan 
 |-  ( ( ( ph /\ g e. ( Base ` S ) ) /\ Q = ( ( g .+ T ) .- g ) ) -> E. p e. A Q = ( ( p .+ T ) .- p ) )
206 1 3 4 5 36 6 7 68 9 10 11 cycpmconjs 
 |-  ( ph -> E. g e. ( Base ` S ) Q = ( ( g .+ T ) .- g ) )
207 205 206 r19.29a 
 |-  ( ph -> E. p e. A Q = ( ( p .+ T ) .- p ) )