Metamath Proof Explorer

Theorem rusgr1vtxlem

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

Ref Expression
Assertion rusgr1vtxlem ⊢ ∀ v ∈ V A = K ∧ ∀ v ∈ V A = ∅ ∧ V ∈ W ∧ V = 1 → K = 0

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ v ∈ V A = K ∧ A = ∅ ↔ ∀ v ∈ V A = K ∧ ∀ v ∈ V A = ∅
2 fveqeq2 ⊢ A = ∅ → A = K ↔ ∅ = K
3 2 biimpac ⊢ A = K ∧ A = ∅ → ∅ = K
4 3 ralimi ⊢ ∀ v ∈ V A = K ∧ A = ∅ → ∀ v ∈ V ∅ = K
5 hash1n0 ⊢ V ∈ W ∧ V = 1 → V ≠ ∅
6 rspn0 ⊢ V ≠ ∅ → ∀ v ∈ V ∅ = K → ∅ = K
7 5 6 syl ⊢ V ∈ W ∧ V = 1 → ∀ v ∈ V ∅ = K → ∅ = K
8 hash0 ⊢ ∅ = 0
9 eqeq1 ⊢ ∅ = K → ∅ = 0 ↔ K = 0
10 8 9 mpbii ⊢ ∅ = K → K = 0
11 7 10 syl6com ⊢ ∀ v ∈ V ∅ = K → V ∈ W ∧ V = 1 → K = 0
12 4 11 syl ⊢ ∀ v ∈ V A = K ∧ A = ∅ → V ∈ W ∧ V = 1 → K = 0
13 1 12 sylbir ⊢ ∀ v ∈ V A = K ∧ ∀ v ∈ V A = ∅ → V ∈ W ∧ V = 1 → K = 0
14 13 imp ⊢ ∀ v ∈ V A = K ∧ ∀ v ∈ V A = ∅ ∧ V ∈ W ∧ V = 1 → K = 0