Metamath Proof Explorer

Theorem rusgr1vtxlem

Description: Lemma for rusgr1vtx . (Contributed by AV, 27-Dec-2020)

Ref Expression
Assertion rusgr1vtxlem 
|- ( ( ( A. v e. V ( # ` A ) = K /\ A. v e. V A = (/) ) /\ ( V e. W /\ ( # ` V ) = 1 ) ) -> K = 0 )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. v e. V ( ( # ` A ) = K /\ A = (/) ) <-> ( A. v e. V ( # ` A ) = K /\ A. v e. V A = (/) ) )
2 fveqeq2 
 |-  ( A = (/) -> ( ( # ` A ) = K <-> ( # ` (/) ) = K ) )
3 2 biimpac 
 |-  ( ( ( # ` A ) = K /\ A = (/) ) -> ( # ` (/) ) = K )
4 3 ralimi 
 |-  ( A. v e. V ( ( # ` A ) = K /\ A = (/) ) -> A. v e. V ( # ` (/) ) = K )
5 hash1n0 
 |-  ( ( V e. W /\ ( # ` V ) = 1 ) -> V =/= (/) )
6 rspn0 
 |-  ( V =/= (/) -> ( A. v e. V ( # ` (/) ) = K -> ( # ` (/) ) = K ) )
7 5 6 syl 
 |-  ( ( V e. W /\ ( # ` V ) = 1 ) -> ( A. v e. V ( # ` (/) ) = K -> ( # ` (/) ) = K ) )
8 hash0 
 |-  ( # ` (/) ) = 0
9 eqeq1 
 |-  ( ( # ` (/) ) = K -> ( ( # ` (/) ) = 0 <-> K = 0 ) )
10 8 9 mpbii 
 |-  ( ( # ` (/) ) = K -> K = 0 )
11 7 10 syl6com 
 |-  ( A. v e. V ( # ` (/) ) = K -> ( ( V e. W /\ ( # ` V ) = 1 ) -> K = 0 ) )
12 4 11 syl 
 |-  ( A. v e. V ( ( # ` A ) = K /\ A = (/) ) -> ( ( V e. W /\ ( # ` V ) = 1 ) -> K = 0 ) )
13 1 12 sylbir 
 |-  ( ( A. v e. V ( # ` A ) = K /\ A. v e. V A = (/) ) -> ( ( V e. W /\ ( # ` V ) = 1 ) -> K = 0 ) )
14 13 imp 
 |-  ( ( ( A. v e. V ( # ` A ) = K /\ A. v e. V A = (/) ) /\ ( V e. W /\ ( # ` V ) = 1 ) ) -> K = 0 )