Metamath Proof Explorer

Theorem ismtyres

Description: A restriction of an isometry is an isometry. The condition A C_ X is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses ismtyres.2 
|- B = ( F " A )
ismtyres.3 
|- S = ( M |` ( A X. A ) )
ismtyres.4 
|- T = ( N |` ( B X. B ) )
Assertion ismtyres 
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( F |` A ) e. ( S Ismty T ) )

Proof

Step Hyp Ref Expression
1 ismtyres.2 
 |-  B = ( F " A )
2 ismtyres.3 
 |-  S = ( M |` ( A X. A ) )
3 ismtyres.4 
 |-  T = ( N |` ( B X. B ) )
4 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 ) ) ) ) )
5 4 simprbda 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ F e. ( M Ismty N ) ) -> F : X -1-1-onto-> Y )
6 5 adantrr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> F : X -1-1-onto-> Y )
7 f1of1 
 |-  ( F : X -1-1-onto-> Y -> F : X -1-1-> Y )
8 6 7 syl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> F : X -1-1-> Y )
9 simprr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> A C_ X )
10 f1ores 
 |-  ( ( F : X -1-1-> Y /\ A C_ X ) -> ( F |` A ) : A -1-1-onto-> ( F " A ) )
11 8 9 10 syl2anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( F |` A ) : A -1-1-onto-> ( F " A ) )
12 4 biimpa 
 |-  ( ( ( 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 ) ) ) )
13 12 adantrr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) )
14 ssel 
 |-  ( A C_ X -> ( u e. A -> u e. X ) )
15 ssel 
 |-  ( A C_ X -> ( v e. A -> v e. X ) )
16 14 15 anim12d 
 |-  ( A C_ X -> ( ( u e. A /\ v e. A ) -> ( u e. X /\ v e. X ) ) )
17 16 imp 
 |-  ( ( A C_ X /\ ( u e. A /\ v e. A ) ) -> ( u e. X /\ v e. X ) )
18 oveq1 
 |-  ( x = u -> ( x M y ) = ( u M y ) )
19 fveq2 
 |-  ( x = u -> ( F ` x ) = ( F ` u ) )
20 19 oveq1d 
 |-  ( x = u -> ( ( F ` x ) N ( F ` y ) ) = ( ( F ` u ) N ( F ` y ) ) )
21 18 20 eqeq12d 
 |-  ( x = u -> ( ( x M y ) = ( ( F ` x ) N ( F ` y ) ) <-> ( u M y ) = ( ( F ` u ) N ( F ` y ) ) ) )
22 oveq2 
 |-  ( y = v -> ( u M y ) = ( u M v ) )
23 fveq2 
 |-  ( y = v -> ( F ` y ) = ( F ` v ) )
24 23 oveq2d 
 |-  ( y = v -> ( ( F ` u ) N ( F ` y ) ) = ( ( F ` u ) N ( F ` v ) ) )
25 22 24 eqeq12d 
 |-  ( y = v -> ( ( u M y ) = ( ( F ` u ) N ( F ` y ) ) <-> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) ) )
26 21 25 rspc2v 
 |-  ( ( u e. X /\ v e. X ) -> ( A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) -> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) ) )
27 17 26 syl 
 |-  ( ( A C_ X /\ ( u e. A /\ v e. A ) ) -> ( A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) -> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) ) )
28 27 imp 
 |-  ( ( ( A C_ X /\ ( u e. A /\ v e. A ) ) /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) )
29 28 an32s 
 |-  ( ( ( A C_ X /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) )
30 29 adantlrl 
 |-  ( ( ( A C_ X /\ ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) )
31 30 adantlll 
 |-  ( ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ A C_ X ) /\ ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( u M v ) = ( ( F ` u ) N ( F ` v ) ) )
32 2 oveqi 
 |-  ( u S v ) = ( u ( M |` ( A X. A ) ) v )
33 ovres 
 |-  ( ( u e. A /\ v e. A ) -> ( u ( M |` ( A X. A ) ) v ) = ( u M v ) )
34 32 33 syl5eq 
 |-  ( ( u e. A /\ v e. A ) -> ( u S v ) = ( u M v ) )
35 34 adantl 
 |-  ( ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ A C_ X ) /\ ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( u S v ) = ( u M v ) )
36 fvres 
 |-  ( u e. A -> ( ( F |` A ) ` u ) = ( F ` u ) )
37 36 ad2antrl 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( ( F |` A ) ` u ) = ( F ` u ) )
38 fvres 
 |-  ( v e. A -> ( ( F |` A ) ` v ) = ( F ` v ) )
39 38 ad2antll 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( ( F |` A ) ` v ) = ( F ` v ) )
40 37 39 oveq12d 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) = ( ( F ` u ) T ( F ` v ) ) )
41 3 oveqi 
 |-  ( ( F ` u ) T ( F ` v ) ) = ( ( F ` u ) ( N |` ( B X. B ) ) ( F ` v ) )
42 f1ofun 
 |-  ( F : X -1-1-onto-> Y -> Fun F )
