Step | Hyp | Ref
| Expression |
1 | | trgcgrg.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | trgcgrg.m |
. . 3
⊢ − =
(dist‘𝐺) |
3 | | trgcgrg.r |
. . 3
⊢ ∼ =
(cgrG‘𝐺) |
4 | | trgcgrg.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | | iscgrglt.d |
. . 3
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
6 | | iscgrglt.a |
. . 3
⊢ (𝜑 → 𝐴:𝐷⟶𝑃) |
7 | | iscgrglt.b |
. . 3
⊢ (𝜑 → 𝐵:𝐷⟶𝑃) |
8 | 1, 2, 3, 4, 5, 6, 7 | iscgrgd 25208 |
. 2
⊢ (𝜑 → (𝐴 ∼ 𝐵 ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
9 | | simp2 1055 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴)) ∧ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)) ∧ 𝑖 < 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
10 | 9 | 3expia 1259 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴)) ∧ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) → (𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
11 | 10 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴)) → (((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)) → (𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
12 | 11 | ralimdvva 2947 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)) → ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
13 | | breq1 4586 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (𝑘 < 𝑙 ↔ 𝑖 < 𝑙)) |
14 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖)) |
15 | 14 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐴‘𝑖) − (𝐴‘𝑙))) |
16 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖)) |
17 | 16 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → ((𝐵‘𝑘) − (𝐵‘𝑙)) = ((𝐵‘𝑖) − (𝐵‘𝑙))) |
18 | 15, 17 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑙)) = ((𝐵‘𝑖) − (𝐵‘𝑙)))) |
19 | 13, 18 | imbi12d 333 |
. . . . 5
⊢ (𝑘 = 𝑖 → ((𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))) ↔ (𝑖 < 𝑙 → ((𝐴‘𝑖) − (𝐴‘𝑙)) = ((𝐵‘𝑖) − (𝐵‘𝑙))))) |
20 | | breq2 4587 |
. . . . . 6
⊢ (𝑙 = 𝑗 → (𝑖 < 𝑙 ↔ 𝑖 < 𝑗)) |
21 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑙 = 𝑗 → (𝐴‘𝑙) = (𝐴‘𝑗)) |
22 | 21 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑙 = 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑙)) = ((𝐴‘𝑖) − (𝐴‘𝑗))) |
23 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑙 = 𝑗 → (𝐵‘𝑙) = (𝐵‘𝑗)) |
24 | 23 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑙 = 𝑗 → ((𝐵‘𝑖) − (𝐵‘𝑙)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
25 | 22, 24 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑙 = 𝑗 → (((𝐴‘𝑖) − (𝐴‘𝑙)) = ((𝐵‘𝑖) − (𝐵‘𝑙)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
26 | 20, 25 | imbi12d 333 |
. . . . 5
⊢ (𝑙 = 𝑗 → ((𝑖 < 𝑙 → ((𝐴‘𝑖) − (𝐴‘𝑙)) = ((𝐵‘𝑖) − (𝐵‘𝑙))) ↔ (𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
27 | 19, 26 | cbvral2v 3155 |
. . . 4
⊢
(∀𝑘 ∈
dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
28 | | simpllr 795 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 < 𝑗) → 𝑖 ∈ dom 𝐴) |
29 | | simplr 788 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 < 𝑗) → 𝑗 ∈ dom 𝐴) |
30 | | simp-4r 803 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 < 𝑗) → ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) |
31 | 28, 29, 30 | jca31 555 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 < 𝑗) → ((𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴) ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))))) |
32 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗) |
33 | 19, 26 | rspc2v 3293 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴) → (∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))) → (𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
34 | 33 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴) ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) → (𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
35 | 34 | imp 444 |
. . . . . . . . 9
⊢ ((((𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴) ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 < 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
36 | 31, 32, 35 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 < 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
37 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Itv‘𝐺) =
(Itv‘𝐺) |
38 | 4 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → 𝐺 ∈ TarskiG) |
39 | 6 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝐴:𝐷⟶𝑃) |
40 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑖 ∈ dom 𝐴) |
41 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝐴:𝐷⟶𝑃 → dom 𝐴 = 𝐷) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → dom 𝐴 = 𝐷) |
43 | 40, 42 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑖 ∈ 𝐷) |
44 | 39, 43 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → (𝐴‘𝑖) ∈ 𝑃) |
45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → (𝐴‘𝑖) ∈ 𝑃) |
46 | 7 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝐵:𝐷⟶𝑃) |
47 | 46, 43 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → (𝐵‘𝑖) ∈ 𝑃) |
48 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → (𝐵‘𝑖) ∈ 𝑃) |
49 | 1, 2, 37, 38, 45, 48 | tgcgrtriv 25179 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑖)) = ((𝐵‘𝑖) − (𝐵‘𝑖))) |
50 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → (𝐴‘𝑖) = (𝐴‘𝑗)) |
52 | 51 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑖)) = ((𝐴‘𝑖) − (𝐴‘𝑗))) |
53 | 50 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → (𝐵‘𝑖) = (𝐵‘𝑗)) |
54 | 53 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → ((𝐵‘𝑖) − (𝐵‘𝑖)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
55 | 49, 52, 54 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
56 | 55 | adantl3r 782 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑖 = 𝑗) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
57 | 4 | ad4antr 764 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → 𝐺 ∈ TarskiG) |
58 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑗 ∈ dom 𝐴) |
59 | 58, 42 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑗 ∈ 𝐷) |
60 | 39, 59 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → (𝐴‘𝑗) ∈ 𝑃) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐴‘𝑗) ∈ 𝑃) |
62 | 61 | adantl3r 782 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐴‘𝑗) ∈ 𝑃) |
63 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐴‘𝑖) ∈ 𝑃) |
64 | 63 | adantl3r 782 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐴‘𝑖) ∈ 𝑃) |
65 | 46, 59 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → (𝐵‘𝑗) ∈ 𝑃) |
66 | 65 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐵‘𝑗) ∈ 𝑃) |
67 | 66 | adantl3r 782 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐵‘𝑗) ∈ 𝑃) |
68 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐵‘𝑖) ∈ 𝑃) |
69 | 68 | adantl3r 782 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → (𝐵‘𝑖) ∈ 𝑃) |
70 | | simplr 788 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → 𝑗 ∈ dom 𝐴) |
71 | | simpllr 795 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → 𝑖 ∈ dom 𝐴) |
72 | | simp-4r 803 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) |
73 | 70, 71, 72 | jca31 555 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → ((𝑗 ∈ dom 𝐴 ∧ 𝑖 ∈ dom 𝐴) ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))))) |
74 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → 𝑗 < 𝑖) |
75 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (𝑘 < 𝑙 ↔ 𝑗 < 𝑙)) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
77 | 76 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐴‘𝑗) − (𝐴‘𝑙))) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗)) |
79 | 78 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → ((𝐵‘𝑘) − (𝐵‘𝑙)) = ((𝐵‘𝑗) − (𝐵‘𝑙))) |
80 | 77, 79 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)) ↔ ((𝐴‘𝑗) − (𝐴‘𝑙)) = ((𝐵‘𝑗) − (𝐵‘𝑙)))) |
81 | 75, 80 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → ((𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))) ↔ (𝑗 < 𝑙 → ((𝐴‘𝑗) − (𝐴‘𝑙)) = ((𝐵‘𝑗) − (𝐵‘𝑙))))) |
82 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑖 → (𝑗 < 𝑙 ↔ 𝑗 < 𝑖)) |
83 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑖 → (𝐴‘𝑙) = (𝐴‘𝑖)) |
84 | 83 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑖 → ((𝐴‘𝑗) − (𝐴‘𝑙)) = ((𝐴‘𝑗) − (𝐴‘𝑖))) |
85 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑖 → (𝐵‘𝑙) = (𝐵‘𝑖)) |
86 | 85 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑖 → ((𝐵‘𝑗) − (𝐵‘𝑙)) = ((𝐵‘𝑗) − (𝐵‘𝑖))) |
87 | 84, 86 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑖 → (((𝐴‘𝑗) − (𝐴‘𝑙)) = ((𝐵‘𝑗) − (𝐵‘𝑙)) ↔ ((𝐴‘𝑗) − (𝐴‘𝑖)) = ((𝐵‘𝑗) − (𝐵‘𝑖)))) |
88 | 82, 87 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑖 → ((𝑗 < 𝑙 → ((𝐴‘𝑗) − (𝐴‘𝑙)) = ((𝐵‘𝑗) − (𝐵‘𝑙))) ↔ (𝑗 < 𝑖 → ((𝐴‘𝑗) − (𝐴‘𝑖)) = ((𝐵‘𝑗) − (𝐵‘𝑖))))) |
89 | 81, 88 | rspc2v 3293 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ dom 𝐴 ∧ 𝑖 ∈ dom 𝐴) → (∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))) → (𝑗 < 𝑖 → ((𝐴‘𝑗) − (𝐴‘𝑖)) = ((𝐵‘𝑗) − (𝐵‘𝑖))))) |
90 | 89 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ dom 𝐴 ∧ 𝑖 ∈ dom 𝐴) ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) → (𝑗 < 𝑖 → ((𝐴‘𝑗) − (𝐴‘𝑖)) = ((𝐵‘𝑗) − (𝐵‘𝑖)))) |
91 | 90 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝑗 ∈ dom 𝐴 ∧ 𝑖 ∈ dom 𝐴) ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑗 < 𝑖) → ((𝐴‘𝑗) − (𝐴‘𝑖)) = ((𝐵‘𝑗) − (𝐵‘𝑖))) |
92 | 73, 74, 91 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → ((𝐴‘𝑗) − (𝐴‘𝑖)) = ((𝐵‘𝑗) − (𝐵‘𝑖))) |
93 | 1, 2, 37, 57, 62, 64, 67, 69, 92 | tgcgrcomlr 25175 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) ∧ 𝑗 < 𝑖) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
94 | 6, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐴 = 𝐷) |
95 | 94, 5 | eqsstrd 3602 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐴 ⊆ ℝ) |
96 | 95 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → dom 𝐴 ⊆ ℝ) |
97 | 40 | adantllr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑖 ∈ dom 𝐴) |
98 | 96, 97 | sseldd 3569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑖 ∈ ℝ) |
99 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑗 ∈ dom 𝐴) |
100 | 96, 99 | sseldd 3569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → 𝑗 ∈ ℝ) |
101 | 98, 100 | lttri4d 10057 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → (𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖)) |
102 | 36, 56, 93, 101 | mpjao3dan 1387 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ 𝑖 ∈ dom 𝐴) ∧ 𝑗 ∈ dom 𝐴) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
103 | 102 | anasss 677 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) ∧ (𝑖 ∈ dom 𝐴 ∧ 𝑗 ∈ dom 𝐴)) → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
104 | 103 | ralrimivva 2954 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙)))) → ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
105 | 104 | ex 449 |
. . . 4
⊢ (𝜑 → (∀𝑘 ∈ dom 𝐴∀𝑙 ∈ dom 𝐴(𝑘 < 𝑙 → ((𝐴‘𝑘) − (𝐴‘𝑙)) = ((𝐵‘𝑘) − (𝐵‘𝑙))) → ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
106 | 27, 105 | syl5bir 232 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) → ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
107 | 12, 106 | impbid 201 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
108 | 8, 107 | bitrd 267 |
1
⊢ (𝜑 → (𝐴 ∼ 𝐵 ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |