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 𝑀 ) ) )