Metamath Proof Explorer

Theorem upgrimwlklem3

Description: Lemma 3 for upgrimwlk . (Contributed by AV, 25-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i 
|- I = ( iEdg ` G )
upgrimwlk.j 
|- J = ( iEdg ` H )
upgrimwlk.g 
|- ( ph -> G e. USPGraph )
upgrimwlk.h 
|- ( ph -> H e. USPGraph )
upgrimwlk.n 
|- ( ph -> N e. ( G GraphIso H ) )
upgrimwlk.e 
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
upgrimwlk.f 
|- ( ph -> F e. Word dom I )
Assertion upgrimwlklem3 
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` X ) ) = ( N " ( I ` ( F ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 upgrimwlk.i 
 |-  I = ( iEdg ` G )
2 upgrimwlk.j 
 |-  J = ( iEdg ` H )
3 upgrimwlk.g 
 |-  ( ph -> G e. USPGraph )
4 upgrimwlk.h 
 |-  ( ph -> H e. USPGraph )
5 upgrimwlk.n 
 |-  ( ph -> N e. ( G GraphIso H ) )
6 upgrimwlk.e 
 |-  E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
7 upgrimwlk.f 
 |-  ( ph -> F e. Word dom I )
8 6 a1i 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) )
9 2fveq3 
 |-  ( x = X -> ( I ` ( F ` x ) ) = ( I ` ( F ` X ) ) )
10 9 imaeq2d 
 |-  ( x = X -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` X ) ) ) )
11 10 fveq2d 
 |-  ( x = X -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) )
12 11 adantl 
 |-  ( ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) /\ x = X ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) )
13 1 2 3 4 5 6 7 upgrimwlklem1 
 |-  ( ph -> ( # ` E ) = ( # ` F ) )
14 13 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` E ) ) = ( 0 ..^ ( # ` F ) ) )
15 wrdf 
 |-  ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
16 fdm 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
17 16 eqcomd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( 0 ..^ ( # ` F ) ) = dom F )
18 15 17 syl 
 |-  ( F e. Word dom I -> ( 0 ..^ ( # ` F ) ) = dom F )
19 7 18 syl 
 |-  ( ph -> ( 0 ..^ ( # ` F ) ) = dom F )
20 14 19 eqtrd 
 |-  ( ph -> ( 0 ..^ ( # ` E ) ) = dom F )
21 20 eleq2d 
 |-  ( ph -> ( X e. ( 0 ..^ ( # ` E ) ) <-> X e. dom F ) )
22 21 biimpa 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> X e. dom F )
23 fvexd 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) e. _V )
24 8 12 22 23 fvmptd 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( E ` X ) = ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) )
25 24 fveq2d 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` X ) ) = ( J ` ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) )
26 4 adantr 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> H e. USPGraph )
27 2 uspgrf1oedg 
 |-  ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) )
28 26 27 syl 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
29 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
30 3 29 syl 
 |-  ( ph -> G e. UHGraph )
31 uspgruhgr 
 |-  ( H e. USPGraph -> H e. UHGraph )
32 4 31 syl 
 |-  ( ph -> H e. UHGraph )
33 30 32 jca 
 |-  ( ph -> ( G e. UHGraph /\ H e. UHGraph ) )
34 33 adantr 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( G e. UHGraph /\ H e. UHGraph ) )
35 5 adantr 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> N e. ( G GraphIso H ) )
36 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
37 30 36 syl 
 |-  ( ph -> Fun I )
38 37 adantr 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> Fun I )
39 13 7 wrdfd 
 |-  ( ph -> F : ( 0 ..^ ( # ` E ) ) --> dom I )
40 39 ffvelcdmda 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( F ` X ) e. dom I )
41 1 iedgedg 
 |-  ( ( Fun I /\ ( F ` X ) e. dom I ) -> ( I ` ( F ` X ) ) e. ( Edg ` G ) )
42 38 40 41 syl2anc 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( I ` ( F ` X ) ) e. ( Edg ` G ) )
43 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
44 eqid 
 |-  ( Edg ` H ) = ( Edg ` H )
45 43 44 uhgrimedgi 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ ( N e. ( G GraphIso H ) /\ ( I ` ( F ` X ) ) e. ( Edg ` G ) ) ) -> ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) )
46 34 35 42 45 syl12anc 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) )
47 f1ocnvfv2 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) ) -> ( J ` ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) = ( N " ( I ` ( F ` X ) ) ) )
48 28 46 47 syl2anc 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) = ( N " ( I ` ( F ` X ) ) ) )
49 25 48 eqtrd 
 |-  ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` X ) ) = ( N " ( I ` ( F ` X ) ) ) )