Theorem resseuf

Description: The Euclidean function is unaffected by structure restriction. (Contributed by Thierry Arnoux, 9-Nov-2026)

	Ref	Expression
Hypotheses	resseuf.h	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
	resseuf.f	⊢ 𝐹 = ( EuclF ‘ 𝐺 )
Assertion	resseuf	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 = ( EuclF ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		resseuf.h	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2		resseuf.f	⊢ 𝐹 = ( EuclF ‘ 𝐺 )
3		eufid	⊢ EuclF = Slot ( EuclF ‘ ndx )
4		basendxneufndx	⊢ ( Base ‘ ndx ) ≠ ( EuclF ‘ ndx )
5	4	necomi	⊢ ( EuclF ‘ ndx ) ≠ ( Base ‘ ndx )
6	1 2 3 5	resseqnbas	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 = ( EuclF ‘ 𝐻 ) )