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	$⊢ \underset{˙}{-} = dist (G)$
	trgcgrg.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	trgcgrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgrglt.d	$⊢ φ \to D \subseteq ℝ$
	iscgrglt.a	$⊢ φ \to A : D ⟶ P$
	iscgrglt.b	$⊢ φ \to B : D ⟶ P$
Assertion	iscgrglt	$⊢ φ \to (A \underset{˙}{\sim} B \leftrightarrow \forall i \in dom A \forall j \in dom A (i < j \to A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j)))$

Proof

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

Metamath Proof Explorer

Theorem iscgrglt

Proof