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 = ( toTG ` H )
ttgitvval.i 
|- I = ( Itv ` G )
ttgitvval.b 
|- P = ( Base ` H )
ttgitvval.m 
|- .- = ( -g ` H )
ttgitvval.s 
|- .x. = ( .s ` H )
ttgelitv.x 
|- ( ph -> X e. P )
ttgelitv.y 
|- ( ph -> Y e. P )
ttgbtwnid.r 
|- R = ( Base ` ( Scalar ` H ) )
ttgbtwnid.2 
|- ( ph -> ( 0 [,] 1 ) C_ R )
ttgbtwnid.1 
|- ( ph -> H e. CMod )
ttgbtwnid.y 
|- ( ph -> Y e. ( X I X ) )
Assertion ttgbtwnid 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 ttgval.n 
 |-  G = ( toTG ` H )
2 ttgitvval.i 
 |-  I = ( Itv ` G )
3 ttgitvval.b 
 |-  P = ( Base ` H )
4 ttgitvval.m 
 |-  .- = ( -g ` H )
5 ttgitvval.s 
 |-  .x. = ( .s ` H )
6 ttgelitv.x 
 |-  ( ph -> X e. P )
7 ttgelitv.y 
 |-  ( ph -> Y e. P )
8 ttgbtwnid.r 
 |-  R = ( Base ` ( Scalar ` H ) )
9 ttgbtwnid.2 
 |-  ( ph -> ( 0 [,] 1 ) C_ R )
10 ttgbtwnid.1 
 |-  ( ph -> H e. CMod )
11 ttgbtwnid.y 
 |-  ( ph -> Y e. ( X I X ) )
12 simpll 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ph )
13 simpr 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ( Y .- X ) = ( k .x. ( X .- X ) ) )
14 clmlmod 
 |-  ( H e. CMod -> H e. LMod )
15 10 14 syl 
 |-  ( ph -> H e. LMod )
16 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
17 3 16 4 lmodsubid 
 |-  ( ( H e. LMod /\ X e. P ) -> ( X .- X ) = ( 0g ` H ) )
18 15 6 17 syl2anc 
 |-  ( ph -> ( X .- X ) = ( 0g ` H ) )
19 18 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ( X .- X ) = ( 0g ` H ) )
20 19 oveq2d 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ( k .x. ( X .- X ) ) = ( k .x. ( 0g ` H ) ) )
21 15 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> H e. LMod )
22 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ( 0 [,] 1 ) C_ R )
23 simplr 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> k e. ( 0 [,] 1 ) )
24 22 23 sseldd 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> k e. R )
25 eqid 
 |-  ( Scalar ` H ) = ( Scalar ` H )
26 25 5 8 16 lmodvs0 
 |-  ( ( H e. LMod /\ k e. R ) -> ( k .x. ( 0g ` H ) ) = ( 0g ` H ) )
27 21 24 26 syl2anc 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ( k .x. ( 0g ` H ) ) = ( 0g ` H ) )
28 13 20 27 3eqtrd 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> ( Y .- X ) = ( 0g ` H ) )
29 3 16 4 lmodsubeq0 
 |-  ( ( H e. LMod /\ Y e. P /\ X e. P ) -> ( ( Y .- X ) = ( 0g ` H ) <-> Y = X ) )
30 15 7 6 29 syl3anc 
 |-  ( ph -> ( ( Y .- X ) = ( 0g ` H ) <-> Y = X ) )
31 30 biimpa 
 |-  ( ( ph /\ ( Y .- X ) = ( 0g ` H ) ) -> Y = X )
32 12 28 31 syl2anc 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> Y = X )
33 32 eqcomd 
 |-  ( ( ( ph /\ k e. ( 0 [,] 1 ) ) /\ ( Y .- X ) = ( k .x. ( X .- X ) ) ) -> X = Y )
34 1 2 3 4 5 6 6 10 7 ttgelitv 
 |-  ( ph -> ( Y e. ( X I X ) <-> E. k e. ( 0 [,] 1 ) ( Y .- X ) = ( k .x. ( X .- X ) ) ) )
35 11 34 mpbid 
 |-  ( ph -> E. k e. ( 0 [,] 1 ) ( Y .- X ) = ( k .x. ( X .- X ) ) )
36 33 35 r19.29a 
 |-  ( ph -> X = Y )