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