Metamath Proof Explorer

Theorem frgrreg

Description: If a finite nonempty friendship graph is K-regular, then K must be 2 (or 0 ). (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 3-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v 
|- V = ( Vtx ` G )
Assertion frgrreg 
|- ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( K = 0 \/ K = 2 ) ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v 
 |-  V = ( Vtx ` G )
2 ancom 
 |-  ( ( V e. Fin /\ V =/= (/) ) <-> ( V =/= (/) /\ V e. Fin ) )
3 ancom 
 |-  ( ( G e. FriendGraph /\ G RegUSGraph K ) <-> ( G RegUSGraph K /\ G e. FriendGraph ) )
4 2 3 anbi12i 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) <-> ( ( V =/= (/) /\ V e. Fin ) /\ ( G RegUSGraph K /\ G e. FriendGraph ) ) )
5 4 biimpi 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( ( V =/= (/) /\ V e. Fin ) /\ ( G RegUSGraph K /\ G e. FriendGraph ) ) )
6 5 ancomd 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) )
7 1 numclwwlk7lem 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> K e. NN0 )
8 6 7 syl 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> K e. NN0 )
9 neanior 
 |-  ( ( K =/= 0 /\ K =/= 2 ) <-> -. ( K = 0 \/ K = 2 ) )
10 nn0re 
 |-  ( K e. NN0 -> K e. RR )
11 1re 
 |-  1 e. RR
12 lenlt 
 |-  ( ( K e. RR /\ 1 e. RR ) -> ( K <_ 1 <-> -. 1 < K ) )
13 10 11 12 sylancl 
 |-  ( K e. NN0 -> ( K <_ 1 <-> -. 1 < K ) )
14 13 adantl 
 |-  ( ( ( K =/= 0 /\ K =/= 2 ) /\ K e. NN0 ) -> ( K <_ 1 <-> -. 1 < K ) )
15 elnnne0 
 |-  ( K e. NN <-> ( K e. NN0 /\ K =/= 0 ) )
16 nnle1eq1 
 |-  ( K e. NN -> ( K <_ 1 <-> K = 1 ) )
17 16 biimpd 
 |-  ( K e. NN -> ( K <_ 1 -> K = 1 ) )
18 15 17 sylbir 
 |-  ( ( K e. NN0 /\ K =/= 0 ) -> ( K <_ 1 -> K = 1 ) )
19 18 a1d 
 |-  ( ( K e. NN0 /\ K =/= 0 ) -> ( K =/= 2 -> ( K <_ 1 -> K = 1 ) ) )
20 19 expimpd 
 |-  ( K e. NN0 -> ( ( K =/= 0 /\ K =/= 2 ) -> ( K <_ 1 -> K = 1 ) ) )
21 20 impcom 
 |-  ( ( ( K =/= 0 /\ K =/= 2 ) /\ K e. NN0 ) -> ( K <_ 1 -> K = 1 ) )
22 14 21 sylbird 
 |-  ( ( ( K =/= 0 /\ K =/= 2 ) /\ K e. NN0 ) -> ( -. 1 < K -> K = 1 ) )
