Step | Hyp | Ref
| Expression |
1 | | ismid.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
2 | | ismid.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
3 | | ismid.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
4 | | eqid 2610 |
. . . . . 6
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
5 | | ismid.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐺 ∈ TarskiG) |
7 | | eqid 2610 |
. . . . . 6
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
8 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝑎 ∈ 𝑃) |
9 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝑏 ∈ 𝑃) |
10 | | ismid.1 |
. . . . . . 7
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐺DimTarskiG≥2) |
12 | 1, 2, 3, 4, 6, 7, 8, 9, 11 | mideu 25430 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ∃!𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) |
13 | 12 | ralrimivva 2954 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃!𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) |
14 | | riotacl 6525 |
. . . . . 6
⊢
(∃!𝑚 ∈
𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎) → (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) ∈ 𝑃) |
15 | 14 | ralimi 2936 |
. . . . 5
⊢
(∀𝑏 ∈
𝑃 ∃!𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎) → ∀𝑏 ∈ 𝑃 (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) ∈ 𝑃) |
16 | 15 | ralimi 2936 |
. . . 4
⊢
(∀𝑎 ∈
𝑃 ∀𝑏 ∈ 𝑃 ∃!𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎) → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) ∈ 𝑃) |
17 | 13, 16 | syl 17 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) ∈ 𝑃) |
18 | | eqid 2610 |
. . . 4
⊢ (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))) = (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))) |
19 | 18 | fmpt2 7126 |
. . 3
⊢
(∀𝑎 ∈
𝑃 ∀𝑏 ∈ 𝑃 (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)) ∈ 𝑃 ↔ (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))):(𝑃 × 𝑃)⟶𝑃) |
20 | 17, 19 | sylib 207 |
. 2
⊢ (𝜑 → (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))):(𝑃 × 𝑃)⟶𝑃) |
21 | | df-mid 25466 |
. . . . 5
⊢ midG =
(𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)))) |
22 | 21 | a1i 11 |
. . . 4
⊢ (𝜑 → midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))) |
23 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
24 | 23, 1 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
25 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (pInvG‘𝑔) = (pInvG‘𝐺)) |
26 | 25 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((pInvG‘𝑔)‘𝑚) = ((pInvG‘𝐺)‘𝑚)) |
27 | 26 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (((pInvG‘𝑔)‘𝑚)‘𝑎) = (((pInvG‘𝐺)‘𝑚)‘𝑎)) |
28 | 27 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎) ↔ 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))) |
29 | 24, 28 | riotaeqbidv 6514 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)) = (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))) |
30 | 24, 24, 29 | mpt2eq123dv 6615 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))) = (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)))) |
31 | 30 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))) = (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)))) |
32 | | elex 3185 |
. . . . 5
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
33 | 5, 32 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ V) |
34 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
35 | 1, 34 | eqeltri 2684 |
. . . . . 6
⊢ 𝑃 ∈ V |
36 | 35, 35 | mpt2ex 7136 |
. . . . 5
⊢ (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))) ∈ V |
37 | 36 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))) ∈ V) |
38 | 22, 31, 33, 37 | fvmptd 6197 |
. . 3
⊢ (𝜑 → (midG‘𝐺) = (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎)))) |
39 | 38 | feq1d 5943 |
. 2
⊢ (𝜑 → ((midG‘𝐺):(𝑃 × 𝑃)⟶𝑃 ↔ (𝑎 ∈ 𝑃, 𝑏 ∈ 𝑃 ↦ (℩𝑚 ∈ 𝑃 𝑏 = (((pInvG‘𝐺)‘𝑚)‘𝑎))):(𝑃 × 𝑃)⟶𝑃)) |
40 | 20, 39 | mpbird 246 |
1
⊢ (𝜑 → (midG‘𝐺):(𝑃 × 𝑃)⟶𝑃) |