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 ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F ∈ M Ismty N → F -1 ∈ N Ismty M

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ F : X ⟶ 1-1 onto Y → F -1 : Y ⟶ 1-1 onto X
2 1 adantr ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y → F -1 : Y ⟶ 1-1 onto X
3 f1ocnvdm ⊢ F : X ⟶ 1-1 onto Y ∧ u ∈ Y → F -1 ⁡ u ∈ X
4 3 ex ⊢ F : X ⟶ 1-1 onto Y → u ∈ Y → F -1 ⁡ u ∈ X
5 f1ocnvdm ⊢ F : X ⟶ 1-1 onto Y ∧ v ∈ Y → F -1 ⁡ v ∈ X
6 5 ex ⊢ F : X ⟶ 1-1 onto Y → v ∈ Y → F -1 ⁡ v ∈ X
7 4 6 anim12d ⊢ F : X ⟶ 1-1 onto Y → u ∈ Y ∧ v ∈ Y → F -1 ⁡ u ∈ X ∧ F -1 ⁡ v ∈ X
8 7 adantr ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y → u ∈ Y ∧ v ∈ Y → F -1 ⁡ u ∈ X ∧ F -1 ⁡ v ∈ X
9 8 imdistani ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ u ∈ Y ∧ v ∈ Y → F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ F -1 ⁡ u ∈ X ∧ F -1 ⁡ v ∈ X
10 oveq1 ⊢ x = F -1 ⁡ u → x M y = F -1 ⁡ u M y
11 fveq2 ⊢ x = F -1 ⁡ u → F ⁡ x = F ⁡ F -1 ⁡ u
12 11 oveq1d ⊢ x = F -1 ⁡ u → F ⁡ x N F ⁡ y = F ⁡ F -1 ⁡ u N F ⁡ y
13 10 12 eqeq12d ⊢ x = F -1 ⁡ u → x M y = F ⁡ x N F ⁡ y ↔ F -1 ⁡ u M y = F ⁡ F -1 ⁡ u N F ⁡ y
14 oveq2 ⊢ y = F -1 ⁡ v → F -1 ⁡ u M y = F -1 ⁡ u M F -1 ⁡ v
15 fveq2 ⊢ y = F -1 ⁡ v → F ⁡ y = F ⁡ F -1 ⁡ v
16 15 oveq2d ⊢ y = F -1 ⁡ v → F ⁡ F -1 ⁡ u N F ⁡ y = F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v
17 14 16 eqeq12d ⊢ y = F -1 ⁡ v → F -1 ⁡ u M y = F ⁡ F -1 ⁡ u N F ⁡ y ↔ F -1 ⁡ u M F -1 ⁡ v = F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v
18 13 17 rspc2v ⊢ F -1 ⁡ u ∈ X ∧ F -1 ⁡ v ∈ X → ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y → F -1 ⁡ u M F -1 ⁡ v = F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v
19 18 impcom ⊢ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ F -1 ⁡ u ∈ X ∧ F -1 ⁡ v ∈ X → F -1 ⁡ u M F -1 ⁡ v = F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v
20 19 adantll ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ F -1 ⁡ u ∈ X ∧ F -1 ⁡ v ∈ X → F -1 ⁡ u M F -1 ⁡ v = F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v
21 9 20 syl ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ u ∈ Y ∧ v ∈ Y → F -1 ⁡ u M F -1 ⁡ v = F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v
22 f1ocnvfv2 ⊢ F : X ⟶ 1-1 onto Y ∧ u ∈ Y → F ⁡ F -1 ⁡ u = u
23 22 adantrr ⊢ F : X ⟶ 1-1 onto Y ∧ u ∈ Y ∧ v ∈ Y → F ⁡ F -1 ⁡ u = u
24 f1ocnvfv2 ⊢ F : X ⟶ 1-1 onto Y ∧ v ∈ Y → F ⁡ F -1 ⁡ v = v
25 24 adantrl ⊢ F : X ⟶ 1-1 onto Y ∧ u ∈ Y ∧ v ∈ Y → F ⁡ F -1 ⁡ v = v
26 23 25 oveq12d ⊢ F : X ⟶ 1-1 onto Y ∧ u ∈ Y ∧ v ∈ Y → F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v = u N v
27 26 adantlr ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ u ∈ Y ∧ v ∈ Y → F ⁡ F -1 ⁡ u N F ⁡ F -1 ⁡ v = u N v
28 21 27 eqtr2d ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y ∧ u ∈ Y ∧ v ∈ Y → u N v = F -1 ⁡ u M F -1 ⁡ v
29 28 ralrimivva ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y → ∀ u ∈ Y ∀ v ∈ Y u N v = F -1 ⁡ u M F -1 ⁡ v
30 2 29 jca ⊢ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y → F -1 : Y ⟶ 1-1 onto X ∧ ∀ u ∈ Y ∀ v ∈ Y u N v = F -1 ⁡ u M F -1 ⁡ v
31 30 a1i ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y → F -1 : Y ⟶ 1-1 onto X ∧ ∀ u ∈ Y ∀ v ∈ Y u N v = F -1 ⁡ u M F -1 ⁡ v
32 isismty ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F ∈ M Ismty N ↔ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y
33 isismty ⊢ N ∈ ∞Met ⁡ Y ∧ M ∈ ∞Met ⁡ X → F -1 ∈ N Ismty M ↔ F -1 : Y ⟶ 1-1 onto X ∧ ∀ u ∈ Y ∀ v ∈ Y u N v = F -1 ⁡ u M F -1 ⁡ v
34 33 ancoms ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F -1 ∈ N Ismty M ↔ F -1 : Y ⟶ 1-1 onto X ∧ ∀ u ∈ Y ∀ v ∈ Y u N v = F -1 ⁡ u M F -1 ⁡ v
35 31 32 34 3imtr4d ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F ∈ M Ismty N → F -1 ∈ N Ismty M