MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ismt Structured version   Visualization version   GIF version

Definition df-ismt 25649
Description: Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 25650. (Contributed by Thierry Arnoux, 13-Dec-2019.)
Assertion
Ref Expression
df-ismt Ismt = (𝑔 ∈ V, ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))})
Distinct variable group:   𝑎,𝑏,𝑓,𝑔,

Detailed syntax breakdown of Definition df-ismt
StepHypRef Expression
1 cismt 25648 . 2 class Ismt
2 vg . . 3 setvar 𝑔
3 vh . . 3 setvar
4 cvv 3341 . . 3 class V
52cv 1631 . . . . . . 7 class 𝑔
6 cbs 16080 . . . . . . 7 class Base
75, 6cfv 6050 . . . . . 6 class (Base‘𝑔)
83cv 1631 . . . . . . 7 class
98, 6cfv 6050 . . . . . 6 class (Base‘)
10 vf . . . . . . 7 setvar 𝑓
1110cv 1631 . . . . . 6 class 𝑓
127, 9, 11wf1o 6049 . . . . 5 wff 𝑓:(Base‘𝑔)–1-1-onto→(Base‘)
13 va . . . . . . . . . . 11 setvar 𝑎
1413cv 1631 . . . . . . . . . 10 class 𝑎
1514, 11cfv 6050 . . . . . . . . 9 class (𝑓𝑎)
16 vb . . . . . . . . . . 11 setvar 𝑏
1716cv 1631 . . . . . . . . . 10 class 𝑏
1817, 11cfv 6050 . . . . . . . . 9 class (𝑓𝑏)
19 cds 16173 . . . . . . . . . 10 class dist
208, 19cfv 6050 . . . . . . . . 9 class (dist‘)
2115, 18, 20co 6815 . . . . . . . 8 class ((𝑓𝑎)(dist‘)(𝑓𝑏))
225, 19cfv 6050 . . . . . . . . 9 class (dist‘𝑔)
2314, 17, 22co 6815 . . . . . . . 8 class (𝑎(dist‘𝑔)𝑏)
2421, 23wceq 1632 . . . . . . 7 wff ((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2524, 16, 7wral 3051 . . . . . 6 wff 𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2625, 13, 7wral 3051 . . . . 5 wff 𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2712, 26wa 383 . . . 4 wff (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))
2827, 10cab 2747 . . 3 class {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))}
292, 3, 4, 4, 28cmpt2 6817 . 2 class (𝑔 ∈ V, ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))})
301, 29wceq 1632 1 wff Ismt = (𝑔 ∈ V, ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))})
Colors of variables: wff setvar class
This definition is referenced by:  isismt  25650
  Copyright terms: Public domain W3C validator