Step | Hyp | Ref
| Expression |
1 | | istrkg.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | istrkg.d |
. . 3
⊢ − =
(dist‘𝐺) |
3 | | simpl 486 |
. . . . . 6
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ) → 𝑝 = 𝑃) |
4 | 3 | eqcomd 2743 |
. . . . 5
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ) → 𝑃 = 𝑝) |
5 | 4 | adantr 484 |
. . . . . 6
⊢ (((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) → 𝑃 = 𝑝) |
6 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → 𝑑 = − ) |
7 | 6 | eqcomd 2743 |
. . . . . . . 8
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → − = 𝑑) |
8 | 7 | oveqd 7230 |
. . . . . . 7
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → (𝑥 − 𝑦) = (𝑥𝑑𝑦)) |
9 | 7 | oveqd 7230 |
. . . . . . 7
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → (𝑦 − 𝑥) = (𝑦𝑑𝑥)) |
10 | 8, 9 | eqeq12d 2753 |
. . . . . 6
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → ((𝑥 − 𝑦) = (𝑦 − 𝑥) ↔ (𝑥𝑑𝑦) = (𝑦𝑑𝑥))) |
11 | 5, 10 | raleqbidva 3331 |
. . . . 5
⊢ (((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) → (∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ↔ ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥))) |
12 | 4, 11 | raleqbidva 3331 |
. . . 4
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ) →
(∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ↔ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥))) |
13 | 5 | adantr 484 |
. . . . . . 7
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → 𝑃 = 𝑝) |
14 | 7 | oveqdr 7241 |
. . . . . . . . 9
⊢
(((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (𝑥 − 𝑦) = (𝑥𝑑𝑦)) |
15 | 7 | oveqdr 7241 |
. . . . . . . . 9
⊢
(((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (𝑧 − 𝑧) = (𝑧𝑑𝑧)) |
16 | 14, 15 | eqeq12d 2753 |
. . . . . . . 8
⊢
(((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → ((𝑥 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑥𝑑𝑦) = (𝑧𝑑𝑧))) |
17 | 16 | imbi1d 345 |
. . . . . . 7
⊢
(((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))) |
18 | 13, 17 | raleqbidva 3331 |
. . . . . 6
⊢ ((((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → (∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))) |
19 | 5, 18 | raleqbidva 3331 |
. . . . 5
⊢ (((𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃) → (∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))) |
20 | 4, 19 | raleqbidva 3331 |
. . . 4
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ) →
(∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))) |
21 | 12, 20 | anbi12d 634 |
. . 3
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ) →
((∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)) ↔ (∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)))) |
22 | 1, 2, 21 | sbcie2s 16714 |
. 2
⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)) ↔ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)))) |
23 | | df-trkgc 26539 |
. 2
⊢
TarskiGC = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))} |
24 | 22, 23 | elab4g 3592 |
1
⊢ (𝐺 ∈ TarskiGC
↔ (𝐺 ∈ V ∧
(∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)))) |