43 42 adantl 
 |-  ( ( A C_ X /\ F : X -1-1-onto-> Y ) -> Fun F )
44 f1odm 
 |-  ( F : X -1-1-onto-> Y -> dom F = X )
45 44 sseq2d 
 |-  ( F : X -1-1-onto-> Y -> ( A C_ dom F <-> A C_ X ) )
46 45 biimparc 
 |-  ( ( A C_ X /\ F : X -1-1-onto-> Y ) -> A C_ dom F )
47 funfvima2 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( u e. A -> ( F ` u ) e. ( F " A ) ) )
48 43 46 47 syl2anc 
 |-  ( ( A C_ X /\ F : X -1-1-onto-> Y ) -> ( u e. A -> ( F ` u ) e. ( F " A ) ) )
49 48 imp 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ u e. A ) -> ( F ` u ) e. ( F " A ) )
50 49 1 eleqtrrdi 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ u e. A ) -> ( F ` u ) e. B )
51 50 adantrr 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( F ` u ) e. B )
52 funfvima2 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( v e. A -> ( F ` v ) e. ( F " A ) ) )
53 43 46 52 syl2anc 
 |-  ( ( A C_ X /\ F : X -1-1-onto-> Y ) -> ( v e. A -> ( F ` v ) e. ( F " A ) ) )
54 53 imp 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ v e. A ) -> ( F ` v ) e. ( F " A ) )
55 54 1 eleqtrrdi 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ v e. A ) -> ( F ` v ) e. B )
56 55 adantrl 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( F ` v ) e. B )
57 51 56 ovresd 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( ( F ` u ) ( N |` ( B X. B ) ) ( F ` v ) ) = ( ( F ` u ) N ( F ` v ) ) )
58 41 57 syl5eq 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( ( F ` u ) T ( F ` v ) ) = ( ( F ` u ) N ( F ` v ) ) )
59 40 58 eqtrd 
 |-  ( ( ( A C_ X /\ F : X -1-1-onto-> Y ) /\ ( u e. A /\ v e. A ) ) -> ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) = ( ( F ` u ) N ( F ` v ) ) )
60 59 adantlrr 
 |-  ( ( ( A C_ X /\ ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) = ( ( F ` u ) N ( F ` v ) ) )
61 60 adantlll 
 |-  ( ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ A C_ X ) /\ ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) = ( ( F ` u ) N ( F ` v ) ) )
62 31 35 61 3eqtr4d 
 |-  ( ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ A C_ X ) /\ ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) /\ ( u e. A /\ v e. A ) ) -> ( u S v ) = ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) )
63 62 ralrimivva 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ A C_ X ) /\ ( 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. A A. v e. A ( u S v ) = ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) )
64 63 adantlrl 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) /\ ( 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. A A. v e. A ( u S v ) = ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) )
65 13 64 mpdan 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> A. u e. A A. v e. A ( u S v ) = ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) )
66 xmetres2 
 |-  ( ( M e. ( *Met ` X ) /\ A C_ X ) -> ( M |` ( A X. A ) ) e. ( *Met ` A ) )
67 2 66 eqeltrid 
 |-  ( ( M e. ( *Met ` X ) /\ A C_ X ) -> S e. ( *Met ` A ) )
68 67 ad2ant2rl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> S e. ( *Met ` A ) )
69 simplr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> N e. ( *Met ` Y ) )
70 imassrn 
 |-  ( F " A ) C_ ran F
71 1 70 eqsstri 
 |-  B C_ ran F
72 f1ofo 
 |-  ( F : X -1-1-onto-> Y -> F : X -onto-> Y )
73 forn 
 |-  ( F : X -onto-> Y -> ran F = Y )
74 6 72 73 3syl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ran F = Y )
75 71 74 sseqtrid 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> B C_ Y )
76 xmetres2 
 |-  ( ( N e. ( *Met ` Y ) /\ B C_ Y ) -> ( N |` ( B X. B ) ) e. ( *Met ` B ) )
77 69 75 76 syl2anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( N |` ( B X. B ) ) e. ( *Met ` B ) )
78 3 77 eqeltrid 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> T e. ( *Met ` B ) )
79 1 fveq2i 
 |-  ( *Met ` B ) = ( *Met ` ( F " A ) )
80 78 79 eleqtrdi 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> T e. ( *Met ` ( F " A ) ) )
81 isismty 
 |-  ( ( S e. ( *Met ` A ) /\ T e. ( *Met ` ( F " A ) ) ) -> ( ( F |` A ) e. ( S Ismty T ) <-> ( ( F |` A ) : A -1-1-onto-> ( F " A ) /\ A. u e. A A. v e. A ( u S v ) = ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) ) ) )
82 68 80 81 syl2anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( ( F |` A ) e. ( S Ismty T ) <-> ( ( F |` A ) : A -1-1-onto-> ( F " A ) /\ A. u e. A A. v e. A ( u S v ) = ( ( ( F |` A ) ` u ) T ( ( F |` A ) ` v ) ) ) ) )
83 11 65 82 mpbir2and 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( F |` A ) e. ( S Ismty T ) )