Metamath Proof Explorer

Theorem cycpmco2lem1

Description: Lemma for cycpmco2 . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c 
|- M = ( toCyc ` D )
cycpmco2.s 
|- S = ( SymGrp ` D )
cycpmco2.d 
|- ( ph -> D e. V )
cycpmco2.w 
|- ( ph -> W e. dom M )
cycpmco2.i 
|- ( ph -> I e. ( D \ ran W ) )
cycpmco2.j 
|- ( ph -> J e. ran W )
cycpmco2.e 
|- E = ( ( `' W ` J ) + 1 )
cycpmco2.1 
|- U = ( W splice <. E , E , <" I "> >. )
Assertion cycpmco2lem1 
|- ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` W ) ` J ) )

Proof

Step Hyp Ref Expression
1 cycpmco2.c 
 |-  M = ( toCyc ` D )
2 cycpmco2.s 
 |-  S = ( SymGrp ` D )
3 cycpmco2.d 
 |-  ( ph -> D e. V )
4 cycpmco2.w 
 |-  ( ph -> W e. dom M )
5 cycpmco2.i 
 |-  ( ph -> I e. ( D \ ran W ) )
6 cycpmco2.j 
 |-  ( ph -> J e. ran W )
7 cycpmco2.e 
 |-  E = ( ( `' W ` J ) + 1 )
8 cycpmco2.1 
 |-  U = ( W splice <. E , E , <" I "> >. )
9 5 eldifad 
 |-  ( ph -> I e. D )
10 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
11 eqid 
 |-  ( Base ` S ) = ( Base ` S )
12 1 2 11 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
13 3 12 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
14 13 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
15 4 14 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
16 10 15 sselid 
 |-  ( ph -> W e. Word D )
17 id 
 |-  ( w = W -> w = W )
18 dmeq 
 |-  ( w = W -> dom w = dom W )
19 eqidd 
 |-  ( w = W -> D = D )
20 17 18 19 f1eq123d 
 |-  ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
21 20 elrab3 
 |-  ( W e. Word D -> ( W e. { w e. Word D | w : dom w -1-1-> D } <-> W : dom W -1-1-> D ) )
22 21 biimpa 
 |-  ( ( W e. Word D /\ W e. { w e. Word D | w : dom w -1-1-> D } ) -> W : dom W -1-1-> D )
23 16 15 22 syl2anc 
 |-  ( ph -> W : dom W -1-1-> D )
24 f1f 
 |-  ( W : dom W -1-1-> D -> W : dom W --> D )
25 23 24 syl 
 |-  ( ph -> W : dom W --> D )
26 25 frnd 
 |-  ( ph -> ran W C_ D )
27 26 6 sseldd 
 |-  ( ph -> J e. D )
28 5 eldifbd 
 |-  ( ph -> -. I e. ran W )
29 nelne2 
 |-  ( ( J e. ran W /\ -. I e. ran W ) -> J =/= I )
30 6 28 29 syl2anc 
 |-  ( ph -> J =/= I )
31 30 necomd 
 |-  ( ph -> I =/= J )
32 1 3 9 27 31 2 cyc2fv1 
 |-  ( ph -> ( ( M ` <" I J "> ) ` I ) = J )
33 32 fveq2d 
 |-  ( ph -> ( ( M ` W ) ` ( ( M ` <" I J "> ) ` I ) ) = ( ( M ` W ) ` J ) )