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 e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) -> `' F e. ( N Ismty M ) ) )

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
2 1 adantr 
 |-  ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> `' F : Y -1-1-onto-> X )
3 f1ocnvdm 
 |-  ( ( F : X -1-1-onto-> Y /\ u e. Y ) -> ( `' F ` u ) e. X )
4 3 ex 
 |-  ( F : X -1-1-onto-> Y -> ( u e. Y -> ( `' F ` u ) e. X ) )
5 f1ocnvdm 
 |-  ( ( F : X -1-1-onto-> Y /\ v e. Y ) -> ( `' F ` v ) e. X )
6 5 ex 
 |-  ( F : X -1-1-onto-> Y -> ( v e. Y -> ( `' F ` v ) e. X ) )
7 4 6 anim12d 
 |-  ( F : X -1-1-onto-> Y -> ( ( u e. Y /\ v e. Y ) -> ( ( `' F ` u ) e. X /\ ( `' F ` v ) e. X ) ) )
8 7 adantr 
 |-  ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> ( ( u e. Y /\ v e. Y ) -> ( ( `' F ` u ) e. X /\ ( `' F ` v ) e. X ) ) )
9 8 imdistani 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( ( `' F ` u ) e. X /\ ( `' F ` v ) e. X ) ) )
10 oveq1 
 |-  ( x = ( `' F ` u ) -> ( x M y ) = ( ( `' F ` u ) M y ) )
11 fveq2 
 |-  ( x = ( `' F ` u ) -> ( F ` x ) = ( F ` ( `' F ` u ) ) )
12 11 oveq1d 
 |-  ( x = ( `' F ` u ) -> ( ( F ` x ) N ( F ` y ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` y ) ) )
13 10 12 eqeq12d 
 |-  ( x = ( `' F ` u ) -> ( ( x M y ) = ( ( F ` x ) N ( F ` y ) ) <-> ( ( `' F ` u ) M y ) = ( ( F ` ( `' F ` u ) ) N ( F ` y ) ) ) )
14 oveq2 
 |-  ( y = ( `' F ` v ) -> ( ( `' F ` u ) M y ) = ( ( `' F ` u ) M ( `' F ` v ) ) )
15 fveq2 
 |-  ( y = ( `' F ` v ) -> ( F ` y ) = ( F ` ( `' F ` v ) ) )
16 15 oveq2d 
 |-  ( y = ( `' F ` v ) -> ( ( F ` ( `' F ` u ) ) N ( F ` y ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) )
17 14 16 eqeq12d 
 |-  ( y = ( `' F ` v ) -> ( ( ( `' F ` u ) M y ) = ( ( F ` ( `' F ` u ) ) N ( F ` y ) ) <-> ( ( `' F ` u ) M ( `' F ` v ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) ) )
18 13 17 rspc2v 
 |-  ( ( ( `' F ` u ) e. X /\ ( `' F ` v ) e. X ) -> ( A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) -> ( ( `' F ` u ) M ( `' F ` v ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) ) )
19 18 impcom 
 |-  ( ( A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) /\ ( ( `' F ` u ) e. X /\ ( `' F ` v ) e. X ) ) -> ( ( `' F ` u ) M ( `' F ` v ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) )
20 19 adantll 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( ( `' F ` u ) e. X /\ ( `' F ` v ) e. X ) ) -> ( ( `' F ` u ) M ( `' F ` v ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) )
21 9 20 syl 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( `' F ` u ) M ( `' F ` v ) ) = ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) )
22 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ u e. Y ) -> ( F ` ( `' F ` u ) ) = u )
23 22 adantrr 
 |-  ( ( F : X -1-1-onto-> Y /\ ( u e. Y /\ v e. Y ) ) -> ( F ` ( `' F ` u ) ) = u )
24 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ v e. Y ) -> ( F ` ( `' F ` v ) ) = v )
25 24 adantrl 
 |-  ( ( F : X -1-1-onto-> Y /\ ( u e. Y /\ v e. Y ) ) -> ( F ` ( `' F ` v ) ) = v )
26 23 25 oveq12d 
 |-  ( ( F : X -1-1-onto-> Y /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) = ( u N v ) )
27 26 adantlr 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` ( `' F ` u ) ) N ( F ` ( `' F ` v ) ) ) = ( u N v ) )
28 21 27 eqtr2d 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( u e. Y /\ v e. Y ) ) -> ( u N v ) = ( ( `' F ` u ) M ( `' F ` v ) ) )
29 28 ralrimivva 
 |-  ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> A. u e. Y A. v e. Y ( u N v ) = ( ( `' F ` u ) M ( `' F ` v ) ) )
30 2 29 jca 
 |-  ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> ( `' F : Y -1-1-onto-> X /\ A. u e. Y A. v e. Y ( u N v ) = ( ( `' F ` u ) M ( `' F ` v ) ) ) )
31 30 a1i 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> ( `' F : Y -1-1-onto-> X /\ A. u e. Y A. v e. Y ( u N v ) = ( ( `' F ` u ) M ( `' F ` v ) ) ) ) )
32 isismty 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) )
33 isismty 
 |-  ( ( N e. ( *Met ` Y ) /\ M e. ( *Met ` X ) ) -> ( `' F e. ( N Ismty M ) <-> ( `' F : Y -1-1-onto-> X /\ A. u e. Y A. v e. Y ( u N v ) = ( ( `' F ` u ) M ( `' F ` v ) ) ) ) )
34 33 ancoms 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( `' F e. ( N Ismty M ) <-> ( `' F : Y -1-1-onto-> X /\ A. u e. Y A. v e. Y ( u N v ) = ( ( `' F ` u ) M ( `' F ` v ) ) ) ) )
35 31 32 34 3imtr4d 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) -> `' F e. ( N Ismty M ) ) )