ismtyima

Description: The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014)

		Ref	Expression
	Assertion	ismtyima	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F [P ball (M) R] = F (P) ball (N) R$

Proof

Step	Hyp	Ref	Expression
1		imassrn	$⊢ F [P ball (M) R] \subseteq ran F$
2		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)))$
3	2	biimp3a	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \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))$
4	3	adantr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \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))$
5	4	simpld	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F : X \underset{1-1 onto}{⟶} Y$
6		f1of	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X ⟶ Y$
7	5 6	syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F : X ⟶ Y$
8	7	frnd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to ran F \subseteq Y$
9	1 8	sstrid	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F [P ball (M) R] \subseteq Y$
10	9	sseld	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to (x \in F [P ball (M) R] \to x \in Y)$
11		simpl2	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to N \in ∞Met (Y)$
12		simprl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to P \in X$
13		ffvelcdm	$⊢ (F : X ⟶ Y \land P \in X) \to F (P) \in Y$
14	7 12 13	syl2anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F (P) \in Y$
15		simprr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{})) \to R \in ℝ^{}$
16		blssm	$⊢ (N \in ∞Met (Y) \land F (P) \in Y \land R \in ℝ^{*}) \to F (P) ball (N) R \subseteq Y$
17	11 14 15 16	syl3anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F (P) ball (N) R \subseteq Y$
18	17	sseld	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to (x \in (F (P) ball (N) R) \to x \in Y)$
19		simpl1	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to M \in ∞Met (X)$
20	19	adantr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to M \in ∞Met (X)$
21		simplrr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{})) \land x \in Y) \to R \in ℝ^{}$
22		simplrl	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to P \in X$
23		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
24		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
25	5 23 24	3syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F^{-1} : Y ⟶ X$
26		ffvelcdm	$⊢ (F^{-1} : Y ⟶ X \land x \in Y) \to F^{-1} (x) \in X$
27	25 26	sylan	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to F^{-1} (x) \in X$
28		elbl2	$⊢ ((M \in ∞Met (X) \land R \in ℝ^{*}) \land (P \in X \land F^{-1} (x) \in X)) \to (F^{-1} (x) \in (P ball (M) R) \leftrightarrow P M F^{-1} (x) < R)$
29	20 21 22 27 28	syl22anc	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F^{-1} (x) \in (P ball (M) R) \leftrightarrow P M F^{-1} (x) < R)$
30	4	simprd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to \forall x \in X \forall y \in X x M y = F (x) N F (y)$
31		oveq1	$⊢ x = P \to x M y = P M y$
32		fveq2	$⊢ x = P \to F (x) = F (P)$
33	32	oveq1d	$⊢ x = P \to F (x) N F (y) = F (P) N F (y)$
34	31 33	eqeq12d	$⊢ x = P \to (x M y = F (x) N F (y) \leftrightarrow P M y = F (P) N F (y))$
35		oveq2	$⊢ y = F^{-1} (x) \to P M y = P M F^{-1} (x)$
36		fveq2	$⊢ y = F^{-1} (x) \to F (y) = F (F^{-1} (x))$
37	36	oveq2d	$⊢ y = F^{-1} (x) \to F (P) N F (y) = F (P) N F (F^{-1} (x))$
38	35 37	eqeq12d	$⊢ y = F^{-1} (x) \to (P M y = F (P) N F (y) \leftrightarrow P M F^{-1} (x) = F (P) N F (F^{-1} (x)))$
39	34 38	rspc2v	$⊢ (P \in X \land F^{-1} (x) \in X) \to (\forall x \in X \forall y \in X x M y = F (x) N F (y) \to P M F^{-1} (x) = F (P) N F (F^{-1} (x)))$
40	39	impancom	$⊢ (P \in X \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \to (F^{-1} (x) \in X \to P M F^{-1} (x) = F (P) N F (F^{-1} (x)))$
41	12 30 40	syl2anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to (F^{-1} (x) \in X \to P M F^{-1} (x) = F (P) N F (F^{-1} (x)))$
42	41	imp	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land F^{-1} (x) \in X) \to P M F^{-1} (x) = F (P) N F (F^{-1} (x))$
43	27 42	syldan	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to P M F^{-1} (x) = F (P) N F (F^{-1} (x))$
44	43	breq1d	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (P M F^{-1} (x) < R \leftrightarrow F (P) N F (F^{-1} (x)) < R)$
45	29 44	bitrd	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F^{-1} (x) \in (P ball (M) R) \leftrightarrow F (P) N F (F^{-1} (x)) < R)$
46		f1of1	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{1-1}{⟶} Y$
47	5 46	syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F : X \underset{1-1}{⟶} Y$
48	47	adantr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to F : X \underset{1-1}{⟶} Y$
49		blssm	$⊢ (M \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (M) R \subseteq X$
50	19 12 15 49	syl3anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to P ball (M) R \subseteq X$
51	50	adantr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to P ball (M) R \subseteq X$
52		f1elima	$⊢ (F : X \underset{1-1}{⟶} Y \land F^{-1} (x) \in X \land P ball (M) R \subseteq X) \to (F (F^{-1} (x)) \in F [P ball (M) R] \leftrightarrow F^{-1} (x) \in (P ball (M) R))$
53	48 27 51 52	syl3anc	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F (F^{-1} (x)) \in F [P ball (M) R] \leftrightarrow F^{-1} (x) \in (P ball (M) R))$
54	11	adantr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to N \in ∞Met (Y)$
55	14	adantr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to F (P) \in Y$
56		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land x \in Y) \to F (F^{-1} (x)) = x$
57	5 56	sylan	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to F (F^{-1} (x)) = x$
58		simpr	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to x \in Y$
59	57 58	eqeltrd	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to F (F^{-1} (x)) \in Y$
60		elbl2	$⊢ ((N \in ∞Met (Y) \land R \in ℝ^{*}) \land (F (P) \in Y \land F (F^{-1} (x)) \in Y)) \to (F (F^{-1} (x)) \in (F (P) ball (N) R) \leftrightarrow F (P) N F (F^{-1} (x)) < R)$
61	54 21 55 59 60	syl22anc	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F (F^{-1} (x)) \in (F (P) ball (N) R) \leftrightarrow F (P) N F (F^{-1} (x)) < R)$
62	45 53 61	3bitr4d	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F (F^{-1} (x)) \in F [P ball (M) R] \leftrightarrow F (F^{-1} (x)) \in (F (P) ball (N) R))$
63	57	eleq1d	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F (F^{-1} (x)) \in F [P ball (M) R] \leftrightarrow x \in F [P ball (M) R])$
64	57	eleq1d	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (F (F^{-1} (x)) \in (F (P) ball (N) R) \leftrightarrow x \in (F (P) ball (N) R))$
65	62 63 64	3bitr3d	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \land x \in Y) \to (x \in F [P ball (M) R] \leftrightarrow x \in (F (P) ball (N) R))$
66	65	ex	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to (x \in Y \to (x \in F [P ball (M) R] \leftrightarrow x \in (F (P) ball (N) R)))$
67	10 18 66	pm5.21ndd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to (x \in F [P ball (M) R] \leftrightarrow x \in (F (P) ball (N) R))$
68	67	eqrdv	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (P \in X \land R \in ℝ^{*})) \to F [P ball (M) R] = F (P) ball (N) R$

Metamath Proof Explorer

Theorem ismtyima

Proof