Step | Hyp | Ref
| Expression |
1 | | simp3l 1202 |
. . . 4
⢠((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) â ð â ð) |
2 | | eqid 2737 |
. . . . 5
â¢
(Vtxâðº) =
(Vtxâðº) |
3 | 2 | wwlks2onv 28940 |
. . . 4
⢠((ð â ð ⧠âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) |
4 | 1, 3 | sylan 581 |
. . 3
⢠(((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) |
5 | | simp3r 1203 |
. . . . . . . 8
⢠((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) â ð â ð) |
6 | 2 | wwlks2onv 28940 |
. . . . . . . 8
⢠((ð â ð ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â (ðµ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðŽ â (Vtxâðº))) |
7 | 5, 6 | sylan 581 |
. . . . . . 7
⢠(((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â (ðµ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðŽ â (Vtxâðº))) |
8 | | frgrusgr 29247 |
. . . . . . . . . . . . . . 15
⢠(ðº â FriendGraph â ðº â
USGraph) |
9 | | usgrumgr 28172 |
. . . . . . . . . . . . . . 15
⢠(ðº â USGraph â ðº â
UMGraph) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
⢠(ðº â FriendGraph â ðº â
UMGraph) |
11 | 10 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⢠((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) â ðº â UMGraph) |
12 | | simpr3 1197 |
. . . . . . . . . . . . . 14
⢠((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) â ðµ â (Vtxâðº)) |
13 | | simpl 484 |
. . . . . . . . . . . . . 14
⢠((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) â ð â (Vtxâðº)) |
14 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⢠((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) â ðŽ â (Vtxâðº)) |
15 | 12, 13, 14 | 3jca 1129 |
. . . . . . . . . . . . 13
⢠((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) â (ðµ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðŽ â (Vtxâðº))) |
16 | 2 | wwlks2onsym 28945 |
. . . . . . . . . . . . 13
⢠((ðº â UMGraph ⧠(ðµ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðŽ â (Vtxâðº))) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ))) |
17 | 11, 15, 16 | syl2anr 598 |
. . . . . . . . . . . 12
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ))) |
18 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â ðº â FriendGraph ) |
19 | | 3simpb 1150 |
. . . . . . . . . . . . . . 15
⢠((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (ðŽ â (Vtxâðº) ⧠ðµ â (Vtxâðº))) |
20 | 19 | ad2antlr 726 |
. . . . . . . . . . . . . 14
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â (ðŽ â (Vtxâðº) ⧠ðµ â (Vtxâðº))) |
21 | | simpr2 1196 |
. . . . . . . . . . . . . 14
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â ðŽ â ðµ) |
22 | 2 | frgr2wwlkeu 29313 |
. . . . . . . . . . . . . 14
⢠((ðº â FriendGraph ⧠(ðŽ â (Vtxâðº) ⧠ðµ â (Vtxâðº)) ⧠ðŽ â ðµ) â â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) |
23 | 18, 20, 21, 22 | syl3anc 1372 |
. . . . . . . . . . . . 13
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) |
24 | | s3eq2 14766 |
. . . . . . . . . . . . . . . . 17
⢠(ð¥ = ð â âšâðŽð¥ðµââ© = âšâðŽððµââ©) |
25 | 24 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
⢠(ð¥ = ð â (âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ))) |
26 | 25 | riota2 7344 |
. . . . . . . . . . . . . . 15
⢠((ð â (Vtxâðº) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â (â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð)) |
27 | 26 | ad4ant14 751 |
. . . . . . . . . . . . . 14
⢠((((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â (â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð)) |
28 | | simplr2 1217 |
. . . . . . . . . . . . . . . . 17
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â ð â (Vtxâðº)) |
29 | | s3eq2 14766 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð¥ = ð â âšâðŽð¥ðµââ© = âšâðŽððµââ©) |
30 | 29 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
⢠(ð¥ = ð â (âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ))) |
31 | 30 | riota2 7344 |
. . . . . . . . . . . . . . . . 17
⢠((ð â (Vtxâðº) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â (â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð)) |
32 | 28, 31 | sylan 581 |
. . . . . . . . . . . . . . . 16
⢠((((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â (â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð)) |
33 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . 17
â¢
(((â©ð¥
â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð ⧠(â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð) â ð = ð) |
34 | 33 | expcom 415 |
. . . . . . . . . . . . . . . 16
â¢
((â©ð¥
â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð â ((â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð â ð = ð)) |
35 | 32, 34 | syl6bi 253 |
. . . . . . . . . . . . . . 15
⢠((((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ((â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð â ð = ð))) |
36 | 35 | com23 86 |
. . . . . . . . . . . . . 14
⢠((((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â ((â©ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) = ð â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð))) |
37 | 27, 36 | sylbid 239 |
. . . . . . . . . . . . 13
⢠((((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) ⧠â!ð¥ â (Vtxâðº)âšâðŽð¥ðµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð))) |
38 | 23, 37 | mpdan 686 |
. . . . . . . . . . . 12
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð))) |
39 | 17, 38 | sylbid 239 |
. . . . . . . . . . 11
⢠(((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) ⧠(ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð))) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð))) |
40 | 39 | expimpd 455 |
. . . . . . . . . 10
⢠((ð â (Vtxâðº) ⧠(ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº))) â (((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð))) |
41 | 40 | ex 414 |
. . . . . . . . 9
⢠(ð â (Vtxâðº) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð)))) |
42 | 41 | com23 86 |
. . . . . . . 8
⢠(ð â (Vtxâðº) â (((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð)))) |
43 | 42 | 3ad2ant2 1135 |
. . . . . . 7
⢠((ðµ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðŽ â (Vtxâðº)) â (((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð)))) |
44 | 7, 43 | mpcom 38 |
. . . . . 6
⢠(((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð))) |
45 | 44 | ex 414 |
. . . . 5
⢠((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ð = ð)))) |
46 | 45 | com24 95 |
. . . 4
⢠((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) â (âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â ð = ð)))) |
47 | 46 | imp 408 |
. . 3
⢠(((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â ((ðŽ â (Vtxâðº) ⧠ð â (Vtxâðº) ⧠ðµ â (Vtxâðº)) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â ð = ð))) |
48 | 4, 47 | mpd 15 |
. 2
⢠(((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) ⧠âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ)) â (âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ) â ð = ð)) |
49 | 48 | expimpd 455 |
1
⢠((ðº â FriendGraph ⧠ðŽ â ðµ ⧠(ð â ð ⧠ð â ð)) â ((âšâðŽððµââ© â (ðŽ(2 WWalksNOn ðº)ðµ) ⧠âšâðµððŽââ© â (ðµ(2 WWalksNOn ðº)ðŽ)) â ð = ð)) |