Metamath Proof Explorer

Theorem isismt

Description: Property of being an isometry. Compare with isismty . (Contributed by Thierry Arnoux, 13-Dec-2019)

Ref Expression
Hypotheses isismt.b ⊢B=BaseG
isismt.p ⊢P=BaseH
isismt.d ⊢D=dist⁡G
isismt.m ⊢-˙=dist⁡H
Assertion isismt ⊢G∈V∧H∈W→F∈GIsmtH↔F:B⟶1-1 ontoP∧∀a∈B∀b∈BF⁡a-˙F⁡b=aDb

Proof

Step Hyp Ref Expression
1 isismt.b ⊢B=BaseG
2 isismt.p ⊢P=BaseH
3 isismt.d ⊢D=dist⁡G
4 isismt.m ⊢-˙=dist⁡H
5 elex ⊢G∈V→G∈V
6 elex ⊢H∈W→H∈V
7 fveq2 ⊢g=G→Baseg=BaseG
8 7 1 eqtr4di ⊢g=G→Baseg=B
9 8 f1oeq2d ⊢g=G→f:Baseg⟶1-1 ontoBaseh↔f:B⟶1-1 ontoBaseh
10 fveq2 ⊢g=G→dist⁡g=dist⁡G
11 10 3 eqtr4di ⊢g=G→dist⁡g=D
12 11 oveqd ⊢g=G→adist⁡gb=aDb
13 12 eqeq2d ⊢g=G→f⁡adist⁡hf⁡b=adist⁡gb↔f⁡adist⁡hf⁡b=aDb
14 8 13 raleqbidv ⊢g=G→∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb↔∀b∈Bf⁡adist⁡hf⁡b=aDb
15 8 14 raleqbidv ⊢g=G→∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb↔∀a∈B∀b∈Bf⁡adist⁡hf⁡b=aDb
16 9 15 anbi12d ⊢g=G→f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb↔f:B⟶1-1 ontoBaseh∧∀a∈B∀b∈Bf⁡adist⁡hf⁡b=aDb
17 16 abbidv ⊢g=G→f|f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb=f|f:B⟶1-1 ontoBaseh∧∀a∈B∀b∈Bf⁡adist⁡hf⁡b=aDb
18 fveq2 ⊢h=H→Baseh=BaseH
19 18 2 eqtr4di ⊢h=H→Baseh=P
20 19 f1oeq3d ⊢h=H→f:B⟶1-1 ontoBaseh↔f:B⟶1-1 ontoP
21 fveq2 ⊢h=H→dist⁡h=dist⁡H
22 21 4 eqtr4di ⊢h=H→dist⁡h=-˙
23 22 oveqd ⊢h=H→f⁡adist⁡hf⁡b=f⁡a-˙f⁡b
24 23 eqeq1d ⊢h=H→f⁡adist⁡hf⁡b=aDb↔f⁡a-˙f⁡b=aDb
25 24 2ralbidv ⊢h=H→∀a∈B∀b∈Bf⁡adist⁡hf⁡b=aDb↔∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb
26 20 25 anbi12d ⊢h=H→f:B⟶1-1 ontoBaseh∧∀a∈B∀b∈Bf⁡adist⁡hf⁡b=aDb↔f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb
27 26 abbidv ⊢h=H→f|f:B⟶1-1 ontoBaseh∧∀a∈B∀b∈Bf⁡adist⁡hf⁡b=aDb=f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb
28 df-ismt ⊢Ismt=g∈V,h∈V⟼f|f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb
29 ovex ⊢PB∈V
30 f1of ⊢f:B⟶1-1 ontoP→f:B⟶P
31 2 fvexi ⊢P∈V
32 1 fvexi ⊢B∈V
33 31 32 elmap ⊢f∈PB↔f:B⟶P
34 30 33 sylibr ⊢f:B⟶1-1 ontoP→f∈PB
35 34 adantr ⊢f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb→f∈PB
36 35 abssi ⊢f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb⊆PB
37 29 36 ssexi ⊢f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb∈V
38 17 27 28 37 ovmpo ⊢G∈V∧H∈V→GIsmtH=f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb
39 5 6 38 syl2an ⊢G∈V∧H∈W→GIsmtH=f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb
40 39 eleq2d ⊢G∈V∧H∈W→F∈GIsmtH↔F∈f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb
41 f1of ⊢F:B⟶1-1 ontoP→F:B⟶P
42 fex ⊢F:B⟶P∧B∈V→F∈V
43 41 32 42 sylancl ⊢F:B⟶1-1 ontoP→F∈V
44 43 adantr ⊢F:B⟶1-1 ontoP∧∀a∈B∀b∈BF⁡a-˙F⁡b=aDb→F∈V
45 f1oeq1 ⊢f=F→f:B⟶1-1 ontoP↔F:B⟶1-1 ontoP
46 fveq1 ⊢f=F→f⁡a=F⁡a
47 fveq1 ⊢f=F→f⁡b=F⁡b
48 46 47 oveq12d ⊢f=F→f⁡a-˙f⁡b=F⁡a-˙F⁡b
49 48 eqeq1d ⊢f=F→f⁡a-˙f⁡b=aDb↔F⁡a-˙F⁡b=aDb
50 49 2ralbidv ⊢f=F→∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb↔∀a∈B∀b∈BF⁡a-˙F⁡b=aDb
51 45 50 anbi12d ⊢f=F→f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb↔F:B⟶1-1 ontoP∧∀a∈B∀b∈BF⁡a-˙F⁡b=aDb
52 44 51 elab3 ⊢F∈f|f:B⟶1-1 ontoP∧∀a∈B∀b∈Bf⁡a-˙f⁡b=aDb↔F:B⟶1-1 ontoP∧∀a∈B∀b∈BF⁡a-˙F⁡b=aDb
53 40 52 bitrdi ⊢G∈V∧H∈W→F∈GIsmtH↔F:B⟶1-1 ontoP∧∀a∈B∀b∈BF⁡a-˙F⁡b=aDb