cnre2csqlem

	Ref	Expression
Hypotheses	cnre2csqlem.1	$⊢ {G ↾}_{ℝ^{2}} = H \circ F$
	cnre2csqlem.2	$⊢ F Fn ℝ^{2}$
	cnre2csqlem.3	$⊢ G Fn V$
	cnre2csqlem.4	$⊢ x \in ℝ^{2} \to G (x) \in ℝ$
	cnre2csqlem.5	$⊢ (x \in ran F \land y \in ran F) \to H (x - y) = H (x) - H (y)$
Assertion	cnre2csqlem	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)] \to \|H (F (Y) - F (X))\| < D)$

Proof

Step	Hyp	Ref	Expression
1		cnre2csqlem.1	$⊢ {G ↾}_{ℝ^{2}} = H \circ F$
2		cnre2csqlem.2	$⊢ F Fn ℝ^{2}$
3		cnre2csqlem.3	$⊢ G Fn V$
4		cnre2csqlem.4	$⊢ x \in ℝ^{2} \to G (x) \in ℝ$
5		cnre2csqlem.5	$⊢ (x \in ran F \land y \in ran F) \to H (x - y) = H (x) - H (y)$
6		ssv	$⊢ ℝ^{2} \subseteq V$
7		fnssres	$⊢ (G Fn V \land ℝ^{2} \subseteq V) \to ({G ↾}_{ℝ^{2}}) Fn ℝ^{2}$
8	3 6 7	mp2an	$⊢ ({G ↾}_{ℝ^{2}}) Fn ℝ^{2}$
9		elpreima	$⊢ ({G ↾}_{ℝ^{2}}) Fn ℝ^{2} \to (Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)] \leftrightarrow (Y \in ℝ^{2} \land ({G ↾}_{ℝ^{2}}) (Y) \in (G (X) - D, G (X) + D)))$
10	8 9	mp1i	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)] \leftrightarrow (Y \in ℝ^{2} \land ({G ↾}_{ℝ^{2}}) (Y) \in (G (X) - D, G (X) + D)))$
11	10	simplbda	$⊢ ((X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \land Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)]) \to ({G ↾}_{ℝ^{2}}) (Y) \in (G (X) - D, G (X) + D)$
12	11	ex	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)] \to ({G ↾}_{ℝ^{2}}) (Y) \in (G (X) - D, G (X) + D))$
13		simp2	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to Y \in ℝ^{2}$
14		fvres	$⊢ Y \in ℝ^{2} \to ({G ↾}_{ℝ^{2}}) (Y) = G (Y)$
15	13 14	syl	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to ({G ↾}_{ℝ^{2}}) (Y) = G (Y)$
16	15	eleq1d	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (({G ↾}_{ℝ^{2}}) (Y) \in (G (X) - D, G (X) + D) \leftrightarrow G (Y) \in (G (X) - D, G (X) + D))$
17		simp1	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to X \in ℝ^{2}$
18		fveq2	$⊢ x = X \to G (x) = G (X)$
19	18	eleq1d	$⊢ x = X \to (G (x) \in ℝ \leftrightarrow G (X) \in ℝ)$
20	19 4	vtoclga	$⊢ X \in ℝ^{2} \to G (X) \in ℝ$
21	17 20	syl	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (X) \in ℝ$
22		simp3	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to D \in ℝ^{+}$
23	22	rpred	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to D \in ℝ$
24	21 23	resubcld	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (X) - D \in ℝ$
25	24	rexrd	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (X) - D \in ℝ^{*}$
26	21 23	readdcld	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (X) + D \in ℝ$
27	26	rexrd	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (X) + D \in ℝ^{*}$
28		elioo2	$⊢ (G (X) - D \in ℝ^{} \land G (X) + D \in ℝ^{}) \to (G (Y) \in (G (X) - D, G (X) + D) \leftrightarrow (G (Y) \in ℝ \land G (X) - D < G (Y) \land G (Y) < G (X) + D))$
29	25 27 28	syl2anc	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (G (Y) \in (G (X) - D, G (X) + D) \leftrightarrow (G (Y) \in ℝ \land G (X) - D < G (Y) \land G (Y) < G (X) + D))$
30	29	biimpa	$⊢ ((X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \land G (Y) \in (G (X) - D, G (X) + D)) \to (G (Y) \in ℝ \land G (X) - D < G (Y) \land G (Y) < G (X) + D)$
31	30	simp2d	$⊢ ((X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \land G (Y) \in (G (X) - D, G (X) + D)) \to G (X) - D < G (Y)$
32	30	simp3d	$⊢ ((X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \land G (Y) \in (G (X) - D, G (X) + D)) \to G (Y) < G (X) + D$
33	31 32	jca	$⊢ ((X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \land G (Y) \in (G (X) - D, G (X) + D)) \to (G (X) - D < G (Y) \land G (Y) < G (X) + D)$
34	33	ex	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (G (Y) \in (G (X) - D, G (X) + D) \to (G (X) - D < G (Y) \land G (Y) < G (X) + D))$
35	16 34	sylbid	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (({G ↾}_{ℝ^{2}}) (Y) \in (G (X) - D, G (X) + D) \to (G (X) - D < G (Y) \land G (Y) < G (X) + D))$
36		fveq2	$⊢ x = Y \to G (x) = G (Y)$
37	36	eleq1d	$⊢ x = Y \to (G (x) \in ℝ \leftrightarrow G (Y) \in ℝ)$
38	37 4	vtoclga	$⊢ Y \in ℝ^{2} \to G (Y) \in ℝ$
39	13 38	syl	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (Y) \in ℝ$
40		absdiflt	$⊢ (G (Y) \in ℝ \land G (X) \in ℝ \land D \in ℝ) \to (\|G (Y) - G (X)\| < D \leftrightarrow (G (X) - D < G (Y) \land G (Y) < G (X) + D))$
41	40	biimprd	$⊢ (G (Y) \in ℝ \land G (X) \in ℝ \land D \in ℝ) \to ((G (X) - D < G (Y) \land G (Y) < G (X) + D) \to \|G (Y) - G (X)\| < D)$
42	39 21 23 41	syl3anc	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to ((G (X) - D < G (Y) \land G (Y) < G (X) + D) \to \|G (Y) - G (X)\| < D)$
43	12 35 42	3syld	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)] \to \|G (Y) - G (X)\| < D)$
44		fnfvelrn	$⊢ (F Fn ℝ^{2} \land Y \in ℝ^{2}) \to F (Y) \in ran F$
45	2 13 44	sylancr	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to F (Y) \in ran F$
46		fnfvelrn	$⊢ (F Fn ℝ^{2} \land X \in ℝ^{2}) \to F (X) \in ran F$
47	2 17 46	sylancr	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to F (X) \in ran F$
48		fvoveq1	$⊢ x = F (Y) \to H (x - y) = H (F (Y) - y)$
49		fveq2	$⊢ x = F (Y) \to H (x) = H (F (Y))$
50	49	oveq1d	$⊢ x = F (Y) \to H (x) - H (y) = H (F (Y)) - H (y)$
51	48 50	eqeq12d	$⊢ x = F (Y) \to (H (x - y) = H (x) - H (y) \leftrightarrow H (F (Y) - y) = H (F (Y)) - H (y))$
52		oveq2	$⊢ y = F (X) \to F (Y) - y = F (Y) - F (X)$
53	52	fveq2d	$⊢ y = F (X) \to H (F (Y) - y) = H (F (Y) - F (X))$
54		fveq2	$⊢ y = F (X) \to H (y) = H (F (X))$
55	54	oveq2d	$⊢ y = F (X) \to H (F (Y)) - H (y) = H (F (Y)) - H (F (X))$
56	53 55	eqeq12d	$⊢ y = F (X) \to (H (F (Y) - y) = H (F (Y)) - H (y) \leftrightarrow H (F (Y) - F (X)) = H (F (Y)) - H (F (X)))$
57	51 56 5	vtocl2ga	$⊢ (F (Y) \in ran F \land F (X) \in ran F) \to H (F (Y) - F (X)) = H (F (Y)) - H (F (X))$
58	45 47 57	syl2anc	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to H (F (Y) - F (X)) = H (F (Y)) - H (F (X))$
59	1	fveq1i	$⊢ ({G ↾}_{ℝ^{2}}) (Y) = (H \circ F) (Y)$
60		fvco2	$⊢ (F Fn ℝ^{2} \land Y \in ℝ^{2}) \to (H \circ F) (Y) = H (F (Y))$
61	2 13 60	sylancr	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (H \circ F) (Y) = H (F (Y))$
62	59 15 61	3eqtr3a	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (Y) = H (F (Y))$
63	1	fveq1i	$⊢ ({G ↾}_{ℝ^{2}}) (X) = (H \circ F) (X)$
64		fvres	$⊢ X \in ℝ^{2} \to ({G ↾}_{ℝ^{2}}) (X) = G (X)$
65	17 64	syl	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to ({G ↾}_{ℝ^{2}}) (X) = G (X)$
66		fvco2	$⊢ (F Fn ℝ^{2} \land X \in ℝ^{2}) \to (H \circ F) (X) = H (F (X))$
67	2 17 66	sylancr	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (H \circ F) (X) = H (F (X))$
68	63 65 67	3eqtr3a	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (X) = H (F (X))$
69	62 68	oveq12d	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to G (Y) - G (X) = H (F (Y)) - H (F (X))$
70	58 69	eqtr4d	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to H (F (Y) - F (X)) = G (Y) - G (X)$
71	70	fveq2d	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to \|H (F (Y) - F (X))\| = \|G (Y) - G (X)\|$
72	71	breq1d	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (\|H (F (Y) - F (X))\| < D \leftrightarrow \|G (Y) - G (X)\| < D)$
73	43 72	sylibrd	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({G ↾}_{ℝ^{2}})}^{-1} [(G (X) - D, G (X) + D)] \to \|H (F (Y) - F (X))\| < D)$

Metamath Proof Explorer

Theorem cnre2csqlem

Proof