Metamath Proof Explorer

Theorem ismtycnv

Description: The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion ismtycnv ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
2 1 adantr ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
3 f1ocnvdm ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑢 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 )
4 3 ex ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( 𝑢 ∈ 𝑌 → ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) )
5 f1ocnvdm ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 )
6 5 ex ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( 𝑣 ∈ 𝑌 → ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) )
7 4 6 anim12d ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) )
8 7 adantr ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) )
9 8 imdistani ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) )
10 oveq1 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑢 ) → ( 𝑥 𝑀 𝑦 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 𝑦 ) )
11 fveq2 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) )
12 11 oveq1d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑢 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) )
13 10 12 eqeq12d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑢 ) → ( ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 𝑦 ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
14 oveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑣 ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 𝑦 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) )
15 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑣 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) )
16 15 oveq2d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑣 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
17 14 16 eqeq12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑣 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 𝑦 ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ) )
18 13 17 rspc2v ⊢ ( ( ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ) )
19 18 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
20 19 adantll ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
21 9 20 syl ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
22 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑢 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) = 𝑢 )
23 22 adantrr ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) = 𝑢 )
24 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) = 𝑣 )
25 24 adantrl ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) = 𝑣 )
26 23 25 oveq12d ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( 𝑢 𝑁 𝑣 ) )
27 26 adantlr ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( 𝑢 𝑁 𝑣 ) )
28 21 27 eqtr2d ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( 𝑢 𝑁 𝑣 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) )
29 28 ralrimivva ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) )
30 2 29 jca ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
31 30 a1i ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) ) ) )
32 isismty ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
33 isismty ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ↔ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) ) ) )
34 33 ancoms ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ↔ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝑀 ( ◡ 𝐹 ‘ 𝑣 ) ) ) ) )
35 31 32 34 3imtr4d ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) )