Metamath Proof Explorer

Definition df-ismt

Description: Define the set of isometries between two structures. Definition 4.8 of Schwabhauser p. 36. See isismt . (Contributed by Thierry Arnoux, 13-Dec-2019)

Ref Expression
Assertion df-ismt ⊢Ismt=g∈V,h∈V⟼f|f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb

Detailed syntax breakdown

Step Hyp Ref Expression
0 cismt classIsmt
1 vg setvarg
2 cvv classV
3 vh setvarh
4 vf setvarf
5 4 cv setvarf
6 cbs classBase
7 1 cv setvarg
8 7 6 cfv classBaseg
9 3 cv setvarh
10 9 6 cfv classBaseh
11 8 10 5 wf1o wfff:Baseg⟶1-1 ontoBaseh
12 va setvara
13 vb setvarb
14 12 cv setvara
15 14 5 cfv classf⁡a
16 cds classdist
17 9 16 cfv classdist⁡h
18 13 cv setvarb
19 18 5 cfv classf⁡b
20 15 19 17 co classf⁡adist⁡hf⁡b
21 7 16 cfv classdist⁡g
22 14 18 21 co classadist⁡gb
23 20 22 wceq wfff⁡adist⁡hf⁡b=adist⁡gb
24 23 13 8 wral wff∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb
25 24 12 8 wral wff∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb
26 11 25 wa wfff:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb
27 26 4 cab classf|f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb
28 1 3 2 2 27 cmpo classg∈V,h∈V⟼f|f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb
29 0 28 wceq wffIsmt=g∈V,h∈V⟼f|f:Baseg⟶1-1 ontoBaseh∧∀a∈Baseg∀b∈Basegf⁡adist⁡hf⁡b=adist⁡gb