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 : Base g ⟶ 1-1 onto Base h ∧ ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cismt class Ismt
1 vg setvar g
2 cvv class V
3 vh setvar h
4 vf setvar f
5 4 cv setvar f
6 cbs class Base
7 1 cv setvar g
8 7 6 cfv class Base g
9 3 cv setvar h
10 9 6 cfv class Base h
11 8 10 5 wf1o wff f : Base g ⟶ 1-1 onto Base h
12 va setvar a
13 vb setvar b
14 12 cv setvar a
15 14 5 cfv class f ⁡ a
16 cds class dist
17 9 16 cfv class dist ⁡ h
18 13 cv setvar b
19 18 5 cfv class f ⁡ b
20 15 19 17 co class f ⁡ a dist ⁡ h f ⁡ b
21 7 16 cfv class dist ⁡ g
22 14 18 21 co class a dist ⁡ g b
23 20 22 wceq wff f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
24 23 13 8 wral wff ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
25 24 12 8 wral wff ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
26 11 25 wa wff f : Base g ⟶ 1-1 onto Base h ∧ ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
27 26 4 cab class f | f : Base g ⟶ 1-1 onto Base h ∧ ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
28 1 3 2 2 27 cmpo class g ∈ V , h ∈ V ⟼ f | f : Base g ⟶ 1-1 onto Base h ∧ ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
29 0 28 wceq wff Ismt = g ∈ V , h ∈ V ⟼ f | f : Base g ⟶ 1-1 onto Base h ∧ ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b