23 1 fveq2i 
 |-  ( # ` V ) = ( # ` ( Vtx ` G ) )
24 23 eqeq1i 
 |-  ( ( # ` V ) = 1 <-> ( # ` ( Vtx ` G ) ) = 1 )
25 24 biimpi 
 |-  ( ( # ` V ) = 1 -> ( # ` ( Vtx ` G ) ) = 1 )
26 simpr 
 |-  ( ( G e. FriendGraph /\ G RegUSGraph K ) -> G RegUSGraph K )
27 26 adantl 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> G RegUSGraph K )
28 rusgr1vtx 
 |-  ( ( ( # ` ( Vtx ` G ) ) = 1 /\ G RegUSGraph K ) -> K = 0 )
29 25 27 28 syl2an 
 |-  ( ( ( # ` V ) = 1 /\ ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) ) -> K = 0 )
30 29 orcd 
 |-  ( ( ( # ` V ) = 1 /\ ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) ) -> ( K = 0 \/ K = 2 ) )
31 30 ex 
 |-  ( ( # ` V ) = 1 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) )
32 31 a1d 
 |-  ( ( # ` V ) = 1 -> ( K = 1 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) )
33 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
34 1 33 rusgrprop0 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) )
35 simp2 
 |-  ( ( -. ( # ` V ) = 1 /\ G e. FriendGraph /\ ( V e. Fin /\ V =/= (/) ) ) -> G e. FriendGraph )
36 hashnncl 
 |-  ( V e. Fin -> ( ( # ` V ) e. NN <-> V =/= (/) ) )
37 df-ne 
 |-  ( ( # ` V ) =/= 1 <-> -. ( # ` V ) = 1 )
38 nngt1ne1 
 |-  ( ( # ` V ) e. NN -> ( 1 < ( # ` V ) <-> ( # ` V ) =/= 1 ) )
39 38 biimprd 
 |-  ( ( # ` V ) e. NN -> ( ( # ` V ) =/= 1 -> 1 < ( # ` V ) ) )
40 37 39 biimtrrid 
 |-  ( ( # ` V ) e. NN -> ( -. ( # ` V ) = 1 -> 1 < ( # ` V ) ) )
41 36 40 biimtrrdi 
 |-  ( V e. Fin -> ( V =/= (/) -> ( -. ( # ` V ) = 1 -> 1 < ( # ` V ) ) ) )
42 41 imp 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( -. ( # ` V ) = 1 -> 1 < ( # ` V ) ) )
43 42 impcom 
 |-  ( ( -. ( # ` V ) = 1 /\ ( V e. Fin /\ V =/= (/) ) ) -> 1 < ( # ` V ) )
44 1 vdgn1frgrv3 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 )
45 35 43 44 3imp3i2an 
 |-  ( ( -. ( # ` V ) = 1 /\ G e. FriendGraph /\ ( V e. Fin /\ V =/= (/) ) ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 )
46 r19.26 
 |-  ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) <-> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) )
47 r19.2z 
 |-  ( ( V =/= (/) /\ A. v e. V ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) ) -> E. v e. V ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) )
48 neeq1 
 |-  ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( ( VtxDeg ` G ) ` v ) =/= 1 <-> K =/= 1 ) )
49 48 biimpd 
 |-  ( ( ( VtxDeg ` G ) ` v ) = K -> ( ( ( VtxDeg ` G ) ` v ) =/= 1 -> K =/= 1 ) )
50 49 impcom 
 |-  ( ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) -> K =/= 1 )
51 eqneqall 
 |-  ( K = 1 -> ( K =/= 1 -> ( K = 0 \/ K = 2 ) ) )
52 51 com12 
 |-  ( K =/= 1 -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) )
53 50 52 syl 
 |-  ( ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) )
54 53 rexlimivw 
 |-  ( E. v e. V ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) )
55 47 54 syl 
 |-  ( ( V =/= (/) /\ A. v e. V ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) ) -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) )
56 55 ex 
 |-  ( V =/= (/) -> ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) =/= 1 /\ ( ( VtxDeg ` G ) ` v ) = K ) -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) ) )
57 46 56 biimtrrid 
 |-  ( V =/= (/) -> ( ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) ) )
58 57 expd 
 |-  ( V =/= (/) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( K = 1 -> ( K = 0 \/ K = 2 ) ) ) ) )
59 58 com34 
 |-  ( V =/= (/) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 -> ( K = 1 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( K = 0 \/ K = 2 ) ) ) ) )
60 59 adantl 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 -> ( K = 1 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( K = 0 \/ K = 2 ) ) ) ) )
61 60 3ad2ant3 
 |-  ( ( -. ( # ` V ) = 1 /\ G e. FriendGraph /\ ( V e. Fin /\ V =/= (/) ) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 1 -> ( K = 1 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( K = 0 \/ K = 2 ) ) ) ) )
62 45 61 mpd 
 |-  ( ( -. ( # ` V ) = 1 /\ G e. FriendGraph /\ ( V e. Fin /\ V =/= (/) ) ) -> ( K = 1 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( K = 0 \/ K = 2 ) ) ) )
63 62 3exp 
 |-  ( -. ( # ` V ) = 1 -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 1 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( K = 0 \/ K = 2 ) ) ) ) ) )
64 63 com15 
 |-  ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 1 -> ( -. ( # ` V ) = 1 -> ( K = 0 \/ K = 2 ) ) ) ) ) )
65 64 3ad2ant3 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 1 -> ( -. ( # ` V ) = 1 -> ( K = 0 \/ K = 2 ) ) ) ) ) )
66 34 65 syl 
 |-  ( G RegUSGraph K -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 1 -> ( -. ( # ` V ) = 1 -> ( K = 0 \/ K = 2 ) ) ) ) ) )
67 66 impcom 
 |-  ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 1 -> ( -. ( # ` V ) = 1 -> ( K = 0 \/ K = 2 ) ) ) ) )
68 67 impcom 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 1 -> ( -. ( # ` V ) = 1 -> ( K = 0 \/ K = 2 ) ) ) )
69 68 com13 
 |-  ( -. ( # ` V ) = 1 -> ( K = 1 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) )
70 32 69 pm2.61i 
 |-  ( K = 1 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) )
71 22 70 syl6 
 |-  ( ( ( K =/= 0 /\ K =/= 2 ) /\ K e. NN0 ) -> ( -. 1 < K -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) )
72 71 ex 
 |-  ( ( K =/= 0 /\ K =/= 2 ) -> ( K e. NN0 -> ( -. 1 < K -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) ) )
73 72 com23 
 |-  ( ( K =/= 0 /\ K =/= 2 ) -> ( -. 1 < K -> ( K e. NN0 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) ) )
74 9 73 sylbir 
 |-  ( -. ( K = 0 \/ K = 2 ) -> ( -. 1 < K -> ( K e. NN0 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) ) )
75 74 impcom 
 |-  ( ( -. 1 < K /\ -. ( K = 0 \/ K = 2 ) ) -> ( K e. NN0 -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) ) )
76 75 com13 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K e. NN0 -> ( ( -. 1 < K /\ -. ( K = 0 \/ K = 2 ) ) -> ( K = 0 \/ K = 2 ) ) ) )
77 8 76 mpd 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( ( -. 1 < K /\ -. ( K = 0 \/ K = 2 ) ) -> ( K = 0 \/ K = 2 ) ) )
78 77 com12 
 |-  ( ( -. 1 < K /\ -. ( K = 0 \/ K = 2 ) ) -> ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) ) )
79 78 exp4b 
 |-  ( -. 1 < K -> ( -. ( K = 0 \/ K = 2 ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( K = 0 \/ K = 2 ) ) ) ) )
80 simprl 
 |-  ( ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> G e. FriendGraph )
81 simpl 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> V e. Fin )
82 81 ad2antlr 
 |-  ( ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> V e. Fin )
83 simpr 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> V =/= (/) )
84 83 ad2antlr 
 |-  ( ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> V =/= (/) )
85 simpl 
 |-  ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) -> 1 < K )
86 85 26 anim12ci 
 |-  ( ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( G RegUSGraph K /\ 1 < K ) )
87 1 frgrreggt1 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( ( G RegUSGraph K /\ 1 < K ) -> K = 2 ) )
88 87 imp 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ ( G RegUSGraph K /\ 1 < K ) ) -> K = 2 )
89 80 82 84 86 88 syl31anc 
 |-  ( ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> K = 2 )
90 89 olcd 
 |-  ( ( ( 1 < K /\ ( V e. Fin /\ V =/= (/) ) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) )
91 90 exp31 
 |-  ( 1 < K -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( K = 0 \/ K = 2 ) ) ) )
92 2a1 
 |-  ( ( K = 0 \/ K = 2 ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( K = 0 \/ K = 2 ) ) ) )
93 79 91 92 pm2.61ii 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( K = 0 \/ K = 2 ) ) )