Metamath Proof Explorer


Theorem rusgr1vtxlem

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

Ref Expression
Assertion rusgr1vtxlem vVA=KvVA=VWV=1K=0

Proof

Step Hyp Ref Expression
1 r19.26 vVA=KA=vVA=KvVA=
2 fveqeq2 A=A=K=K
3 2 biimpac A=KA==K
4 3 ralimi vVA=KA=vV=K
5 hash1n0 VWV=1V
6 rspn0 VvV=K=K
7 5 6 syl VWV=1vV=K=K
8 hash0 =0
9 eqeq1 =K=0K=0
10 8 9 mpbii =KK=0
11 7 10 syl6com vV=KVWV=1K=0
12 4 11 syl vVA=KA=VWV=1K=0
13 1 12 sylbir vVA=KvVA=VWV=1K=0
14 13 imp vVA=KvVA=VWV=1K=0