Step | Hyp | Ref
| Expression |
1 | | wksonproplem.v |
. . . . . 6
⢠ð = (Vtxâðº) |
2 | 1 | fvexi 6906 |
. . . . 5
⢠ð â V |
3 | | wksonproplem.d |
. . . . . 6
⢠ð = (ð â V ⊠(ð â (Vtxâð), ð â (Vtxâð) ⊠{âšð, ð⩠⣠(ð(ð(ðâð)ð)ð ⧠ð(ðâð)ð)})) |
4 | | simp1 1137 |
. . . . . . 7
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â ðº â V) |
5 | | simp2 1138 |
. . . . . . . 8
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â ðŽ â ð) |
6 | 5, 1 | eleqtrdi 2844 |
. . . . . . 7
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â ðŽ â (Vtxâðº)) |
7 | | simp3 1139 |
. . . . . . . 8
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â ðµ â ð) |
8 | 7, 1 | eleqtrdi 2844 |
. . . . . . 7
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â ðµ â (Vtxâðº)) |
9 | 4, 6, 8, 3 | mptmpoopabovd 8068 |
. . . . . 6
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â (ðŽ(ðâðº)ðµ) = {âšð, ð⩠⣠(ð(ðŽ(ðâðº)ðµ)ð ⧠ð(ðâðº)ð)}) |
10 | | fveq2 6892 |
. . . . . . 7
⢠(ð = ðº â (Vtxâð) = (Vtxâðº)) |
11 | 10, 1 | eqtr4di 2791 |
. . . . . 6
⢠(ð = ðº â (Vtxâð) = ð) |
12 | | fveq2 6892 |
. . . . . . . . 9
⢠(ð = ðº â (ðâð) = (ðâðº)) |
13 | 12 | oveqd 7426 |
. . . . . . . 8
⢠(ð = ðº â (ð(ðâð)ð) = (ð(ðâðº)ð)) |
14 | 13 | breqd 5160 |
. . . . . . 7
⢠(ð = ðº â (ð(ð(ðâð)ð)ð â ð(ð(ðâðº)ð)ð)) |
15 | | fveq2 6892 |
. . . . . . . 8
⢠(ð = ðº â (ðâð) = (ðâðº)) |
16 | 15 | breqd 5160 |
. . . . . . 7
⢠(ð = ðº â (ð(ðâð)ð â ð(ðâðº)ð)) |
17 | 14, 16 | anbi12d 632 |
. . . . . 6
⢠(ð = ðº â ((ð(ð(ðâð)ð)ð ⧠ð(ðâð)ð) â (ð(ð(ðâðº)ð)ð ⧠ð(ðâðº)ð))) |
18 | 3, 9, 11, 11, 17 | bropfvvvv 8078 |
. . . . 5
⢠((ð â V ⧠ð â V) â (ð¹(ðŽ(ðâðº)ðµ)ð â (ðº â V ⧠(ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)))) |
19 | 2, 2, 18 | mp2an 691 |
. . . 4
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â (ðº â V ⧠(ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V))) |
20 | | 3anass 1096 |
. . . . . 6
⢠((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) â (ðº â V ⧠(ðŽ â ð ⧠ðµ â ð))) |
21 | 20 | anbi1i 625 |
. . . . 5
⢠(((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) â ((ðº â V ⧠(ðŽ â ð ⧠ðµ â ð)) ⧠(ð¹ â V ⧠ð â V))) |
22 | | df-3an 1090 |
. . . . 5
⢠((ðº â V ⧠(ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) â ((ðº â V ⧠(ðŽ â ð ⧠ðµ â ð)) ⧠(ð¹ â V ⧠ð â V))) |
23 | 21, 22 | bitr4i 278 |
. . . 4
⢠(((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) â (ðº â V ⧠(ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V))) |
24 | 19, 23 | sylibr 233 |
. . 3
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â ((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V))) |
25 | | wksonproplem.b |
. . . . 5
⢠(((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) â (ð¹(ðŽ(ðâðº)ðµ)ð â (ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð))) |
26 | 25 | biimpd 228 |
. . . 4
⢠(((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) â (ð¹(ðŽ(ðâðº)ðµ)ð â (ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð))) |
27 | 26 | imdistani 570 |
. . 3
⢠((((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) ⧠ð¹(ðŽ(ðâðº)ðµ)ð) â (((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) ⧠(ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð))) |
28 | 24, 27 | mpancom 687 |
. 2
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â (((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) ⧠(ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð))) |
29 | | df-3an 1090 |
. 2
⢠(((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V) ⧠(ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð)) â (((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V)) ⧠(ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð))) |
30 | 28, 29 | sylibr 233 |
1
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â ((ðº â V ⧠ðŽ â ð ⧠ðµ â ð) ⧠(ð¹ â V ⧠ð â V) ⧠(ð¹(ðŽ(ðâðº)ðµ)ð ⧠ð¹(ðâðº)ð))) |