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 = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cismt	⊢ Ismt
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vh	⊢ ℎ
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6		cbs	⊢ Base
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Base ‘ 𝑔 )
9	3	cv	⊢ ℎ
10	9 6	cfv	⊢ ( Base ‘ ℎ )
11	8 10 5	wf1o	⊢ 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ )
12		va	⊢ 𝑎
13		vb	⊢ 𝑏
14	12	cv	⊢ 𝑎
15	14 5	cfv	⊢ ( 𝑓 ‘ 𝑎 )
16		cds	⊢ dist
17	9 16	cfv	⊢ ( dist ‘ ℎ )
18	13	cv	⊢ 𝑏
19	18 5	cfv	⊢ ( 𝑓 ‘ 𝑏 )
20	15 19 17	co	⊢ ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) )
21	7 16	cfv	⊢ ( dist ‘ 𝑔 )
22	14 18 21	co	⊢ ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 )
23	20 22	wceq	⊢ ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 )
24	23 13 8	wral	⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 )
25	24 12 8	wral	⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 )
26	11 25	wa	⊢ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) )
27	26 4	cab	⊢ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) }
28	1 3 2 2 27	cmpo	⊢ ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) } )
29	0 28	wceq	⊢ Ismt = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) } )