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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	trgcgrg.m	⊢ − = ( dist ‘ 𝐺 )
	trgcgrg.r	⊢ ∼ = ( cgrG ‘ 𝐺 )
	trgcgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	iscgrglt.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	iscgrglt.a	⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑃 )
	iscgrglt.b	⊢ ( 𝜑 → 𝐵 : 𝐷 ⟶ 𝑃 )
Assertion	iscgrglt	⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		trgcgrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		trgcgrg.m	⊢ − = ( dist ‘ 𝐺 )
3		trgcgrg.r	⊢ ∼ = ( cgrG ‘ 𝐺 )
4		trgcgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		iscgrglt.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
6		iscgrglt.a	⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑃 )
7		iscgrglt.b	⊢ ( 𝜑 → 𝐵 : 𝐷 ⟶ 𝑃 )
8	1 2 3 4 5 6 7	iscgrgd	⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
9		simp2	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴 ) ) ∧ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ∧ 𝑖 < 𝑗 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
10	9	3exp	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) → ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
11	10	ralimdvva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) → ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
12		breq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 < 𝑙 ↔ 𝑖 < 𝑙 ) )
13		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑖 ) )
14	13	oveq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑙 ) ) )
15		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
16	15	oveq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑙 ) ) )
17	14 16	eqeq12d	⊢ ( 𝑘 = 𝑖 → ( ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ↔ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑙 ) ) ) )
18	12 17	imbi12d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ↔ ( 𝑖 < 𝑙 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) )
19		breq2	⊢ ( 𝑙 = 𝑗 → ( 𝑖 < 𝑙 ↔ 𝑖 < 𝑗 ) )
20		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐴 ‘ 𝑙 ) = ( 𝐴 ‘ 𝑗 ) )
21	20	oveq2d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) )
22		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐵 ‘ 𝑙 ) = ( 𝐵 ‘ 𝑗 ) )
23	22	oveq2d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
24	21 23	eqeq12d	⊢ ( 𝑙 = 𝑗 → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑙 ) ) ↔ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
25	19 24	imbi12d	⊢ ( 𝑙 = 𝑗 → ( ( 𝑖 < 𝑙 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑙 ) ) ) ↔ ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
26	18 25	cbvral2vw	⊢ ( ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
27		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ dom 𝐴 )
28		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ dom 𝐴 )
29		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 < 𝑗 ) → ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) )
30	27 28 29	jca31	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 < 𝑗 ) → ( ( 𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴 ) ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) )
31		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 )
32	18 25	rspc2va	⊢ ( ( ( 𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴 ) ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) → ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
33	30 31 32	sylc	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 < 𝑗 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
34		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
35	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → 𝐺 ∈ TarskiG )
36	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝐴 : 𝐷 ⟶ 𝑃 )
37		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑖 ∈ dom 𝐴 )
38	36	fdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → dom 𝐴 = 𝐷 )
39	37 38	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑖 ∈ 𝐷 )
40	36 39	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝑃 )
41	40	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝑃 )
42	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝐵 : 𝐷 ⟶ 𝑃 )
43	42 39	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → ( 𝐵 ‘ 𝑖 ) ∈ 𝑃 )
44	43	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( 𝐵 ‘ 𝑖 ) ∈ 𝑃 )
45	1 2 34 35 41 44	tgcgrtriv	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
46		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → 𝑖 = 𝑗 )
47	46	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑗 ) )
48	47	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) )
49	46	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑗 ) )
50	49	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
51	45 48 50	3eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
52	51	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
53	4	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → 𝐺 ∈ TarskiG )
54		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑗 ∈ dom 𝐴 )
55	54 38	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑗 ∈ 𝐷 )
56	36 55	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → ( 𝐴 ‘ 𝑗 ) ∈ 𝑃 )
57	56	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐴 ‘ 𝑗 ) ∈ 𝑃 )
58	57	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐴 ‘ 𝑗 ) ∈ 𝑃 )
59	40	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝑃 )
60	59	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝑃 )
61	42 55	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → ( 𝐵 ‘ 𝑗 ) ∈ 𝑃 )
62	61	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐵 ‘ 𝑗 ) ∈ 𝑃 )
63	62	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐵 ‘ 𝑗 ) ∈ 𝑃 )
64	43	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐵 ‘ 𝑖 ) ∈ 𝑃 )
65	64	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( 𝐵 ‘ 𝑖 ) ∈ 𝑃 )
66		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → 𝑗 ∈ dom 𝐴 )
67		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → 𝑖 ∈ dom 𝐴 )
68		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) )
69	66 67 68	jca31	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( ( 𝑗 ∈ dom 𝐴 ∧ 𝑖 ∈ dom 𝐴 ) ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) )
70		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → 𝑗 < 𝑖 )
71		breq1	⊢ ( 𝑘 = 𝑗 → ( 𝑘 < 𝑙 ↔ 𝑗 < 𝑙 ) )
72		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑗 ) )
73	72	oveq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑙 ) ) )
74		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑗 ) )
75	74	oveq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑙 ) ) )
76	73 75	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ↔ ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑙 ) ) ) )
77	71 76	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ↔ ( 𝑗 < 𝑙 → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) )
78		breq2	⊢ ( 𝑙 = 𝑖 → ( 𝑗 < 𝑙 ↔ 𝑗 < 𝑖 ) )
79		fveq2	⊢ ( 𝑙 = 𝑖 → ( 𝐴 ‘ 𝑙 ) = ( 𝐴 ‘ 𝑖 ) )
80	79	oveq2d	⊢ ( 𝑙 = 𝑖 → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑖 ) ) )
81		fveq2	⊢ ( 𝑙 = 𝑖 → ( 𝐵 ‘ 𝑙 ) = ( 𝐵 ‘ 𝑖 ) )
82	81	oveq2d	⊢ ( 𝑙 = 𝑖 → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑖 ) ) )
83	80 82	eqeq12d	⊢ ( 𝑙 = 𝑖 → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑙 ) ) ↔ ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑖 ) ) ) )
84	78 83	imbi12d	⊢ ( 𝑙 = 𝑖 → ( ( 𝑗 < 𝑙 → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑙 ) ) ) ↔ ( 𝑗 < 𝑖 → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) )
85	77 84	rspc2va	⊢ ( ( ( 𝑗 ∈ dom 𝐴 ∧ 𝑖 ∈ dom 𝐴 ) ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) → ( 𝑗 < 𝑖 → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑖 ) ) ) )
86	69 70 85	sylc	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑖 ) ) )
87	1 2 34 53 58 60 63 65 86	tgcgrcomlr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) ∧ 𝑗 < 𝑖 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
88	6	fdmd	⊢ ( 𝜑 → dom 𝐴 = 𝐷 )
89	88 5	eqsstrd	⊢ ( 𝜑 → dom 𝐴 ⊆ ℝ )
90	89	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → dom 𝐴 ⊆ ℝ )
91		simplr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑖 ∈ dom 𝐴 )
92	90 91	sseldd	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑖 ∈ ℝ )
93		simpr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑗 ∈ dom 𝐴 )
94	90 93	sseldd	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → 𝑗 ∈ ℝ )
95	92 94	lttri4d	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → ( 𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖 ) )
96	33 52 87 95	mpjao3dan	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ 𝑖 ∈ dom 𝐴 ) ∧ 𝑗 ∈ dom 𝐴 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
97	96	anasss	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) ∧ ( 𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴 ) ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
98	97	ralrimivva	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) ) → ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
99	98	ex	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ dom 𝐴 ∀ 𝑙 ∈ dom 𝐴 ( 𝑘 < 𝑙 → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑙 ) ) ) → ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
100	26 99	biimtrrid	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) → ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
101	11 100	impbid	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
102	8 101	bitrd	⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )