Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdlfgrval.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
vtxdlfgrval.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
|
vtxdlfgrval.a |
⊢ 𝐴 = dom 𝐼 |
4 |
|
vtxdlfgrval.d |
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) |
5 |
4
|
fveq1i |
⊢ ( 𝐷 ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) |
6 |
1 2 3
|
vtxdgval |
⊢ ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) ) |
7 |
6
|
adantl |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) ) |
8 |
5 7
|
syl5eq |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) ) |
9 |
|
eqid |
⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } |
10 |
2 3 9
|
lfgrnloop |
⊢ ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } = ∅ ) |
11 |
10
|
adantr |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } = ∅ ) |
12 |
11
|
fveq2d |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) = ( ♯ ‘ ∅ ) ) |
13 |
|
hash0 |
⊢ ( ♯ ‘ ∅ ) = 0 |
14 |
12 13
|
eqtrdi |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) = 0 ) |
15 |
14
|
oveq2d |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 0 ) ) |
16 |
2
|
dmeqi |
⊢ dom 𝐼 = dom ( iEdg ‘ 𝐺 ) |
17 |
3 16
|
eqtri |
⊢ 𝐴 = dom ( iEdg ‘ 𝐺 ) |
18 |
|
fvex |
⊢ ( iEdg ‘ 𝐺 ) ∈ V |
19 |
18
|
dmex |
⊢ dom ( iEdg ‘ 𝐺 ) ∈ V |
20 |
17 19
|
eqeltri |
⊢ 𝐴 ∈ V |
21 |
20
|
rabex |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ∈ V |
22 |
|
hashxnn0 |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ∈ V → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℕ0* ) |
23 |
|
xnn0xr |
⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℕ0* → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ* ) |
24 |
21 22 23
|
mp2b |
⊢ ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ* |
25 |
|
xaddid1 |
⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ* → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 0 ) = ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ) |
26 |
24 25
|
mp1i |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 0 ) = ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ) |
27 |
8 15 26
|
3eqtrd |
⊢ ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ) |