Metamath Proof Explorer


Theorem iscgrglt

Description: The property for two sequences A and B of points to be congruent, where the congruence is only required for indices verifying a less-than relation. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Hypotheses trgcgrg.p P = Base G
trgcgrg.m - ˙ = dist G
trgcgrg.r ˙ = 𝒢 G
trgcgrg.g φ G 𝒢 Tarski
iscgrglt.d φ D
iscgrglt.a φ A : D P
iscgrglt.b φ B : D P
Assertion iscgrglt φ A ˙ B i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j

Proof

Step Hyp Ref Expression
1 trgcgrg.p P = Base G
2 trgcgrg.m - ˙ = dist G
3 trgcgrg.r ˙ = 𝒢 G
4 trgcgrg.g φ G 𝒢 Tarski
5 iscgrglt.d φ D
6 iscgrglt.a φ A : D P
7 iscgrglt.b φ B : D P
8 1 2 3 4 5 6 7 iscgrgd φ A ˙ B i dom A j dom A A i - ˙ A j = B i - ˙ B j
9 simp2 φ i dom A j dom A A i - ˙ A j = B i - ˙ B j i < j A i - ˙ A j = B i - ˙ B j
10 9 3exp φ i dom A j dom A A i - ˙ A j = B i - ˙ B j i < j A i - ˙ A j = B i - ˙ B j
11 10 ralimdvva φ i dom A j dom A A i - ˙ A j = B i - ˙ B j i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j
12 breq1 k = i k < l i < l
13 fveq2 k = i A k = A i
14 13 oveq1d k = i A k - ˙ A l = A i - ˙ A l
15 fveq2 k = i B k = B i
16 15 oveq1d k = i B k - ˙ B l = B i - ˙ B l
17 14 16 eqeq12d k = i A k - ˙ A l = B k - ˙ B l A i - ˙ A l = B i - ˙ B l
18 12 17 imbi12d k = i k < l A k - ˙ A l = B k - ˙ B l i < l A i - ˙ A l = B i - ˙ B l
19 breq2 l = j i < l i < j
20 fveq2 l = j A l = A j
21 20 oveq2d l = j A i - ˙ A l = A i - ˙ A j
22 fveq2 l = j B l = B j
23 22 oveq2d l = j B i - ˙ B l = B i - ˙ B j
24 21 23 eqeq12d l = j A i - ˙ A l = B i - ˙ B l A i - ˙ A j = B i - ˙ B j
25 19 24 imbi12d l = j i < l A i - ˙ A l = B i - ˙ B l i < j A i - ˙ A j = B i - ˙ B j
26 18 25 cbvral2vw k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j
27 simpllr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j i dom A
28 simplr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j j dom A
29 simp-4r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l
30 27 28 29 jca31 φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j i dom A j dom A k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l
31 simpr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j i < j
32 18 25 rspc2va i dom A j dom A k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i < j A i - ˙ A j = B i - ˙ B j
33 30 31 32 sylc φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j
34 eqid Itv G = Itv G
35 4 ad3antrrr φ i dom A j dom A i = j G 𝒢 Tarski
36 6 ad2antrr φ i dom A j dom A A : D P
37 simplr φ i dom A j dom A i dom A
38 36 fdmd φ i dom A j dom A dom A = D
39 37 38 eleqtrd φ i dom A j dom A i D
40 36 39 ffvelrnd φ i dom A j dom A A i P
41 40 adantr φ i dom A j dom A i = j A i P
42 7 ad2antrr φ i dom A j dom A B : D P
43 42 39 ffvelrnd φ i dom A j dom A B i P
44 43 adantr φ i dom A j dom A i = j B i P
45 1 2 34 35 41 44 tgcgrtriv φ i dom A j dom A i = j A i - ˙ A i = B i - ˙ B i
46 simpr φ i dom A j dom A i = j i = j
47 46 fveq2d φ i dom A j dom A i = j A i = A j
48 47 oveq2d φ i dom A j dom A i = j A i - ˙ A i = A i - ˙ A j
49 46 fveq2d φ i dom A j dom A i = j B i = B j
50 49 oveq2d φ i dom A j dom A i = j B i - ˙ B i = B i - ˙ B j
51 45 48 50 3eqtr3d φ i dom A j dom A i = j A i - ˙ A j = B i - ˙ B j
52 51 adantl3r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i = j A i - ˙ A j = B i - ˙ B j
53 4 ad4antr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i G 𝒢 Tarski
54 simpr φ i dom A j dom A j dom A
55 54 38 eleqtrd φ i dom A j dom A j D
56 36 55 ffvelrnd φ i dom A j dom A A j P
57 56 adantr φ i dom A j dom A j < i A j P
58 57 adantl3r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i A j P
59 40 adantr φ i dom A j dom A j < i A i P
60 59 adantl3r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i A i P
61 42 55 ffvelrnd φ i dom A j dom A B j P
62 61 adantr φ i dom A j dom A j < i B j P
63 62 adantl3r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i B j P
64 43 adantr φ i dom A j dom A j < i B i P
65 64 adantl3r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i B i P
66 simplr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i j dom A
67 simpllr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i i dom A
68 simp-4r φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l
69 66 67 68 jca31 φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i j dom A i dom A k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l
70 simpr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i j < i
71 breq1 k = j k < l j < l
72 fveq2 k = j A k = A j
73 72 oveq1d k = j A k - ˙ A l = A j - ˙ A l
74 fveq2 k = j B k = B j
75 74 oveq1d k = j B k - ˙ B l = B j - ˙ B l
76 73 75 eqeq12d k = j A k - ˙ A l = B k - ˙ B l A j - ˙ A l = B j - ˙ B l
77 71 76 imbi12d k = j k < l A k - ˙ A l = B k - ˙ B l j < l A j - ˙ A l = B j - ˙ B l
78 breq2 l = i j < l j < i
79 fveq2 l = i A l = A i
80 79 oveq2d l = i A j - ˙ A l = A j - ˙ A i
81 fveq2 l = i B l = B i
82 81 oveq2d l = i B j - ˙ B l = B j - ˙ B i
83 80 82 eqeq12d l = i A j - ˙ A l = B j - ˙ B l A j - ˙ A i = B j - ˙ B i
84 78 83 imbi12d l = i j < l A j - ˙ A l = B j - ˙ B l j < i A j - ˙ A i = B j - ˙ B i
85 77 84 rspc2va j dom A i dom A k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l j < i A j - ˙ A i = B j - ˙ B i
86 69 70 85 sylc φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i A j - ˙ A i = B j - ˙ B i
87 1 2 34 53 58 60 63 65 86 tgcgrcomlr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j < i A i - ˙ A j = B i - ˙ B j
88 6 fdmd φ dom A = D
89 88 5 eqsstrd φ dom A
90 89 ad3antrrr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A dom A
91 simplr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i dom A
92 90 91 sseldd φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i
93 simpr φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j dom A
94 90 93 sseldd φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A j
95 92 94 lttri4d φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A i < j i = j j < i
96 33 52 87 95 mpjao3dan φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A A i - ˙ A j = B i - ˙ B j
97 96 anasss φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A A i - ˙ A j = B i - ˙ B j
98 97 ralrimivva φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A A i - ˙ A j = B i - ˙ B j
99 98 ex φ k dom A l dom A k < l A k - ˙ A l = B k - ˙ B l i dom A j dom A A i - ˙ A j = B i - ˙ B j
100 26 99 syl5bir φ i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j i dom A j dom A A i - ˙ A j = B i - ˙ B j
101 11 100 impbid φ i dom A j dom A A i - ˙ A j = B i - ˙ B j i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j
102 8 101 bitrd φ A ˙ B i dom A j dom A i < j A i - ˙ A j = B i - ˙ B j