Step |
Hyp |
Ref |
Expression |
1 |
|
cusgrsizeindb0.v |
|- V = ( Vtx ` G ) |
2 |
|
cusgrsizeindb0.e |
|- E = ( Edg ` G ) |
3 |
|
edgval |
|- ( Edg ` G ) = ran ( iEdg ` G ) |
4 |
2 3
|
eqtri |
|- E = ran ( iEdg ` G ) |
5 |
4
|
a1i |
|- ( ( G e. ComplUSGraph /\ V e. Fin ) -> E = ran ( iEdg ` G ) ) |
6 |
5
|
fveq2d |
|- ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` E ) = ( # ` ran ( iEdg ` G ) ) ) |
7 |
1
|
opeq1i |
|- <. V , ( iEdg ` G ) >. = <. ( Vtx ` G ) , ( iEdg ` G ) >. |
8 |
|
cusgrop |
|- ( G e. ComplUSGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplUSGraph ) |
9 |
7 8
|
eqeltrid |
|- ( G e. ComplUSGraph -> <. V , ( iEdg ` G ) >. e. ComplUSGraph ) |
10 |
|
fvex |
|- ( iEdg ` G ) e. _V |
11 |
|
fvex |
|- ( Edg ` <. v , e >. ) e. _V |
12 |
|
rabexg |
|- ( ( Edg ` <. v , e >. ) e. _V -> { c e. ( Edg ` <. v , e >. ) | n e/ c } e. _V ) |
13 |
12
|
resiexd |
|- ( ( Edg ` <. v , e >. ) e. _V -> ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) e. _V ) |
14 |
11 13
|
ax-mp |
|- ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) e. _V |
15 |
|
rneq |
|- ( e = ( iEdg ` G ) -> ran e = ran ( iEdg ` G ) ) |
16 |
15
|
fveq2d |
|- ( e = ( iEdg ` G ) -> ( # ` ran e ) = ( # ` ran ( iEdg ` G ) ) ) |
17 |
|
fveq2 |
|- ( v = V -> ( # ` v ) = ( # ` V ) ) |
18 |
17
|
oveq1d |
|- ( v = V -> ( ( # ` v ) _C 2 ) = ( ( # ` V ) _C 2 ) ) |
19 |
16 18
|
eqeqan12rd |
|- ( ( v = V /\ e = ( iEdg ` G ) ) -> ( ( # ` ran e ) = ( ( # ` v ) _C 2 ) <-> ( # ` ran ( iEdg ` G ) ) = ( ( # ` V ) _C 2 ) ) ) |
20 |
|
rneq |
|- ( e = f -> ran e = ran f ) |
21 |
20
|
fveq2d |
|- ( e = f -> ( # ` ran e ) = ( # ` ran f ) ) |
22 |
|
fveq2 |
|- ( v = w -> ( # ` v ) = ( # ` w ) ) |
23 |
22
|
oveq1d |
|- ( v = w -> ( ( # ` v ) _C 2 ) = ( ( # ` w ) _C 2 ) ) |
24 |
21 23
|
eqeqan12rd |
|- ( ( v = w /\ e = f ) -> ( ( # ` ran e ) = ( ( # ` v ) _C 2 ) <-> ( # ` ran f ) = ( ( # ` w ) _C 2 ) ) ) |
25 |
|
vex |
|- v e. _V |
26 |
|
vex |
|- e e. _V |
27 |
25 26
|
opvtxfvi |
|- ( Vtx ` <. v , e >. ) = v |
28 |
27
|
eqcomi |
|- v = ( Vtx ` <. v , e >. ) |
29 |
|
eqid |
|- ( Edg ` <. v , e >. ) = ( Edg ` <. v , e >. ) |
30 |
|
eqid |
|- { c e. ( Edg ` <. v , e >. ) | n e/ c } = { c e. ( Edg ` <. v , e >. ) | n e/ c } |
31 |
|
eqid |
|- <. ( v \ { n } ) , ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) >. = <. ( v \ { n } ) , ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) >. |
32 |
28 29 30 31
|
cusgrres |
|- ( ( <. v , e >. e. ComplUSGraph /\ n e. v ) -> <. ( v \ { n } ) , ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) >. e. ComplUSGraph ) |
33 |
|
rneq |
|- ( f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) -> ran f = ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) |
34 |
33
|
fveq2d |
|- ( f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) -> ( # ` ran f ) = ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) ) |
35 |
34
|
adantl |
|- ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( # ` ran f ) = ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) ) |
36 |
|
fveq2 |
|- ( w = ( v \ { n } ) -> ( # ` w ) = ( # ` ( v \ { n } ) ) ) |
37 |
36
|
adantr |
|- ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( # ` w ) = ( # ` ( v \ { n } ) ) ) |
38 |
37
|
oveq1d |
|- ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( ( # ` w ) _C 2 ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) |
39 |
35 38
|
eqeq12d |
|- ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( ( # ` ran f ) = ( ( # ` w ) _C 2 ) <-> ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) ) |
40 |
|
edgopval |
|- ( ( v e. _V /\ e e. _V ) -> ( Edg ` <. v , e >. ) = ran e ) |
41 |
40
|
el2v |
|- ( Edg ` <. v , e >. ) = ran e |
42 |
41
|
a1i |
|- ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( Edg ` <. v , e >. ) = ran e ) |
43 |
42
|
eqcomd |
|- ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ran e = ( Edg ` <. v , e >. ) ) |
44 |
43
|
fveq2d |
|- ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( # ` ran e ) = ( # ` ( Edg ` <. v , e >. ) ) ) |
45 |
|
cusgrusgr |
|- ( <. v , e >. e. ComplUSGraph -> <. v , e >. e. USGraph ) |
46 |
|
usgruhgr |
|- ( <. v , e >. e. USGraph -> <. v , e >. e. UHGraph ) |
47 |
45 46
|
syl |
|- ( <. v , e >. e. ComplUSGraph -> <. v , e >. e. UHGraph ) |
48 |
28 29
|
cusgrsizeindb0 |
|- ( ( <. v , e >. e. UHGraph /\ ( # ` v ) = 0 ) -> ( # ` ( Edg ` <. v , e >. ) ) = ( ( # ` v ) _C 2 ) ) |
49 |
47 48
|
sylan |
|- ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( # ` ( Edg ` <. v , e >. ) ) = ( ( # ` v ) _C 2 ) ) |
50 |
44 49
|
eqtrd |
|- ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) ) |
51 |
|
rnresi |
|- ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) = { c e. ( Edg ` <. v , e >. ) | n e/ c } |
52 |
51
|
fveq2i |
|- ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( # ` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) |
53 |
41
|
a1i |
|- ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( Edg ` <. v , e >. ) = ran e ) |
54 |
53
|
rabeqdv |
|- ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> { c e. ( Edg ` <. v , e >. ) | n e/ c } = { c e. ran e | n e/ c } ) |
55 |
54
|
fveq2d |
|- ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( # ` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) = ( # ` { c e. ran e | n e/ c } ) ) |
56 |
52 55
|
syl5eq |
|- ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( # ` { c e. ran e | n e/ c } ) ) |
57 |
56
|
eqeq1d |
|- ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) <-> ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) ) |
58 |
57
|
biimpd |
|- ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) -> ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) ) |
59 |
58
|
imdistani |
|- ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) -> ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) ) |
60 |
41
|
eqcomi |
|- ran e = ( Edg ` <. v , e >. ) |
61 |
|
eqid |
|- { c e. ran e | n e/ c } = { c e. ran e | n e/ c } |
62 |
28 60 61
|
cusgrsize2inds |
|- ( ( y + 1 ) e. NN0 -> ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> ( ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) ) ) ) |
63 |
62
|
imp31 |
|- ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) ) |
64 |
59 63
|
syl |
|- ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) ) |
65 |
10 14 19 24 32 39 50 64
|
opfi1ind |
|- ( ( <. V , ( iEdg ` G ) >. e. ComplUSGraph /\ V e. Fin ) -> ( # ` ran ( iEdg ` G ) ) = ( ( # ` V ) _C 2 ) ) |
66 |
9 65
|
sylan |
|- ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` ran ( iEdg ` G ) ) = ( ( # ` V ) _C 2 ) ) |
67 |
6 66
|
eqtrd |
|- ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) ) |