Metamath Proof Explorer


Theorem ismidb

Description: Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses ismid.p P = Base G
ismid.d - ˙ = dist G
ismid.i I = Itv G
ismid.g φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
midcl.1 φ A P
midcl.2 φ B P
ismidb.s S = pInv 𝒢 G
ismidb.m φ M P
Assertion ismidb φ B = S M A A mid 𝒢 G B = M

Proof

Step Hyp Ref Expression
1 ismid.p P = Base G
2 ismid.d - ˙ = dist G
3 ismid.i I = Itv G
4 ismid.g φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 midcl.1 φ A P
7 midcl.2 φ B P
8 ismidb.s S = pInv 𝒢 G
9 ismidb.m φ M P
10 eqid Line 𝒢 G = Line 𝒢 G
11 1 2 3 10 4 8 6 7 5 mideu φ ∃! m P B = S m A
12 fveq2 m = M S m = S M
13 12 fveq1d m = M S m A = S M A
14 13 eqeq2d m = M B = S m A B = S M A
15 14 riota2 M P ∃! m P B = S m A B = S M A ι m P | B = S m A = M
16 9 11 15 syl2anc φ B = S M A ι m P | B = S m A = M
17 df-mid mid 𝒢 = g V a Base g , b Base g ι m Base g | b = pInv 𝒢 g m a
18 fveq2 g = G Base g = Base G
19 18 1 eqtr4di g = G Base g = P
20 fveq2 g = G pInv 𝒢 g = pInv 𝒢 G
21 20 8 eqtr4di g = G pInv 𝒢 g = S
22 21 fveq1d g = G pInv 𝒢 g m = S m
23 22 fveq1d g = G pInv 𝒢 g m a = S m a
24 23 eqeq2d g = G b = pInv 𝒢 g m a b = S m a
25 19 24 riotaeqbidv g = G ι m Base g | b = pInv 𝒢 g m a = ι m P | b = S m a
26 19 19 25 mpoeq123dv g = G a Base g , b Base g ι m Base g | b = pInv 𝒢 g m a = a P , b P ι m P | b = S m a
27 4 elexd φ G V
28 1 fvexi P V
29 28 28 mpoex a P , b P ι m P | b = S m a V
30 29 a1i φ a P , b P ι m P | b = S m a V
31 17 26 27 30 fvmptd3 φ mid 𝒢 G = a P , b P ι m P | b = S m a
32 simprr φ a = A b = B b = B
33 simprl φ a = A b = B a = A
34 33 fveq2d φ a = A b = B S m a = S m A
35 32 34 eqeq12d φ a = A b = B b = S m a B = S m A
36 35 riotabidv φ a = A b = B ι m P | b = S m a = ι m P | B = S m A
37 riotacl ∃! m P B = S m A ι m P | B = S m A P
38 11 37 syl φ ι m P | B = S m A P
39 31 36 6 7 38 ovmpod φ A mid 𝒢 G B = ι m P | B = S m A
40 39 eqeq1d φ A mid 𝒢 G B = M ι m P | B = S m A = M
41 16 40 bitr4d φ B = S M A A mid 𝒢 G B = M