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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
isismt.p ⊢ 𝑃 = ( Base ‘ 𝐻 )
isismt.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
isismt.m ⊢ − = ( dist ‘ 𝐻 )
Assertion isismt ( ( 𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐺 Ismt 𝐻 ) ↔ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ) )

Proof

Step Hyp Ref Expression
1 isismt.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 isismt.p ⊢ 𝑃 = ( Base ‘ 𝐻 )
3 isismt.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
4 isismt.m ⊢ − = ( dist ‘ 𝐻 )
5 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
6 elex ⊢ ( 𝐻 ∈ 𝑊 → 𝐻 ∈ V )
7 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
8 7 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
9 8 f1oeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ↔ 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ ℎ ) ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
11 10 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = 𝐷 )
12 11 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑎 𝐷 𝑏 ) )
13 12 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ↔ ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
14 8 13 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
15 8 14 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
16 9 15 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) ↔ ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ) )
17 16 abbidv ⊢ ( 𝑔 = 𝐺 → { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) } = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } )
18 fveq2 ⊢ ( ℎ = 𝐻 → ( Base ‘ ℎ ) = ( Base ‘ 𝐻 ) )
19 18 2 eqtr4di ⊢ ( ℎ = 𝐻 → ( Base ‘ ℎ ) = 𝑃 )
20 19 f1oeq3d ⊢ ( ℎ = 𝐻 → ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ ℎ ) ↔ 𝑓 : 𝐵 –1-1-onto→ 𝑃 ) )
21 fveq2 ⊢ ( ℎ = 𝐻 → ( dist ‘ ℎ ) = ( dist ‘ 𝐻 ) )
22 21 4 eqtr4di ⊢ ( ℎ = 𝐻 → ( dist ‘ ℎ ) = − )
23 22 oveqd ⊢ ( ℎ = 𝐻 → ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) )
24 23 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ↔ ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
25 24 2ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
26 20 25 anbi12d ⊢ ( ℎ = 𝐻 → ( ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ↔ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ) )
27 26 abbidv ⊢ ( ℎ = 𝐻 → { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } )
28 df-ismt ⊢ Ismt = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑔 ) –1-1-onto→ ( Base ‘ ℎ ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑓 ‘ 𝑎 ) ( dist ‘ ℎ ) ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 ( dist ‘ 𝑔 ) 𝑏 ) ) } )
29 ovex ⊢ ( 𝑃 ↑m 𝐵 ) ∈ V
30 f1of ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 → 𝑓 : 𝐵 ⟶ 𝑃 )
31 2 fvexi ⊢ 𝑃 ∈ V
32 1 fvexi ⊢ 𝐵 ∈ V
33 31 32 elmap ⊢ ( 𝑓 ∈ ( 𝑃 ↑m 𝐵 ) ↔ 𝑓 : 𝐵 ⟶ 𝑃 )
34 30 33 sylibr ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 → 𝑓 ∈ ( 𝑃 ↑m 𝐵 ) )
35 34 adantr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) → 𝑓 ∈ ( 𝑃 ↑m 𝐵 ) )
36 35 abssi ⊢ { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } ⊆ ( 𝑃 ↑m 𝐵 )
37 29 36 ssexi ⊢ { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } ∈ V
38 17 27 28 37 ovmpo ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐺 Ismt 𝐻 ) = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } )
39 5 6 38 syl2an ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → ( 𝐺 Ismt 𝐻 ) = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } )
40 39 eleq2d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐺 Ismt 𝐻 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } ) )
41 f1of ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 → 𝐹 : 𝐵 ⟶ 𝑃 )
42 fex ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝑃 ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
43 41 32 42 sylancl ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 → 𝐹 ∈ V )
44 43 adantr ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) → 𝐹 ∈ V )
45 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ↔ 𝐹 : 𝐵 –1-1-onto→ 𝑃 ) )
46 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
47 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
48 46 47 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) )
49 48 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ↔ ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
50 49 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
51 45 50 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ↔ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ) )
52 44 51 elab3 ⊢ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑓 ‘ 𝑎 ) − ( 𝑓 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) } ↔ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) )
53 40 52 bitrdi ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐺 Ismt 𝐻 ) ↔ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐷 𝑏 ) ) ) )