MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mid Structured version   Visualization version   GIF version

Definition df-mid 25384
Description: Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 25388, midbtwn 25389, and midcgr 25390. (Contributed by Thierry Arnoux, 9-Jun-2019.)
Assertion
Ref Expression
df-mid midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))
Distinct variable group:   𝑎,𝑏,𝑔,𝑚

Detailed syntax breakdown of Definition df-mid
StepHypRef Expression
1 cmid 25382 . 2 class midG
2 vg . . 3 setvar 𝑔
3 cvv 3172 . . 3 class V
4 va . . . 4 setvar 𝑎
5 vb . . . 4 setvar 𝑏
62cv 1473 . . . . 5 class 𝑔
7 cbs 15641 . . . . 5 class Base
86, 7cfv 5790 . . . 4 class (Base‘𝑔)
95cv 1473 . . . . . 6 class 𝑏
104cv 1473 . . . . . . 7 class 𝑎
11 vm . . . . . . . . 9 setvar 𝑚
1211cv 1473 . . . . . . . 8 class 𝑚
13 cmir 25265 . . . . . . . . 9 class pInvG
146, 13cfv 5790 . . . . . . . 8 class (pInvG‘𝑔)
1512, 14cfv 5790 . . . . . . 7 class ((pInvG‘𝑔)‘𝑚)
1610, 15cfv 5790 . . . . . 6 class (((pInvG‘𝑔)‘𝑚)‘𝑎)
179, 16wceq 1474 . . . . 5 wff 𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)
1817, 11, 8crio 6488 . . . 4 class (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))
194, 5, 8, 8, 18cmpt2 6529 . . 3 class (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)))
202, 3, 19cmpt 4637 . 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))
211, 20wceq 1474 1 wff midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))
Colors of variables: wff setvar class
This definition is referenced by:  midf  25386  ismidb  25388
  Copyright terms: Public domain W3C validator