# Metamath Proof Explorer

## Theorem ismidb

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

Ref Expression
Hypotheses ismid.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
ismid.d
ismid.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
ismid.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
ismid.1 ${⊢}{\phi }\to {G}{\mathrm{Dim}}_{𝒢}\ge 2$
midcl.1 ${⊢}{\phi }\to {A}\in {P}$
midcl.2 ${⊢}{\phi }\to {B}\in {P}$
ismidb.s ${⊢}{S}={pInv}_{𝒢}\left({G}\right)$
ismidb.m ${⊢}{\phi }\to {M}\in {P}$
Assertion ismidb ${⊢}{\phi }\to \left({B}={S}\left({M}\right)\left({A}\right)↔{A}{mid}_{𝒢}\left({G}\right){B}={M}\right)$

### Proof

Step Hyp Ref Expression
1 ismid.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 ismid.d
3 ismid.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 ismid.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 ismid.1 ${⊢}{\phi }\to {G}{\mathrm{Dim}}_{𝒢}\ge 2$
6 midcl.1 ${⊢}{\phi }\to {A}\in {P}$
7 midcl.2 ${⊢}{\phi }\to {B}\in {P}$
8 ismidb.s ${⊢}{S}={pInv}_{𝒢}\left({G}\right)$
9 ismidb.m ${⊢}{\phi }\to {M}\in {P}$
10 eqid ${⊢}{Line}_{𝒢}\left({G}\right)={Line}_{𝒢}\left({G}\right)$
11 1 2 3 10 4 8 6 7 5 mideu ${⊢}{\phi }\to \exists !{m}\in {P}\phantom{\rule{.4em}{0ex}}{B}={S}\left({m}\right)\left({A}\right)$
12 fveq2 ${⊢}{m}={M}\to {S}\left({m}\right)={S}\left({M}\right)$
13 12 fveq1d ${⊢}{m}={M}\to {S}\left({m}\right)\left({A}\right)={S}\left({M}\right)\left({A}\right)$
14 13 eqeq2d ${⊢}{m}={M}\to \left({B}={S}\left({m}\right)\left({A}\right)↔{B}={S}\left({M}\right)\left({A}\right)\right)$
15 14 riota2 ${⊢}\left({M}\in {P}\wedge \exists !{m}\in {P}\phantom{\rule{.4em}{0ex}}{B}={S}\left({m}\right)\left({A}\right)\right)\to \left({B}={S}\left({M}\right)\left({A}\right)↔\left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)={M}\right)$
16 9 11 15 syl2anc ${⊢}{\phi }\to \left({B}={S}\left({M}\right)\left({A}\right)↔\left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)={M}\right)$
17 df-mid ${⊢}{mid}_{𝒢}=\left({g}\in \mathrm{V}⟼\left({a}\in {\mathrm{Base}}_{{g}},{b}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)\right)\right)$
18 fveq2 ${⊢}{g}={G}\to {\mathrm{Base}}_{{g}}={\mathrm{Base}}_{{G}}$
19 18 1 syl6eqr ${⊢}{g}={G}\to {\mathrm{Base}}_{{g}}={P}$
20 fveq2 ${⊢}{g}={G}\to {pInv}_{𝒢}\left({g}\right)={pInv}_{𝒢}\left({G}\right)$
21 20 8 syl6eqr ${⊢}{g}={G}\to {pInv}_{𝒢}\left({g}\right)={S}$
22 21 fveq1d ${⊢}{g}={G}\to {pInv}_{𝒢}\left({g}\right)\left({m}\right)={S}\left({m}\right)$
23 22 fveq1d ${⊢}{g}={G}\to {pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)={S}\left({m}\right)\left({a}\right)$
24 23 eqeq2d ${⊢}{g}={G}\to \left({b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)↔{b}={S}\left({m}\right)\left({a}\right)\right)$
25 19 24 riotaeqbidv ${⊢}{g}={G}\to \left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)=\left(\iota {m}\in {P}|{b}={S}\left({m}\right)\left({a}\right)\right)$
26 19 19 25 mpoeq123dv ${⊢}{g}={G}\to \left({a}\in {\mathrm{Base}}_{{g}},{b}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)\right)=\left({a}\in {P},{b}\in {P}⟼\left(\iota {m}\in {P}|{b}={S}\left({m}\right)\left({a}\right)\right)\right)$
27 4 elexd ${⊢}{\phi }\to {G}\in \mathrm{V}$
28 1 fvexi ${⊢}{P}\in \mathrm{V}$
29 28 28 mpoex ${⊢}\left({a}\in {P},{b}\in {P}⟼\left(\iota {m}\in {P}|{b}={S}\left({m}\right)\left({a}\right)\right)\right)\in \mathrm{V}$
30 29 a1i ${⊢}{\phi }\to \left({a}\in {P},{b}\in {P}⟼\left(\iota {m}\in {P}|{b}={S}\left({m}\right)\left({a}\right)\right)\right)\in \mathrm{V}$
31 17 26 27 30 fvmptd3 ${⊢}{\phi }\to {mid}_{𝒢}\left({G}\right)=\left({a}\in {P},{b}\in {P}⟼\left(\iota {m}\in {P}|{b}={S}\left({m}\right)\left({a}\right)\right)\right)$
32 simprr ${⊢}\left({\phi }\wedge \left({a}={A}\wedge {b}={B}\right)\right)\to {b}={B}$
33 simprl ${⊢}\left({\phi }\wedge \left({a}={A}\wedge {b}={B}\right)\right)\to {a}={A}$
34 33 fveq2d ${⊢}\left({\phi }\wedge \left({a}={A}\wedge {b}={B}\right)\right)\to {S}\left({m}\right)\left({a}\right)={S}\left({m}\right)\left({A}\right)$
35 32 34 eqeq12d ${⊢}\left({\phi }\wedge \left({a}={A}\wedge {b}={B}\right)\right)\to \left({b}={S}\left({m}\right)\left({a}\right)↔{B}={S}\left({m}\right)\left({A}\right)\right)$
36 35 riotabidv ${⊢}\left({\phi }\wedge \left({a}={A}\wedge {b}={B}\right)\right)\to \left(\iota {m}\in {P}|{b}={S}\left({m}\right)\left({a}\right)\right)=\left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)$
37 riotacl ${⊢}\exists !{m}\in {P}\phantom{\rule{.4em}{0ex}}{B}={S}\left({m}\right)\left({A}\right)\to \left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)\in {P}$
38 11 37 syl ${⊢}{\phi }\to \left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)\in {P}$
39 31 36 6 7 38 ovmpod ${⊢}{\phi }\to {A}{mid}_{𝒢}\left({G}\right){B}=\left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)$
40 39 eqeq1d ${⊢}{\phi }\to \left({A}{mid}_{𝒢}\left({G}\right){B}={M}↔\left(\iota {m}\in {P}|{B}={S}\left({m}\right)\left({A}\right)\right)={M}\right)$
41 16 40 bitr4d ${⊢}{\phi }\to \left({B}={S}\left({M}\right)\left({A}\right)↔{A}{mid}_{𝒢}\left({G}\right){B}={M}\right)$