isismty

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

		Ref	Expression
	Assertion	isismty	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$

Proof

Step	Hyp	Ref	Expression
1		ismtyval	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to M Ismty N = \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\}$
2	1	eleq2d	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \leftrightarrow F \in \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\})$
3		f1of	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X ⟶ Y$
4	3	adantr	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \to F : X ⟶ Y$
5		elfvdm	$⊢ M \in ∞Met (X) \to X \in dom ∞Met$
6		elfvdm	$⊢ N \in ∞Met (Y) \to Y \in dom ∞Met$
7		fex2	$⊢ (F : X ⟶ Y \land X \in dom ∞Met \land Y \in dom ∞Met) \to F \in V$
8	4 5 6 7	syl3an	$⊢ ((F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \land M \in ∞Met (X) \land N \in ∞Met (Y)) \to F \in V$
9	8	3expib	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \to ((M \in ∞Met (X) \land N \in ∞Met (Y)) \to F \in V)$
10	9	com12	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to ((F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \to F \in V)$
11		f1oeq1	$⊢ f = F \to (f : X \underset{1-1 onto}{⟶} Y \leftrightarrow F : X \underset{1-1 onto}{⟶} Y)$
12		fveq1	$⊢ f = F \to f (x) = F (x)$
13		fveq1	$⊢ f = F \to f (y) = F (y)$
14	12 13	oveq12d	$⊢ f = F \to f (x) N f (y) = F (x) N F (y)$
15	14	eqeq2d	$⊢ f = F \to (x M y = f (x) N f (y) \leftrightarrow x M y = F (x) N F (y))$
16	15	2ralbidv	$⊢ f = F \to (\forall x \in X \forall y \in X x M y = f (x) N f (y) \leftrightarrow \forall x \in X \forall y \in X x M y = F (x) N F (y))$
17	11 16	anbi12d	$⊢ f = F \to ((f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y)) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$
18	17	elab3g	$⊢ ((F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \to F \in V) \to (F \in \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\} \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$
19	10 18	syl	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in \{f \| (f : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = f (x) N f (y))\} \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$
20	2 19	bitrd	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$

Metamath Proof Explorer

Theorem isismty

Proof