Description: The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 17-Dec-2020) (Proof shortened by AV, 21-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | uspgrloopvtx.g | ⊢ 𝐺 = 〈 𝑉 , { 〈 𝐴 , { 𝑁 } 〉 } 〉 | |
Assertion | uspgrloopvd2 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uspgrloopvtx.g | ⊢ 𝐺 = 〈 𝑉 , { 〈 𝐴 , { 𝑁 } 〉 } 〉 | |
2 | 1 | uspgrloopvtx | ⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 ) |
3 | 2 | 3ad2ant1 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( Vtx ‘ 𝐺 ) = 𝑉 ) |
4 | simp2 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → 𝐴 ∈ 𝑋 ) | |
5 | simp3 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 ) | |
6 | 1 | uspgrloopiedg | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , { 𝑁 } 〉 } ) |
7 | 6 | 3adant3 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , { 𝑁 } 〉 } ) |
8 | 3 4 5 7 | 1loopgrvd2 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 ) |