Theorem trlsegvdeglem4

Description: Lemma for trlsegvdeg . (Contributed by AV, 21-Feb-2021)

	Ref	Expression
Hypotheses	trlsegvdeg.v	|- V = ( Vtx ` G )
	trlsegvdeg.i	|- I = ( iEdg ` G )
	trlsegvdeg.f	|- ( ph -> Fun I )
	trlsegvdeg.n	|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
	trlsegvdeg.u	|- ( ph -> U e. V )
	trlsegvdeg.w	|- ( ph -> F ( Trails ` G ) P )
	trlsegvdeg.vx	|- ( ph -> ( Vtx ` X ) = V )
	trlsegvdeg.vy	|- ( ph -> ( Vtx ` Y ) = V )
	trlsegvdeg.vz	|- ( ph -> ( Vtx ` Z ) = V )
	trlsegvdeg.ix	|- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
	trlsegvdeg.iy	|- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
	trlsegvdeg.iz	|- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
Assertion	trlsegvdeglem4	|- ( ph -> dom ( iEdg ` X ) = ( ( F " ( 0 ..^ N ) ) i^i dom I ) )

Proof

Step	Hyp	Ref	Expression
1		trlsegvdeg.v	|- V = ( Vtx ` G )
2		trlsegvdeg.i	|- I = ( iEdg ` G )
3		trlsegvdeg.f	|- ( ph -> Fun I )
4		trlsegvdeg.n	|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5		trlsegvdeg.u	|- ( ph -> U e. V )
6		trlsegvdeg.w	|- ( ph -> F ( Trails ` G ) P )
7		trlsegvdeg.vx	|- ( ph -> ( Vtx ` X ) = V )
8		trlsegvdeg.vy	|- ( ph -> ( Vtx ` Y ) = V )
9		trlsegvdeg.vz	|- ( ph -> ( Vtx ` Z ) = V )
10		trlsegvdeg.ix	|- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
11		trlsegvdeg.iy	|- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
12		trlsegvdeg.iz	|- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
13	10	dmeqd	|- ( ph -> dom ( iEdg ` X ) = dom ( I |` ( F " ( 0 ..^ N ) ) ) )
14		dmres	|- dom ( I |` ( F " ( 0 ..^ N ) ) ) = ( ( F " ( 0 ..^ N ) ) i^i dom I )
15	13 14	eqtrdi	|- ( ph -> dom ( iEdg ` X ) = ( ( F " ( 0 ..^ N ) ) i^i dom I ) )