Theorem resseuf

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

	Ref	Expression
Hypotheses	resseuf.h	$$⊢H=G{\upharpoonright }_{𝑠}A$$
	resseuf.f	$$⊢F=\mathrm{EuclF}\left(G\right)$$
Assertion	resseuf	$$⊢A\in V\to F=\mathrm{EuclF}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		resseuf.h	$$⊢H=G{\upharpoonright }_{𝑠}A$$
2		resseuf.f	$$⊢F=\mathrm{EuclF}\left(G\right)$$
3		eufid	$$⊢\mathrm{EuclF}=\mathrm{Slot}\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
4		basendxneufndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
5	4	necomi	$$⊢\mathrm{EuclF}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
6	1 2 3 5	resseqnbas	$$⊢A\in V\to F=\mathrm{EuclF}\left(H\right)$$