Metamath Proof Explorer


Theorem finsumvtxdg2ssteplem1

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 15-Dec-2021)

Ref Expression
Hypotheses finsumvtxdg2sstep.v 𝑉 = ( Vtx ‘ 𝐺 )
finsumvtxdg2sstep.e 𝐸 = ( iEdg ‘ 𝐺 )
finsumvtxdg2sstep.k 𝐾 = ( 𝑉 ∖ { 𝑁 } )
finsumvtxdg2sstep.i 𝐼 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
finsumvtxdg2sstep.p 𝑃 = ( 𝐸𝐼 )
finsumvtxdg2sstep.s 𝑆 = ⟨ 𝐾 , 𝑃
finsumvtxdg2ssteplem.j 𝐽 = { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) }
Assertion finsumvtxdg2ssteplem1 ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 finsumvtxdg2sstep.v 𝑉 = ( Vtx ‘ 𝐺 )
2 finsumvtxdg2sstep.e 𝐸 = ( iEdg ‘ 𝐺 )
3 finsumvtxdg2sstep.k 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4 finsumvtxdg2sstep.i 𝐼 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
5 finsumvtxdg2sstep.p 𝑃 = ( 𝐸𝐼 )
6 finsumvtxdg2sstep.s 𝑆 = ⟨ 𝐾 , 𝑃
7 finsumvtxdg2ssteplem.j 𝐽 = { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) }
8 upgruhgr ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
9 2 uhgrfun ( 𝐺 ∈ UHGraph → Fun 𝐸 )
10 8 9 syl ( 𝐺 ∈ UPGraph → Fun 𝐸 )
11 10 ad2antrr ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Fun 𝐸 )
12 simprr ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝐸 ∈ Fin )
13 4 ssrab3 𝐼 ⊆ dom 𝐸
14 13 a1i ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝐼 ⊆ dom 𝐸 )
15 hashreshashfun ( ( Fun 𝐸𝐸 ∈ Fin ∧ 𝐼 ⊆ dom 𝐸 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ ( 𝐸𝐼 ) ) + ( ♯ ‘ ( dom 𝐸𝐼 ) ) ) )
16 11 12 14 15 syl3anc ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ ( 𝐸𝐼 ) ) + ( ♯ ‘ ( dom 𝐸𝐼 ) ) ) )
17 5 eqcomi ( 𝐸𝐼 ) = 𝑃
18 17 fveq2i ( ♯ ‘ ( 𝐸𝐼 ) ) = ( ♯ ‘ 𝑃 )
19 18 a1i ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ ( 𝐸𝐼 ) ) = ( ♯ ‘ 𝑃 ) )
20 notrab ( dom 𝐸 ∖ { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) } ) = { 𝑖 ∈ dom 𝐸 ∣ ¬ 𝑁 ∉ ( 𝐸𝑖 ) }
21 4 difeq2i ( dom 𝐸𝐼 ) = ( dom 𝐸 ∖ { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) } )
22 nnel ( ¬ 𝑁 ∉ ( 𝐸𝑖 ) ↔ 𝑁 ∈ ( 𝐸𝑖 ) )
23 22 bicomi ( 𝑁 ∈ ( 𝐸𝑖 ) ↔ ¬ 𝑁 ∉ ( 𝐸𝑖 ) )
24 23 rabbii { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } = { 𝑖 ∈ dom 𝐸 ∣ ¬ 𝑁 ∉ ( 𝐸𝑖 ) }
25 7 24 eqtri 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ ¬ 𝑁 ∉ ( 𝐸𝑖 ) }
26 20 21 25 3eqtr4i ( dom 𝐸𝐼 ) = 𝐽
27 26 a1i ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( dom 𝐸𝐼 ) = 𝐽 )
28 27 fveq2d ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ ( dom 𝐸𝐼 ) ) = ( ♯ ‘ 𝐽 ) )
29 19 28 oveq12d ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ♯ ‘ ( 𝐸𝐼 ) ) + ( ♯ ‘ ( dom 𝐸𝐼 ) ) ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) )
30 16 29 eqtrd ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) )