Metamath Proof Explorer


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 ) )