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

Definition df-mid 25711
 Description: Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 25715, midbtwn 25716, and midcgr 25717. (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 25709 . 2 class midG
2 vg . . 3 setvar 𝑔
3 cvv 3231 . . 3 class V
4 va . . . 4 setvar 𝑎
5 vb . . . 4 setvar 𝑏
62cv 1522 . . . . 5 class 𝑔
7 cbs 15904 . . . . 5 class Base
86, 7cfv 5926 . . . 4 class (Base‘𝑔)
95cv 1522 . . . . . 6 class 𝑏
104cv 1522 . . . . . . 7 class 𝑎
11 vm . . . . . . . . 9 setvar 𝑚
1211cv 1522 . . . . . . . 8 class 𝑚
13 cmir 25592 . . . . . . . . 9 class pInvG
146, 13cfv 5926 . . . . . . . 8 class (pInvG‘𝑔)
1512, 14cfv 5926 . . . . . . 7 class ((pInvG‘𝑔)‘𝑚)
1610, 15cfv 5926 . . . . . 6 class (((pInvG‘𝑔)‘𝑚)‘𝑎)
179, 16wceq 1523 . . . . 5 wff 𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)
1817, 11, 8crio 6650 . . . 4 class (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))
194, 5, 8, 8, 18cmpt2 6692 . . 3 class (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)))
202, 3, 19cmpt 4762 . 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))
211, 20wceq 1523 1 wff midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))
 Colors of variables: wff setvar class This definition is referenced by:  midf  25713  ismidb  25715
 Copyright terms: Public domain W3C validator