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

Definition df-ismt 26334
 Description: Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 26335. (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 26333 . 2 class Ismt
2 vg . . 3 setvar 𝑔
3 vh . . 3 setvar
4 cvv 3480 . . 3 class V
52cv 1537 . . . . . . 7 class 𝑔
6 cbs 16483 . . . . . . 7 class Base
75, 6cfv 6343 . . . . . 6 class (Base‘𝑔)
83cv 1537 . . . . . . 7 class
98, 6cfv 6343 . . . . . 6 class (Base‘)
10 vf . . . . . . 7 setvar 𝑓
1110cv 1537 . . . . . 6 class 𝑓
127, 9, 11wf1o 6342 . . . . 5 wff 𝑓:(Base‘𝑔)–1-1-onto→(Base‘)
13 va . . . . . . . . . . 11 setvar 𝑎
1413cv 1537 . . . . . . . . . 10 class 𝑎
1514, 11cfv 6343 . . . . . . . . 9 class (𝑓𝑎)
16 vb . . . . . . . . . . 11 setvar 𝑏
1716cv 1537 . . . . . . . . . 10 class 𝑏
1817, 11cfv 6343 . . . . . . . . 9 class (𝑓𝑏)
19 cds 16574 . . . . . . . . . 10 class dist
208, 19cfv 6343 . . . . . . . . 9 class (dist‘)
2115, 18, 20co 7149 . . . . . . . 8 class ((𝑓𝑎)(dist‘)(𝑓𝑏))
225, 19cfv 6343 . . . . . . . . 9 class (dist‘𝑔)
2314, 17, 22co 7149 . . . . . . . 8 class (𝑎(dist‘𝑔)𝑏)
2421, 23wceq 1538 . . . . . . 7 wff ((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2524, 16, 7wral 3133 . . . . . 6 wff 𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2625, 13, 7wral 3133 . . . . 5 wff 𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏)
2712, 26wa 399 . . . 4 wff (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))
2827, 10cab 2802 . . 3 class {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))}
292, 3, 4, 4, 28cmpo 7151 . 2 class (𝑔 ∈ V, ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓𝑎)(dist‘)(𝑓𝑏)) = (𝑎(dist‘𝑔)𝑏))})
301, 29wceq 1538 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  26335
 Copyright terms: Public domain W3C validator