Definition df-ismt 27815

Description: Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 27816. (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

Step	Hyp	Ref	Expression
1		cismt 27814	. 2 class Ismt
2		vg	. . 3 setvar 𝑔
3		vh	. . 3 setvar ℎ
4		cvv 3475	. . 3 class V
5	2	cv 1541	. . . . . . 7 class 𝑔
6		cbs 17144	. . . . . . 7 class Base
7	5, 6	cfv 6544	. . . . . 6 class (Base‘𝑔)
8	3	cv 1541	. . . . . . 7 class ℎ
9	8, 6	cfv 6544	. . . . . 6 class (Base‘ℎ)
10		vf	. . . . . . 7 setvar 𝑓
11	10	cv 1541	. . . . . 6 class 𝑓
12	7, 9, 11	wf1o 6543	. . . . 5 wff 𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ)
13		va	. . . . . . . . . . 11 setvar 𝑎
14	13	cv 1541	. . . . . . . . . 10 class 𝑎
15	14, 11	cfv 6544	. . . . . . . . 9 class (𝑓‘𝑎)
16		vb	. . . . . . . . . . 11 setvar 𝑏
17	16	cv 1541	. . . . . . . . . 10 class 𝑏
18	17, 11	cfv 6544	. . . . . . . . 9 class (𝑓‘𝑏)
19		cds 17206	. . . . . . . . . 10 class dist
20	8, 19	cfv 6544	. . . . . . . . 9 class (dist‘ℎ)
21	15, 18, 20	co 7409	. . . . . . . 8 class ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏))
22	5, 19	cfv 6544	. . . . . . . . 9 class (dist‘𝑔)
23	14, 17, 22	co 7409	. . . . . . . 8 class (𝑎(dist‘𝑔)𝑏)
24	21, 23	wceq 1542	. . . . . . 7 wff ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏)
25	24, 16, 7	wral 3062	. . . . . 6 wff ∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏)
26	25, 13, 7	wral 3062	. . . . 5 wff ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏)
27	12, 26	wa 397	. . . 4 wff (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))
28	27, 10	cab 2710	. . 3 class {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}
29	2, 3, 4, 4, 28	cmpo 7411	. 2 class (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))})
30	1, 29	wceq 1542	1 wff Ismt = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))})

This definition is referenced by:  isismt  27816