finsumvtxdg2ssteplem1

	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 ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) )

Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem1

Proof