# Metamath Proof Explorer

## Theorem ttgbtwnid

Description: Any subcomplex module equipped with the betweenness operation fulfills the identity of betweenness (Axiom A6). (Contributed by Thierry Arnoux, 26-Mar-2019)

Ref Expression
Hypotheses ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
ttgitvval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
ttgitvval.b ${⊢}{P}={\mathrm{Base}}_{{H}}$
ttgitvval.m
ttgitvval.s
ttgelitv.x ${⊢}{\phi }\to {X}\in {P}$
ttgelitv.y ${⊢}{\phi }\to {Y}\in {P}$
ttgbtwnid.r ${⊢}{R}={\mathrm{Base}}_{\mathrm{Scalar}\left({H}\right)}$
ttgbtwnid.2 ${⊢}{\phi }\to \left[0,1\right]\subseteq {R}$
ttgbtwnid.1 ${⊢}{\phi }\to {H}\in \mathrm{CMod}$
ttgbtwnid.y ${⊢}{\phi }\to {Y}\in \left({X}{I}{X}\right)$
Assertion ttgbtwnid ${⊢}{\phi }\to {X}={Y}$

### Proof

Step Hyp Ref Expression
1 ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
2 ttgitvval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
3 ttgitvval.b ${⊢}{P}={\mathrm{Base}}_{{H}}$
4 ttgitvval.m
5 ttgitvval.s
6 ttgelitv.x ${⊢}{\phi }\to {X}\in {P}$
7 ttgelitv.y ${⊢}{\phi }\to {Y}\in {P}$
8 ttgbtwnid.r ${⊢}{R}={\mathrm{Base}}_{\mathrm{Scalar}\left({H}\right)}$
9 ttgbtwnid.2 ${⊢}{\phi }\to \left[0,1\right]\subseteq {R}$
10 ttgbtwnid.1 ${⊢}{\phi }\to {H}\in \mathrm{CMod}$
11 ttgbtwnid.y ${⊢}{\phi }\to {Y}\in \left({X}{I}{X}\right)$
12 simpll
13 simpr
14 clmlmod ${⊢}{H}\in \mathrm{CMod}\to {H}\in \mathrm{LMod}$
15 10 14 syl ${⊢}{\phi }\to {H}\in \mathrm{LMod}$
16 eqid ${⊢}{0}_{{H}}={0}_{{H}}$
17 3 16 4 lmodsubid
18 15 6 17 syl2anc
20 19 oveq2d
23 simplr
24 22 23 sseldd
25 eqid ${⊢}\mathrm{Scalar}\left({H}\right)=\mathrm{Scalar}\left({H}\right)$
26 25 5 8 16 lmodvs0
27 21 24 26 syl2anc
28 13 20 27 3eqtrd
29 3 16 4 lmodsubeq0
30 15 7 6 29 syl3anc
31 30 biimpa
32 12 28 31 syl2anc
33 32 eqcomd
34 1 2 3 4 5 6 6 10 7 ttgelitv
35 11 34 mpbid
36 33 35 r19.29a ${⊢}{\phi }\to {X}={Y}$