Metamath Proof Explorer

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 ∈ V ∧ H ∈ W → F ∈ G Ismt H ↔ F : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ 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 ∈ V → G ∈ V
6 elex ⊢ H ∈ W → H ∈ 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 → ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b ↔ ∀ b ∈ B f ⁡ a dist ⁡ h f ⁡ b = a D b
15 8 14 raleqbidv ⊢ g = G → ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b ↔ ∀ a ∈ B ∀ b ∈ 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 ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b ↔ f : B ⟶ 1-1 onto Base h ∧ ∀ a ∈ B ∀ b ∈ 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 ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b = f | f : B ⟶ 1-1 onto Base h ∧ ∀ a ∈ B ∀ b ∈ 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 ∈ B ∀ b ∈ B f ⁡ a dist ⁡ h f ⁡ b = a D b ↔ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b
26 20 25 anbi12d ⊢ h = H → f : B ⟶ 1-1 onto Base h ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a dist ⁡ h f ⁡ b = a D b ↔ f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b
27 26 abbidv ⊢ h = H → f | f : B ⟶ 1-1 onto Base h ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a dist ⁡ h f ⁡ b = a D b = f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b
28 df-ismt ⊢ Ismt = g ∈ V , h ∈ V ⟼ f | f : Base g ⟶ 1-1 onto Base h ∧ ∀ a ∈ Base g ∀ b ∈ Base g f ⁡ a dist ⁡ h f ⁡ b = a dist ⁡ g b
29 ovex ⊢ P B ∈ V
30 f1of ⊢ f : B ⟶ 1-1 onto P → f : B ⟶ P
31 2 fvexi ⊢ P ∈ V
32 1 fvexi ⊢ B ∈ V
33 31 32 elmap ⊢ f ∈ P B ↔ f : B ⟶ P
34 30 33 sylibr ⊢ f : B ⟶ 1-1 onto P → f ∈ P B
35 34 adantr ⊢ f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b → f ∈ P B
36 35 abssi ⊢ f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b ⊆ P B
37 29 36 ssexi ⊢ f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b ∈ V
38 17 27 28 37 ovmpo ⊢ G ∈ V ∧ H ∈ V → G Ismt H = f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b
39 5 6 38 syl2an ⊢ G ∈ V ∧ H ∈ W → G Ismt H = f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b
40 39 eleq2d ⊢ G ∈ V ∧ H ∈ W → F ∈ G Ismt H ↔ F ∈ f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ 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 ∈ V → F ∈ V
43 41 32 42 sylancl ⊢ F : B ⟶ 1-1 onto P → F ∈ V
44 43 adantr ⊢ F : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B F ⁡ a - ˙ F ⁡ b = a D b → F ∈ 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 ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b ↔ ∀ a ∈ B ∀ b ∈ B F ⁡ a - ˙ F ⁡ b = a D b
51 45 50 anbi12d ⊢ f = F → f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b ↔ F : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B F ⁡ a - ˙ F ⁡ b = a D b
52 44 51 elab3 ⊢ F ∈ f | f : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B f ⁡ a - ˙ f ⁡ b = a D b ↔ F : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B F ⁡ a - ˙ F ⁡ b = a D b
53 40 52 bitrdi ⊢ G ∈ V ∧ H ∈ W → F ∈ G Ismt H ↔ F : B ⟶ 1-1 onto P ∧ ∀ a ∈ B ∀ b ∈ B F ⁡ a - ˙ F ⁡ b = a D b