Metamath Proof Explorer

Theorem frrusgrord0lem

Description: Lemma for frrusgrord0 . (Contributed by AV, 12-Jan-2022)

Ref Expression
Hypothesis frrusgrord0.v ⊢ V = Vtx ⁡ G
Assertion frrusgrord0lem ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0

Proof

Step Hyp Ref Expression
1 frrusgrord0.v ⊢ V = Vtx ⁡ G
2 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
3 2 anim1i ⊢ G ∈ FriendGraph ∧ V ∈ Fin → G ∈ USGraph ∧ V ∈ Fin
4 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin
5 3 4 sylibr ⊢ G ∈ FriendGraph ∧ V ∈ Fin → G ∈ FinUSGraph
6 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
7 1 6 fusgrregdegfi ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℕ 0
8 5 7 stoic3 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℕ 0
9 8 imp ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℕ 0
10 9 nn0cnd ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℂ
11 hashcl ⊢ V ∈ Fin → V ∈ ℕ 0
12 11 nn0cnd ⊢ V ∈ Fin → V ∈ ℂ
13 12 3ad2ant2 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → V ∈ ℂ
14 13 adantr ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V ∈ ℂ
15 hasheq0 ⊢ V ∈ Fin → V = 0 ↔ V = ∅
16 15 biimpd ⊢ V ∈ Fin → V = 0 → V = ∅
17 16 necon3d ⊢ V ∈ Fin → V ≠ ∅ → V ≠ 0
18 17 imp ⊢ V ∈ Fin ∧ V ≠ ∅ → V ≠ 0
19 18 3adant1 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → V ≠ 0
20 19 adantr ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V ≠ 0
21 10 14 20 3jca ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0