Theorem isismt

Description: Property of being an isometry. Compare with isismty . (Contributed by Thierry Arnoux, 13-Dec-2019)

	Ref	Expression
Hypotheses	isismt.b	|- B = ( Base ` G )
	isismt.p	|- P = ( Base ` H )
	isismt.d	|- D = ( dist ` G )
	isismt.m	|- .- = ( dist ` H )
Assertion	isismt	|- ( ( G e. V /\ H e. W ) -> ( F e. ( G Ismt H ) <-> ( F : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isismt.b	|- B = ( Base ` G )
2		isismt.p	|- P = ( Base ` H )
3		isismt.d	|- D = ( dist ` G )
4		isismt.m	|- .- = ( dist ` H )
5		elex	|- ( G e. V -> G e. _V )
6		elex	|- ( H e. W -> H e. _V )
7		fveq2	|- ( g = G -> ( Base ` g ) = ( Base ` G ) )
8	7 1	eqtr4di	|- ( g = G -> ( Base ` g ) = B )
9	8	f1oeq2d	|- ( g = G -> ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) <-> f : B -1-1-onto-> ( Base ` h ) ) )
10		fveq2	|- ( g = G -> ( dist ` g ) = ( dist ` G ) )
11	10 3	eqtr4di	|- ( g = G -> ( dist ` g ) = D )
12	11	oveqd	|- ( g = G -> ( a ( dist ` g ) b ) = ( a D b ) )
13	12	eqeq2d	|- ( g = G -> ( ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) <-> ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) )
14	8 13	raleqbidv	|- ( g = G -> ( A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) <-> A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) )
15	8 14	raleqbidv	|- ( g = G -> ( A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) <-> A. a e. B A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) )
16	9 15	anbi12d	|- ( g = G -> ( ( 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 ) ) <-> ( f : B -1-1-onto-> ( Base ` h ) /\ A. a e. B A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) ) )
17	16	abbidv	|- ( g = G -> { 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 ) ) } = { f | ( f : B -1-1-onto-> ( Base ` h ) /\ A. a e. B A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) } )
18		fveq2	|- ( h = H -> ( Base ` h ) = ( Base ` H ) )
19	18 2	eqtr4di	|- ( h = H -> ( Base ` h ) = P )
20	19	f1oeq3d	|- ( h = H -> ( f : B -1-1-onto-> ( Base ` h ) <-> f : B -1-1-onto-> P ) )
21		fveq2	|- ( h = H -> ( dist ` h ) = ( dist ` H ) )
22	21 4	eqtr4di	|- ( h = H -> ( dist ` h ) = .- )
23	22	oveqd	|- ( h = H -> ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( ( f ` a ) .- ( f ` b ) ) )
24	23	eqeq1d	|- ( h = H -> ( ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) <-> ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) )
25	24	2ralbidv	|- ( h = H -> ( A. a e. B A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) <-> A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) )
26	20 25	anbi12d	|- ( h = H -> ( ( f : B -1-1-onto-> ( Base ` h ) /\ A. a e. B A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) <-> ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) ) )
27	26	abbidv	|- ( h = H -> { f | ( f : B -1-1-onto-> ( Base ` h ) /\ A. a e. B A. b e. B ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a D b ) ) } = { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } )
28		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 ) ) } )
29		ovex	|- ( P ^m B ) e. _V
30		f1of	|- ( f : B -1-1-onto-> P -> f : B --> P )
31	2	fvexi	|- P e. _V
32	1	fvexi	|- B e. _V
33	31 32	elmap	|- ( f e. ( P ^m B ) <-> f : B --> P )
34	30 33	sylibr	|- ( f : B -1-1-onto-> P -> f e. ( P ^m B ) )
35	34	adantr	|- ( ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) -> f e. ( P ^m B ) )
36	35	abssi	|- { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } C_ ( P ^m B )
37	29 36	ssexi	|- { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } e. _V
38	17 27 28 37	ovmpo	|- ( ( G e. _V /\ H e. _V ) -> ( G Ismt H ) = { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } )
39	5 6 38	syl2an	|- ( ( G e. V /\ H e. W ) -> ( G Ismt H ) = { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } )
40	39	eleq2d	|- ( ( G e. V /\ H e. W ) -> ( F e. ( G Ismt H ) <-> F e. { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } ) )
41		f1of	|- ( F : B -1-1-onto-> P -> F : B --> P )
42		fex	|- ( ( F : B --> P /\ B e. _V ) -> F e. _V )
43	41 32 42	sylancl	|- ( F : B -1-1-onto-> P -> F e. _V )
44	43	adantr	|- ( ( F : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) -> F e. _V )
45		f1oeq1	|- ( f = F -> ( f : B -1-1-onto-> P <-> F : B -1-1-onto-> P ) )
46		fveq1	|- ( f = F -> ( f ` a ) = ( F ` a ) )
47		fveq1	|- ( f = F -> ( f ` b ) = ( F ` b ) )
48	46 47	oveq12d	|- ( f = F -> ( ( f ` a ) .- ( f ` b ) ) = ( ( F ` a ) .- ( F ` b ) ) )
49	48	eqeq1d	|- ( f = F -> ( ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) <-> ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) )
50	49	2ralbidv	|- ( f = F -> ( A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) <-> A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) )
51	45 50	anbi12d	|- ( f = F -> ( ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) <-> ( F : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) ) )
52	44 51	elab3	|- ( F e. { f | ( f : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( f ` a ) .- ( f ` b ) ) = ( a D b ) ) } <-> ( F : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) )
53	40 52	bitrdi	|- ( ( G e. V /\ H e. W ) -> ( F e. ( G Ismt H ) <-> ( F : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) ) )