Step |
Hyp |
Ref |
Expression |
1 |
|
frgrhash2wsp.v |
โข ๐ = ( Vtx โ ๐บ ) |
2 |
|
2nn |
โข 2 โ โ |
3 |
1
|
wspniunwspnon |
โข ( ( 2 โ โ โง ๐บ โ FriendGraph ) โ ( 2 WSPathsN ๐บ ) = โช ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) |
4 |
2 3
|
mpan |
โข ( ๐บ โ FriendGraph โ ( 2 WSPathsN ๐บ ) = โช ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) |
5 |
4
|
fveq2d |
โข ( ๐บ โ FriendGraph โ ( โฏ โ ( 2 WSPathsN ๐บ ) ) = ( โฏ โ โช ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) ) |
6 |
5
|
adantr |
โข ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โ ( โฏ โ ( 2 WSPathsN ๐บ ) ) = ( โฏ โ โช ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) ) |
7 |
|
simpr |
โข ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โ ๐ โ Fin ) |
8 |
|
eqid |
โข ( ๐ โ { ๐ } ) = ( ๐ โ { ๐ } ) |
9 |
1
|
eleq1i |
โข ( ๐ โ Fin โ ( Vtx โ ๐บ ) โ Fin ) |
10 |
|
wspthnonfi |
โข ( ( Vtx โ ๐บ ) โ Fin โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) โ Fin ) |
11 |
9 10
|
sylbi |
โข ( ๐ โ Fin โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) โ Fin ) |
12 |
11
|
adantl |
โข ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) โ Fin ) |
13 |
12
|
3ad2ant1 |
โข ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ โง ๐ โ ( ๐ โ { ๐ } ) ) โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) โ Fin ) |
14 |
|
2wspiundisj |
โข Disj ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) |
15 |
14
|
a1i |
โข ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โ Disj ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) |
16 |
|
2wspdisj |
โข Disj ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) |
17 |
16
|
a1i |
โข ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ ) โ Disj ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) |
18 |
|
simplll |
โข ( ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ ) โง ๐ โ ( ๐ โ { ๐ } ) ) โ ๐บ โ FriendGraph ) |
19 |
|
simpr |
โข ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ ) โ ๐ โ ๐ ) |
20 |
|
eldifi |
โข ( ๐ โ ( ๐ โ { ๐ } ) โ ๐ โ ๐ ) |
21 |
19 20
|
anim12i |
โข ( ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ ) โง ๐ โ ( ๐ โ { ๐ } ) ) โ ( ๐ โ ๐ โง ๐ โ ๐ ) ) |
22 |
|
eldifsni |
โข ( ๐ โ ( ๐ โ { ๐ } ) โ ๐ โ ๐ ) |
23 |
22
|
necomd |
โข ( ๐ โ ( ๐ โ { ๐ } ) โ ๐ โ ๐ ) |
24 |
23
|
adantl |
โข ( ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ ) โง ๐ โ ( ๐ โ { ๐ } ) ) โ ๐ โ ๐ ) |
25 |
1
|
frgr2wsp1 |
โข ( ( ๐บ โ FriendGraph โง ( ๐ โ ๐ โง ๐ โ ๐ ) โง ๐ โ ๐ ) โ ( โฏ โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) = 1 ) |
26 |
18 21 24 25
|
syl3anc |
โข ( ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ ) โง ๐ โ ( ๐ โ { ๐ } ) ) โ ( โฏ โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) = 1 ) |
27 |
26
|
3impa |
โข ( ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โง ๐ โ ๐ โง ๐ โ ( ๐ โ { ๐ } ) ) โ ( โฏ โ ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) = 1 ) |
28 |
7 8 13 15 17 27
|
hash2iun1dif1 |
โข ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โ ( โฏ โ โช ๐ โ ๐ โช ๐ โ ( ๐ โ { ๐ } ) ( ๐ ( 2 WSPathsNOn ๐บ ) ๐ ) ) = ( ( โฏ โ ๐ ) ยท ( ( โฏ โ ๐ ) โ 1 ) ) ) |
29 |
6 28
|
eqtrd |
โข ( ( ๐บ โ FriendGraph โง ๐ โ Fin ) โ ( โฏ โ ( 2 WSPathsN ๐บ ) ) = ( ( โฏ โ ๐ ) ยท ( ( โฏ โ ๐ ) โ 1 ) ) ) |