Metamath Proof Explorer

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 = ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cismt 
 |-  Ismt
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vh 
 |-  h
4 vf 
 |-  f
5 4 cv 
 |-  f
6 cbs 
 |-  Base
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Base ` g )
9 3 cv 
 |-  h
10 9 6 cfv 
 |-  ( Base ` h )
11 8 10 5 wf1o 
 |-  f : ( Base ` g ) -1-1-onto-> ( Base ` h )
12 va 
 |-  a
13 vb 
 |-  b
14 12 cv 
 |-  a
15 14 5 cfv 
 |-  ( f ` a )
16 cds 
 |-  dist
17 9 16 cfv 
 |-  ( dist ` h )
18 13 cv 
 |-  b
19 18 5 cfv 
 |-  ( f ` b )
20 15 19 17 co 
 |-  ( ( f ` a ) ( dist ` h ) ( f ` b ) )
21 7 16 cfv 
 |-  ( dist ` g )
22 14 18 21 co 
 |-  ( a ( dist ` g ) b )
23 20 22 wceq 
 |-  ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b )
24 23 13 8 wral 
 |-  A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b )
25 24 12 8 wral 
 |-  A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b )
26 11 25 wa 
 |-  ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) )
27 26 4 cab 
 |-  { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) }
28 1 3 2 2 27 cmpo 
 |-  ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )
29 0 28 wceq 
 |-  Ismt = ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )