Metamath Proof Explorer


Theorem f1otrgds

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

Ref Expression
Hypotheses f1otrkg.p P=BaseG
f1otrkg.d D=distG
f1otrkg.i I=ItvG
f1otrkg.b B=BaseH
f1otrkg.e E=distH
f1otrkg.j J=ItvH
f1otrkg.f φF:B1-1 ontoP
f1otrkg.1 φeBfBeEf=FeDFf
f1otrkg.2 φeBfBgBgeJfFgFeIFf
f1otrgitv.x φXB
f1otrgitv.y φYB
Assertion f1otrgds φXEY=FXDFY

Proof

Step Hyp Ref Expression
1 f1otrkg.p P=BaseG
2 f1otrkg.d D=distG
3 f1otrkg.i I=ItvG
4 f1otrkg.b B=BaseH
5 f1otrkg.e E=distH
6 f1otrkg.j J=ItvH
7 f1otrkg.f φF:B1-1 ontoP
8 f1otrkg.1 φeBfBeEf=FeDFf
9 f1otrkg.2 φeBfBgBgeJfFgFeIFf
10 f1otrgitv.x φXB
11 f1otrgitv.y φYB
12 8 ralrimivva φeBfBeEf=FeDFf
13 oveq1 e=XeEf=XEf
14 fveq2 e=XFe=FX
15 14 oveq1d e=XFeDFf=FXDFf
16 13 15 eqeq12d e=XeEf=FeDFfXEf=FXDFf
17 oveq2 f=YXEf=XEY
18 fveq2 f=YFf=FY
19 18 oveq2d f=YFXDFf=FXDFY
20 17 19 eqeq12d f=YXEf=FXDFfXEY=FXDFY
21 16 20 rspc2v XBYBeBfBeEf=FeDFfXEY=FXDFY
22 10 11 21 syl2anc φeBfBeEf=FeDFfXEY=FXDFY
23 12 22 mpd φXEY=FXDFY