Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdgval.v |
|- V = ( Vtx ` G ) |
2 |
|
vtxdgval.i |
|- I = ( iEdg ` G ) |
3 |
|
vtxdgval.a |
|- A = dom I |
4 |
1 2 3
|
vtxdgval |
|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) ) |
5 |
4
|
adantl |
|- ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) ) |
6 |
|
rabfi |
|- ( A e. Fin -> { x e. A | U e. ( I ` x ) } e. Fin ) |
7 |
|
hashcl |
|- ( { x e. A | U e. ( I ` x ) } e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0 ) |
8 |
6 7
|
syl |
|- ( A e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0 ) |
9 |
8
|
nn0red |
|- ( A e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. RR ) |
10 |
|
rabfi |
|- ( A e. Fin -> { x e. A | ( I ` x ) = { U } } e. Fin ) |
11 |
|
hashcl |
|- ( { x e. A | ( I ` x ) = { U } } e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. NN0 ) |
12 |
10 11
|
syl |
|- ( A e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. NN0 ) |
13 |
12
|
nn0red |
|- ( A e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) |
14 |
9 13
|
jca |
|- ( A e. Fin -> ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR /\ ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) ) |
15 |
14
|
adantr |
|- ( ( A e. Fin /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR /\ ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) ) |
16 |
|
rexadd |
|- ( ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR /\ ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) ) |
17 |
15 16
|
syl |
|- ( ( A e. Fin /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) ) |
18 |
5 17
|
eqtrd |
|- ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) ) |