Metamath Proof Explorer


Theorem 1to3vfriswmgr

Description: Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v V = Vtx G
3vfriswmgr.e E = Edg G
Assertion 1to3vfriswmgr A X V = A V = A B V = A B C G FriendGraph h V v V h v h E ∃! w V h v w E

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v V = Vtx G
2 3vfriswmgr.e E = Edg G
3 df-3or V = A V = A B V = A B C V = A V = A B V = A B C
4 1 2 1to2vfriswmgr A X V = A V = A B G FriendGraph h V v V h v h E ∃! w V h v w E
5 4 expcom V = A V = A B A X G FriendGraph h V v V h v h E ∃! w V h v w E
6 tppreq3 B = C A B C = A B
7 6 eqeq2d B = C V = A B C V = A B
8 olc V = A B V = A V = A B
9 8 anim1ci V = A B A X A X V = A V = A B
10 9 4 syl V = A B A X G FriendGraph h V v V h v h E ∃! w V h v w E
11 10 ex V = A B A X G FriendGraph h V v V h v h E ∃! w V h v w E
12 7 11 syl6bi B = C V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
13 tpprceq3 ¬ B V B A C A B = C A
14 tprot C A B = A B C
15 14 eqeq1i C A B = C A A B C = C A
16 15 biimpi C A B = C A A B C = C A
17 prcom C A = A C
18 16 17 syl6eq C A B = C A A B C = A C
19 18 eqeq2d C A B = C A V = A B C V = A C
20 olc V = A C V = A V = A C
21 1 2 1to2vfriswmgr A X V = A V = A C G FriendGraph h V v V h v h E ∃! w V h v w E
22 20 21 sylan2 A X V = A C G FriendGraph h V v V h v h E ∃! w V h v w E
23 22 expcom V = A C A X G FriendGraph h V v V h v h E ∃! w V h v w E
24 19 23 syl6bi C A B = C A V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
25 13 24 syl ¬ B V B A V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
26 25 a1d ¬ B V B A B C V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
27 tpprceq3 ¬ C V C A B A C = B A
28 tpcoma B A C = A B C
29 28 eqeq1i B A C = B A A B C = B A
30 29 biimpi B A C = B A A B C = B A
31 prcom B A = A B
32 30 31 syl6eq B A C = B A A B C = A B
33 32 eqeq2d B A C = B A V = A B C V = A B
34 8 4 sylan2 A X V = A B G FriendGraph h V v V h v h E ∃! w V h v w E
35 34 expcom V = A B A X G FriendGraph h V v V h v h E ∃! w V h v w E
36 35 a1d V = A B B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
37 33 36 syl6bi B A C = B A V = A B C B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
38 27 37 syl ¬ C V C A V = A B C B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
39 38 com23 ¬ C V C A B C V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
40 simpl B V B A B V
41 simpl C V C A C V
42 40 41 anim12i B V B A C V C A B V C V
43 42 ad2antrr B V B A C V C A B C V = A B C B V C V
44 43 anim1ci B V B A C V C A B C V = A B C A X A X B V C V
45 3anass A X B V C V A X B V C V
46 44 45 sylibr B V B A C V C A B C V = A B C A X A X B V C V
47 simpr B V B A B A
48 47 necomd B V B A A B
49 simpr C V C A C A
50 49 necomd C V C A A C
51 48 50 anim12i B V B A C V C A A B A C
52 51 anim1i B V B A C V C A B C A B A C B C
53 df-3an A B A C B C A B A C B C
54 52 53 sylibr B V B A C V C A B C A B A C B C
55 54 ad2antrr B V B A C V C A B C V = A B C A X A B A C B C
56 simplr B V B A C V C A B C V = A B C A X V = A B C
57 1 2 3vfriswmgr A X B V C V A B A C B C V = A B C G FriendGraph h V v V h v h E ∃! w V h v w E
58 46 55 56 57 syl3anc B V B A C V C A B C V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
59 58 exp41 B V B A C V C A B C V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
60 26 39 59 ecase B C V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
61 12 60 pm2.61ine V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
62 5 61 jaoi V = A V = A B V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
63 3 62 sylbi V = A V = A B V = A B C A X G FriendGraph h V v V h v h E ∃! w V h v w E
64 63 impcom A X V = A V = A B V = A B C G FriendGraph h V v V h v h E ∃! w V h v w E