Metamath Proof Explorer

Theorem frrusgrord0lem

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

Ref Expression
Hypothesis frrusgrord0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frrusgrord0lem ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) )

Proof

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