Step | Hyp | Ref
| Expression |
1 | | mirval.s |
. . 3
⊢ 𝑆 = (pInvG‘𝐺) |
2 | | df-mir 25548 |
. . . . 5
⊢ pInvG =
(𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑦 ∈ (Base‘𝑔) ↦ (℩𝑧 ∈ (Base‘𝑔)((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦)))))) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → pInvG = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑦 ∈ (Base‘𝑔) ↦ (℩𝑧 ∈ (Base‘𝑔)((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦))))))) |
4 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
5 | | mirval.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
6 | 4, 5 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
7 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺)) |
8 | | mirval.d |
. . . . . . . . . . . 12
⊢ − =
(dist‘𝐺) |
9 | 7, 8 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = − ) |
10 | 9 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥(dist‘𝑔)𝑧) = (𝑥 − 𝑧)) |
11 | 9 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥(dist‘𝑔)𝑦) = (𝑥 − 𝑦)) |
12 | 10, 11 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ↔ (𝑥 − 𝑧) = (𝑥 − 𝑦))) |
13 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = (Itv‘𝐺)) |
14 | | mirval.i |
. . . . . . . . . . . 12
⊢ 𝐼 = (Itv‘𝐺) |
15 | 13, 14 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = 𝐼) |
16 | 15 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑧(Itv‘𝑔)𝑦) = (𝑧𝐼𝑦)) |
17 | 16 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (𝑧(Itv‘𝑔)𝑦) ↔ 𝑥 ∈ (𝑧𝐼𝑦))) |
18 | 12, 17 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦)) ↔ ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))) |
19 | 6, 18 | riotaeqbidv 6614 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (℩𝑧 ∈ (Base‘𝑔)((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦))) = (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))) |
20 | 6, 19 | mpteq12dv 4733 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑦 ∈ (Base‘𝑔) ↦ (℩𝑧 ∈ (Base‘𝑔)((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦)))) = (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦))))) |
21 | 6, 20 | mpteq12dv 4733 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (Base‘𝑔) ↦ (𝑦 ∈ (Base‘𝑔) ↦ (℩𝑧 ∈ (Base‘𝑔)((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦))))) = (𝑥 ∈ 𝑃 ↦ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))))) |
22 | 21 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑥 ∈ (Base‘𝑔) ↦ (𝑦 ∈ (Base‘𝑔) ↦ (℩𝑧 ∈ (Base‘𝑔)((𝑥(dist‘𝑔)𝑧) = (𝑥(dist‘𝑔)𝑦) ∧ 𝑥 ∈ (𝑧(Itv‘𝑔)𝑦))))) = (𝑥 ∈ 𝑃 ↦ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))))) |
23 | | mirval.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
24 | | elex 3212 |
. . . . 5
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ V) |
26 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
27 | 5, 26 | eqeltri 2697 |
. . . . . 6
⊢ 𝑃 ∈ V |
28 | 27 | mptex 6486 |
. . . . 5
⊢ (𝑥 ∈ 𝑃 ↦ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦))))) ∈ V |
29 | 28 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑃 ↦ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦))))) ∈ V) |
30 | 3, 22, 25, 29 | fvmptd 6288 |
. . 3
⊢ (𝜑 → (pInvG‘𝐺) = (𝑥 ∈ 𝑃 ↦ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))))) |
31 | 1, 30 | syl5eq 2668 |
. 2
⊢ (𝜑 → 𝑆 = (𝑥 ∈ 𝑃 ↦ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))))) |
32 | | simpll 790 |
. . . . . . . 8
⊢ (((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → 𝑥 = 𝐴) |
33 | 32 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (𝑥 − 𝑧) = (𝐴 − 𝑧)) |
34 | 32 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (𝑥 − 𝑦) = (𝐴 − 𝑦)) |
35 | 33, 34 | eqeq12d 2637 |
. . . . . 6
⊢ (((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → ((𝑥 − 𝑧) = (𝑥 − 𝑦) ↔ (𝐴 − 𝑧) = (𝐴 − 𝑦))) |
36 | 32 | eleq1d 2686 |
. . . . . 6
⊢ (((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝐴 ∈ (𝑧𝐼𝑦))) |
37 | 35, 36 | anbi12d 747 |
. . . . 5
⊢ (((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)) ↔ ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦)))) |
38 | 37 | riotabidva 6627 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃) → (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦))) = (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦)))) |
39 | 38 | mpteq2dva 4744 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))) = (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦))))) |
40 | 39 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝑥 − 𝑧) = (𝑥 − 𝑦) ∧ 𝑥 ∈ (𝑧𝐼𝑦)))) = (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦))))) |
41 | | mirval.a |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
42 | 27 | mptex 6486 |
. . 3
⊢ (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦)))) ∈ V |
43 | 42 | a1i 11 |
. 2
⊢ (𝜑 → (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦)))) ∈ V) |
44 | 31, 40, 41, 43 | fvmptd 6288 |
1
⊢ (𝜑 → (𝑆‘𝐴) = (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦))))) |