Metamath Proof Explorer

Theorem isismty

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

Ref Expression
Assertion isismty ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismtyval ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝑀 Ismty 𝑁 ) = { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ) } )
2 1 eleq2d ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ) } ) )
3 f1of ⊒ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
4 3 adantr ⊒ ( ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
5 elfvdm ⊒ ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝑋 ∈ dom ∞Met )
6 elfvdm ⊒ ( 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) β†’ π‘Œ ∈ dom ∞Met )
7 fex2 ⊒ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ 𝑋 ∈ dom ∞Met ∧ π‘Œ ∈ dom ∞Met ) β†’ 𝐹 ∈ V )
8 4 5 6 7 syl3an ⊒ ( ( ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ∧ 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ 𝐹 ∈ V )
9 8 3expib ⊒ ( ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) β†’ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ 𝐹 ∈ V ) )
10 9 com12 ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) β†’ 𝐹 ∈ V ) )
11 f1oeq1 ⊒ ( 𝑓 = 𝐹 β†’ ( 𝑓 : 𝑋 –1-1-ontoβ†’ π‘Œ ↔ 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ) )
12 fveq1 ⊒ ( 𝑓 = 𝐹 β†’ ( 𝑓 β€˜ π‘₯ ) = ( 𝐹 β€˜ π‘₯ ) )
13 fveq1 ⊒ ( 𝑓 = 𝐹 β†’ ( 𝑓 β€˜ 𝑦 ) = ( 𝐹 β€˜ 𝑦 ) )
14 12 13 oveq12d ⊒ ( 𝑓 = 𝐹 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) )
15 14 eqeq2d ⊒ ( 𝑓 = 𝐹 β†’ ( ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ↔ ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) )
16 15 2ralbidv ⊒ ( 𝑓 = 𝐹 β†’ ( βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ↔ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) )
17 11 16 anbi12d ⊒ ( 𝑓 = 𝐹 β†’ ( ( 𝑓 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ) ↔ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ) )
18 17 elab3g ⊒ ( ( ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) β†’ 𝐹 ∈ V ) β†’ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ) } ↔ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ) )
19 10 18 syl ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ) } ↔ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ) )
20 2 19 bitrd ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ) )