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	$$⊢\underset{\dot{}}{-}={-}_H$$
	ttgitvval.s	$$⊢\underset{\dot{}}{·}={\cdot }_H$$
	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(XIX\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	$$⊢\underset{\dot{}}{-}={-}_H$$
5		ttgitvval.s	$$⊢\underset{\dot{}}{·}={\cdot }_H$$
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(XIX\right)$$
12		simpll	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to \phi$$
13		simpr	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)$$
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	$$⊢\left(H\in \mathrm{LMod}\wedge X\in P\right)\to X\underset{\dot{}}{-}X=0_H$$
18	15 6 17	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}X=0_H$$
19	18	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to X\underset{\dot{}}{-}X=0_H$$
20	19	oveq2d	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)=k\underset{\dot{}}{·}{0}_H$$
21	15	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to H\in \mathrm{LMod}$$
22	9	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to \left[0,1\right]\subseteq R$$
23		simplr	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to k\in \left[0,1\right]$$
24	22 23	sseldd	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to k\in R$$
25		eqid	$$⊢\mathrm{Scalar}\left(H\right)=\mathrm{Scalar}\left(H\right)$$
26	25 5 8 16	lmodvs0	$$⊢\left(H\in \mathrm{LMod}\wedge k\in R\right)\to k\underset{\dot{}}{·}{0}_H=0_H$$
27	21 24 26	syl2anc	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to k\underset{\dot{}}{·}{0}_H=0_H$$
28	13 20 27	3eqtrd	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to Y\underset{\dot{}}{-}X=0_H$$
29	3 16 4	lmodsubeq0	$$⊢\left(H\in \mathrm{LMod}\wedge Y\in P\wedge X\in P\right)\to \left(Y\underset{\dot{}}{-}X=0_H\leftrightarrow Y=X\right)$$
30	15 7 6 29	syl3anc	$$⊢\phi \to \left(Y\underset{\dot{}}{-}X=0_H\leftrightarrow Y=X\right)$$
31	30	biimpa	$$⊢\left(\phi \wedge Y\underset{\dot{}}{-}X=0_H\right)\to Y=X$$
32	12 28 31	syl2anc	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to Y=X$$
33	32	eqcomd	$$⊢\left(\left(\phi \wedge k\in \left[0,1\right]\right)\wedge Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)\to X=Y$$
34	1 2 3 4 5 6 6 10 7	ttgelitv	$$⊢\phi \to \left(Y\in \left(XIX\right)\leftrightarrow \exists k\in \left[0,1\right]Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)\right)$$
35	11 34	mpbid	$$⊢\phi \to \exists k\in \left[0,1\right]Y\underset{\dot{}}{-}X=k\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}X\right)$$
36	33 35	r19.29a	$$⊢\phi \to X=Y$$