ismtycnv

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

		Ref	Expression
	Assertion	ismtycnv	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \to F^{-1} \in (N Ismty M))$

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
2	1	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^{-1} : Y \underset{1-1 onto}{⟶} X$
3		f1ocnvdm	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land u \in Y) \to F^{-1} (u) \in X$
4	3	ex	$⊢ F : X \underset{1-1 onto}{⟶} Y \to (u \in Y \to F^{-1} (u) \in X)$
5		f1ocnvdm	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land v \in Y) \to F^{-1} (v) \in X$
6	5	ex	$⊢ F : X \underset{1-1 onto}{⟶} Y \to (v \in Y \to F^{-1} (v) \in X)$
7	4 6	anim12d	$⊢ F : X \underset{1-1 onto}{⟶} Y \to ((u \in Y \land v \in Y) \to (F^{-1} (u) \in X \land F^{-1} (v) \in X))$
8	7	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 ((u \in Y \land v \in Y) \to (F^{-1} (u) \in X \land F^{-1} (v) \in X))$
9	8	imdistani	$⊢ ((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 (u \in Y \land v \in 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)) \land (F^{-1} (u) \in X \land F^{-1} (v) \in X))$
10		oveq1	$⊢ x = F^{-1} (u) \to x M y = F^{-1} (u) M y$
11		fveq2	$⊢ x = F^{-1} (u) \to F (x) = F (F^{-1} (u))$
12	11	oveq1d	$⊢ x = F^{-1} (u) \to F (x) N F (y) = F (F^{-1} (u)) N F (y)$
13	10 12	eqeq12d	$⊢ x = F^{-1} (u) \to (x M y = F (x) N F (y) \leftrightarrow F^{-1} (u) M y = F (F^{-1} (u)) N F (y))$
14		oveq2	$⊢ y = F^{-1} (v) \to F^{-1} (u) M y = F^{-1} (u) M F^{-1} (v)$
15		fveq2	$⊢ y = F^{-1} (v) \to F (y) = F (F^{-1} (v))$
16	15	oveq2d	$⊢ y = F^{-1} (v) \to F (F^{-1} (u)) N F (y) = F (F^{-1} (u)) N F (F^{-1} (v))$
17	14 16	eqeq12d	$⊢ y = F^{-1} (v) \to (F^{-1} (u) M y = F (F^{-1} (u)) N F (y) \leftrightarrow F^{-1} (u) M F^{-1} (v) = F (F^{-1} (u)) N F (F^{-1} (v)))$
18	13 17	rspc2v	$⊢ (F^{-1} (u) \in X \land F^{-1} (v) \in X) \to (\forall x \in X \forall y \in X x M y = F (x) N F (y) \to F^{-1} (u) M F^{-1} (v) = F (F^{-1} (u)) N F (F^{-1} (v)))$
19	18	impcom	$⊢ (\forall x \in X \forall y \in X x M y = F (x) N F (y) \land (F^{-1} (u) \in X \land F^{-1} (v) \in X)) \to F^{-1} (u) M F^{-1} (v) = F (F^{-1} (u)) N F (F^{-1} (v))$
20	19	adantll	$⊢ ((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 (F^{-1} (u) \in X \land F^{-1} (v) \in X)) \to F^{-1} (u) M F^{-1} (v) = F (F^{-1} (u)) N F (F^{-1} (v))$
21	9 20	syl	$⊢ ((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 (u \in Y \land v \in Y)) \to F^{-1} (u) M F^{-1} (v) = F (F^{-1} (u)) N F (F^{-1} (v))$
22		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land u \in Y) \to F (F^{-1} (u)) = u$
23	22	adantrr	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land (u \in Y \land v \in Y)) \to F (F^{-1} (u)) = u$
24		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land v \in Y) \to F (F^{-1} (v)) = v$
25	24	adantrl	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land (u \in Y \land v \in Y)) \to F (F^{-1} (v)) = v$
26	23 25	oveq12d	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land (u \in Y \land v \in Y)) \to F (F^{-1} (u)) N F (F^{-1} (v)) = u N v$
27	26	adantlr	$⊢ ((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 (u \in Y \land v \in Y)) \to F (F^{-1} (u)) N F (F^{-1} (v)) = u N v$
28	21 27	eqtr2d	$⊢ ((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 (u \in Y \land v \in Y)) \to u N v = F^{-1} (u) M F^{-1} (v)$
29	28	ralrimivva	$⊢ (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 \forall u \in Y \forall v \in Y u N v = F^{-1} (u) M F^{-1} (v)$
30	2 29	jca	$⊢ (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^{-1} : Y \underset{1-1 onto}{⟶} X \land \forall u \in Y \forall v \in Y u N v = F^{-1} (u) M F^{-1} (v))$
31	30	a1i	$⊢ (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^{-1} : Y \underset{1-1 onto}{⟶} X \land \forall u \in Y \forall v \in Y u N v = F^{-1} (u) M F^{-1} (v)))$
32		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)))$
33		isismty	$⊢ (N \in ∞Met (Y) \land M \in ∞Met (X)) \to (F^{-1} \in (N Ismty M) \leftrightarrow (F^{-1} : Y \underset{1-1 onto}{⟶} X \land \forall u \in Y \forall v \in Y u N v = F^{-1} (u) M F^{-1} (v)))$
34	33	ancoms	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F^{-1} \in (N Ismty M) \leftrightarrow (F^{-1} : Y \underset{1-1 onto}{⟶} X \land \forall u \in Y \forall v \in Y u N v = F^{-1} (u) M F^{-1} (v)))$
35	31 32 34	3imtr4d	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \to F^{-1} \in (N Ismty M))$

Metamath Proof Explorer

Theorem ismtycnv

Proof