ismtyres

Description: A restriction of an isometry is an isometry. The condition A C_ X is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypotheses	ismtyres.2	$⊢ B = F [A]$
	ismtyres.3	$⊢ S = {M ↾}_{(A \times A)}$
	ismtyres.4	$⊢ T = {N ↾}_{(B \times B)}$
Assertion	ismtyres	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to {F ↾}_{A} \in (S Ismty T)$

Proof

Step	Hyp	Ref	Expression
1		ismtyres.2	$⊢ B = F [A]$
2		ismtyres.3	$⊢ S = {M ↾}_{(A \times A)}$
3		ismtyres.4	$⊢ T = {N ↾}_{(B \times B)}$
4		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)))$
5	4	simprbda	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land F \in (M Ismty N)) \to F : X \underset{1-1 onto}{⟶} Y$
6	5	adantrr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to F : X \underset{1-1 onto}{⟶} Y$
7		f1of1	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{1-1}{⟶} Y$
8	6 7	syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to F : X \underset{1-1}{⟶} Y$
9		simprr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to A \subseteq X$
10		f1ores	$⊢ (F : X \underset{1-1}{⟶} Y \land A \subseteq X) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A]$
11	8 9 10	syl2anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A]$
12	4	biimpa	$⊢ ((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))$
13	12	adantrr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \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))$
14		ssel	$⊢ A \subseteq X \to (u \in A \to u \in X)$
15		ssel	$⊢ A \subseteq X \to (v \in A \to v \in X)$
16	14 15	anim12d	$⊢ A \subseteq X \to ((u \in A \land v \in A) \to (u \in X \land v \in X))$
17	16	imp	$⊢ (A \subseteq X \land (u \in A \land v \in A)) \to (u \in X \land v \in X)$
18		oveq1	$⊢ x = u \to x M y = u M y$
19		fveq2	$⊢ x = u \to F (x) = F (u)$
20	19	oveq1d	$⊢ x = u \to F (x) N F (y) = F (u) N F (y)$
21	18 20	eqeq12d	$⊢ x = u \to (x M y = F (x) N F (y) \leftrightarrow u M y = F (u) N F (y))$
22		oveq2	$⊢ y = v \to u M y = u M v$
23		fveq2	$⊢ y = v \to F (y) = F (v)$
24	23	oveq2d	$⊢ y = v \to F (u) N F (y) = F (u) N F (v)$
25	22 24	eqeq12d	$⊢ y = v \to (u M y = F (u) N F (y) \leftrightarrow u M v = F (u) N F (v))$
26	21 25	rspc2v	$⊢ (u \in X \land v \in X) \to (\forall x \in X \forall y \in X x M y = F (x) N F (y) \to u M v = F (u) N F (v))$
27	17 26	syl	$⊢ (A \subseteq X \land (u \in A \land v \in A)) \to (\forall x \in X \forall y \in X x M y = F (x) N F (y) \to u M v = F (u) N F (v))$
28	27	imp	$⊢ ((A \subseteq X \land (u \in A \land v \in A)) \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \to u M v = F (u) N F (v)$
29	28	an32s	$⊢ ((A \subseteq X \land \forall x \in X \forall y \in X x M y = F (x) N F (y)) \land (u \in A \land v \in A)) \to u M v = F (u) N F (v)$
30	29	adantlrl	$⊢ ((A \subseteq X \land (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 A \land v \in A)) \to u M v = F (u) N F (v)$
31	30	adantlll	$⊢ ((((M \in ∞Met (X) \land N \in ∞Met (Y)) \land A \subseteq X) \land (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 A \land v \in A)) \to u M v = F (u) N F (v)$
32	2	oveqi	$⊢ u S v = u ({M ↾}_{(A \times A)}) v$
33		ovres	$⊢ (u \in A \land v \in A) \to u ({M ↾}_{(A \times A)}) v = u M v$
34	32 33	syl5eq	$⊢ (u \in A \land v \in A) \to u S v = u M v$
35	34	adantl	$⊢ ((((M \in ∞Met (X) \land N \in ∞Met (Y)) \land A \subseteq X) \land (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 A \land v \in A)) \to u S v = u M v$
36		fvres	$⊢ u \in A \to ({F ↾}_{A}) (u) = F (u)$
37	36	ad2antrl	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to ({F ↾}_{A}) (u) = F (u)$
38		fvres	$⊢ v \in A \to ({F ↾}_{A}) (v) = F (v)$
39	38	ad2antll	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to ({F ↾}_{A}) (v) = F (v)$
40	37 39	oveq12d	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v) = F (u) T F (v)$
41	3	oveqi	$⊢ F (u) T F (v) = F (u) ({N ↾}_{(B \times B)}) F (v)$
42		f1ofun	$⊢ F : X \underset{1-1 onto}{⟶} Y \to Fun F$
43	42	adantl	$⊢ (A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \to Fun F$
44		f1odm	$⊢ F : X \underset{1-1 onto}{⟶} Y \to dom F = X$
45	44	sseq2d	$⊢ F : X \underset{1-1 onto}{⟶} Y \to (A \subseteq dom F \leftrightarrow A \subseteq X)$
46	45	biimparc	$⊢ (A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \to A \subseteq dom F$
47		funfvima2	$⊢ (Fun F \land A \subseteq dom F) \to (u \in A \to F (u) \in F [A])$
48	43 46 47	syl2anc	$⊢ (A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \to (u \in A \to F (u) \in F [A])$
49	48	imp	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land u \in A) \to F (u) \in F [A]$
50	49 1	eleqtrrdi	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land u \in A) \to F (u) \in B$
51	50	adantrr	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to F (u) \in B$
52		funfvima2	$⊢ (Fun F \land A \subseteq dom F) \to (v \in A \to F (v) \in F [A])$
53	43 46 52	syl2anc	$⊢ (A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \to (v \in A \to F (v) \in F [A])$
54	53	imp	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land v \in A) \to F (v) \in F [A]$
55	54 1	eleqtrrdi	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land v \in A) \to F (v) \in B$
56	55	adantrl	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to F (v) \in B$
57	51 56	ovresd	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to F (u) ({N ↾}_{(B \times B)}) F (v) = F (u) N F (v)$
58	41 57	syl5eq	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to F (u) T F (v) = F (u) N F (v)$
59	40 58	eqtrd	$⊢ ((A \subseteq X \land F : X \underset{1-1 onto}{⟶} Y) \land (u \in A \land v \in A)) \to ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v) = F (u) N F (v)$
60	59	adantlrr	$⊢ ((A \subseteq X \land (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 A \land v \in A)) \to ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v) = F (u) N F (v)$
61	60	adantlll	$⊢ ((((M \in ∞Met (X) \land N \in ∞Met (Y)) \land A \subseteq X) \land (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 A \land v \in A)) \to ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v) = F (u) N F (v)$
62	31 35 61	3eqtr4d	$⊢ ((((M \in ∞Met (X) \land N \in ∞Met (Y)) \land A \subseteq X) \land (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 A \land v \in A)) \to u S v = ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v)$
63	62	ralrimivva	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y)) \land A \subseteq X) \land (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 A \forall v \in A u S v = ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v)$
64	63	adantlrl	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \land (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 A \forall v \in A u S v = ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v)$
65	13 64	mpdan	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to \forall u \in A \forall v \in A u S v = ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v)$
66		xmetres2	$⊢ (M \in ∞Met (X) \land A \subseteq X) \to {M ↾}_{(A \times A)} \in ∞Met (A)$
67	2 66	eqeltrid	$⊢ (M \in ∞Met (X) \land A \subseteq X) \to S \in ∞Met (A)$
68	67	ad2ant2rl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to S \in ∞Met (A)$
69		simplr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to N \in ∞Met (Y)$
70		imassrn	$⊢ F [A] \subseteq ran F$
71	1 70	eqsstri	$⊢ B \subseteq ran F$
72		f1ofo	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{onto}{⟶} Y$
73		forn	$⊢ F : X \underset{onto}{⟶} Y \to ran F = Y$
74	6 72 73	3syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to ran F = Y$
75	71 74	sseqtrid	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to B \subseteq Y$
76		xmetres2	$⊢ (N \in ∞Met (Y) \land B \subseteq Y) \to {N ↾}_{(B \times B)} \in ∞Met (B)$
77	69 75 76	syl2anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to {N ↾}_{(B \times B)} \in ∞Met (B)$
78	3 77	eqeltrid	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to T \in ∞Met (B)$
79	1	fveq2i	$⊢ ∞Met (B) = ∞Met (F [A])$
80	78 79	eleqtrdi	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to T \in ∞Met (F [A])$
81		isismty	$⊢ (S \in ∞Met (A) \land T \in ∞Met (F [A])) \to ({F ↾}_{A} \in (S Ismty T) \leftrightarrow (({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A] \land \forall u \in A \forall v \in A u S v = ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v)))$
82	68 80 81	syl2anc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to ({F ↾}_{A} \in (S Ismty T) \leftrightarrow (({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A] \land \forall u \in A \forall v \in A u S v = ({F ↾}_{A}) (u) T ({F ↾}_{A}) (v)))$
83	11 65 82	mpbir2and	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land (F \in (M Ismty N) \land A \subseteq X)) \to {F ↾}_{A} \in (S Ismty T)$

Metamath Proof Explorer

Theorem ismtyres

Proof