Theorem vtxdginducedm1lem3

Description: Lemma 3 for vtxdginducedm1 : an edge in the induced subgraph S of a pseudograph G obtained by removing one vertex N . (Contributed by AV, 16-Dec-2021)

	Ref	Expression
Hypotheses	vtxdginducedm1.v	|- V = ( Vtx ` G )
	vtxdginducedm1.e	|- E = ( iEdg ` G )
	vtxdginducedm1.k	|- K = ( V \ { N } )
	vtxdginducedm1.i	|- I = { i e. dom E | N e/ ( E ` i ) }
	vtxdginducedm1.p	|- P = ( E |` I )
	vtxdginducedm1.s	|- S = <. K , P >.
Assertion	vtxdginducedm1lem3	|- ( H e. I -> ( ( iEdg ` S ) ` H ) = ( E ` H ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdginducedm1.v	|- V = ( Vtx ` G )
2		vtxdginducedm1.e	|- E = ( iEdg ` G )
3		vtxdginducedm1.k	|- K = ( V \ { N } )
4		vtxdginducedm1.i	|- I = { i e. dom E | N e/ ( E ` i ) }
5		vtxdginducedm1.p	|- P = ( E |` I )
6		vtxdginducedm1.s	|- S = <. K , P >.
7	1 2 3 4 5 6	vtxdginducedm1lem1	|- ( iEdg ` S ) = P
8	7 5	eqtri	|- ( iEdg ` S ) = ( E |` I )
9	8	fveq1i	|- ( ( iEdg ` S ) ` H ) = ( ( E |` I ) ` H )
10		fvres	|- ( H e. I -> ( ( E |` I ) ` H ) = ( E ` H ) )
11	9 10	syl5eq	|- ( H e. I -> ( ( iEdg ` S ) ` H ) = ( E ` H ) )