Metamath Proof Explorer

Theorem cnre2csqlem

Description: Lemma for cnre2csqima . (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Hypotheses cnre2csqlem.1 ⊢G↾ℝ2=H∘F
cnre2csqlem.2 ⊢FFnℝ2
cnre2csqlem.3 ⊢GFnV
cnre2csqlem.4 ⊢x∈ℝ2→G⁡x∈ℝ
cnre2csqlem.5 ⊢x∈ran⁡F∧y∈ran⁡F→H⁡x−y=H⁡x−H⁡y
Assertion cnre2csqlem ⊢X∈ℝ2∧Y∈ℝ2∧D∈ℝ+→Y∈G↾ℝ2-1G⁡X−DG⁡X+D→H⁡F⁡Y−F⁡X<D

Proof

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