Theorem f1otrgds

Description: Convenient lemma for f1otrg . (Contributed by Thierry Arnoux, 19-Mar-2019)

	Ref	Expression
Hypotheses	f1otrkg.p	|- P = ( Base ` G )
	f1otrkg.d	|- D = ( dist ` G )
	f1otrkg.i	|- I = ( Itv ` G )
	f1otrkg.b	|- B = ( Base ` H )
	f1otrkg.e	|- E = ( dist ` H )
	f1otrkg.j	|- J = ( Itv ` H )
	f1otrkg.f	|- ( ph -> F : B -1-1-onto-> P )
	f1otrkg.1	|- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
	f1otrkg.2	|- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
	f1otrgitv.x	|- ( ph -> X e. B )
	f1otrgitv.y	|- ( ph -> Y e. B )
Assertion	f1otrgds	|- ( ph -> ( X E Y ) = ( ( F ` X ) D ( F ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		f1otrkg.p	|- P = ( Base ` G )
2		f1otrkg.d	|- D = ( dist ` G )
3		f1otrkg.i	|- I = ( Itv ` G )
4		f1otrkg.b	|- B = ( Base ` H )
5		f1otrkg.e	|- E = ( dist ` H )
6		f1otrkg.j	|- J = ( Itv ` H )
7		f1otrkg.f	|- ( ph -> F : B -1-1-onto-> P )
8		f1otrkg.1	|- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
9		f1otrkg.2	|- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
10		f1otrgitv.x	|- ( ph -> X e. B )
11		f1otrgitv.y	|- ( ph -> Y e. B )
12	8	ralrimivva	|- ( ph -> A. e e. B A. f e. B ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
13		oveq1	|- ( e = X -> ( e E f ) = ( X E f ) )
14		fveq2	|- ( e = X -> ( F ` e ) = ( F ` X ) )
15	14	oveq1d	|- ( e = X -> ( ( F ` e ) D ( F ` f ) ) = ( ( F ` X ) D ( F ` f ) ) )
16	13 15	eqeq12d	|- ( e = X -> ( ( e E f ) = ( ( F ` e ) D ( F ` f ) ) <-> ( X E f ) = ( ( F ` X ) D ( F ` f ) ) ) )
17		oveq2	|- ( f = Y -> ( X E f ) = ( X E Y ) )
18		fveq2	|- ( f = Y -> ( F ` f ) = ( F ` Y ) )
19	18	oveq2d	|- ( f = Y -> ( ( F ` X ) D ( F ` f ) ) = ( ( F ` X ) D ( F ` Y ) ) )
20	17 19	eqeq12d	|- ( f = Y -> ( ( X E f ) = ( ( F ` X ) D ( F ` f ) ) <-> ( X E Y ) = ( ( F ` X ) D ( F ` Y ) ) ) )
21	16 20	rspc2v	|- ( ( X e. B /\ Y e. B ) -> ( A. e e. B A. f e. B ( e E f ) = ( ( F ` e ) D ( F ` f ) ) -> ( X E Y ) = ( ( F ` X ) D ( F ` Y ) ) ) )
22	10 11 21	syl2anc	|- ( ph -> ( A. e e. B A. f e. B ( e E f ) = ( ( F ` e ) D ( F ` f ) ) -> ( X E Y ) = ( ( F ` X ) D ( F ` Y ) ) ) )
23	12 22	mpd	|- ( ph -> ( X E Y ) = ( ( F ` X ) D ( F ` Y ) ) )