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 25146
Description: Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 25147. (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 25145 . 2 class Ismt
2 vg . . 3 setvar 𝑔
3 vh . . 3 setvar
4 cvv 3172 . . 3 class V
52cv 1473 . . . . . . 7 class 𝑔
6 cbs 15641 . . . . . . 7 class Base
75, 6cfv 5790 . . . . . 6 class (Base‘𝑔)
83cv 1473 . . . . . . 7 class
98, 6cfv 5790 . . . . . 6 class (Base‘)
10 vf . . . . . . 7 setvar 𝑓
1110cv 1473 . . . . . 6 class 𝑓
127, 9, 11wf1o 5789 . . . . 5 wff 𝑓:(Base‘𝑔)–1-1-onto→(Base‘)
13 va . . . . . . . . . . 11 setvar 𝑎
1413cv 1473 . . . . . . . . . 10 class 𝑎
1514, 11cfv 5790 . . . . . . . . 9 class (𝑓𝑎)
16 vb . . . . . . . . . . 11 setvar 𝑏
1716cv 1473 . . . . . . . . . 10 class 𝑏
1817, 11cfv 5790 . . . . . . . . 9 class (𝑓𝑏)
19 cds 15723 . . . . . . . . . 10 class dist
208, 19cfv 5790 . . . . . . . . 9 class (dist‘)
2115, 18, 20co 6527 . . . . . . . 8 class ((𝑓𝑎)(dist‘)(𝑓𝑏))
225, 19cfv 5790 . . . . . . . . 9 class (dist‘𝑔)
2314, 17, 22co 6527 . . . . . . . 8 class (𝑎(dist‘𝑔)𝑏)
2421, 23wceq 1474 . . . . . . 7 wff ((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2524, 16, 7wral 2895 . . . . . 6 wff 𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2625, 13, 7wral 2895 . . . . 5 wff 𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2712, 26wa 382 . . . 4 wff (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))
2827, 10cab 2595 . . 3 class {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))}
292, 3, 4, 4, 28cmpt2 6529 . 2 class (𝑔 ∈ V, ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))})
301, 29wceq 1474 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  25147
  Copyright terms: Public domain W3C validator