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 ⊢ 𝐺 = ( toTG ‘ 𝐻 )
ttgitvval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ttgitvval.b ⊢ 𝑃 = ( Base ‘ 𝐻 )
ttgitvval.m ⊢ − = ( -g ‘ 𝐻 )
ttgitvval.s ⊢ · = ( ·𝑠 ‘ 𝐻 )
ttgelitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
ttgelitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
ttgbtwnid.r ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝐻 ) )
ttgbtwnid.2 ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ 𝑅 )
ttgbtwnid.1 ⊢ ( 𝜑 → 𝐻 ∈ ℂMod )
ttgbtwnid.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) )
Assertion ttgbtwnid ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 ttgval.n ⊢ 𝐺 = ( toTG ‘ 𝐻 )
2 ttgitvval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ttgitvval.b ⊢ 𝑃 = ( Base ‘ 𝐻 )
4 ttgitvval.m ⊢ − = ( -g ‘ 𝐻 )
5 ttgitvval.s ⊢ · = ( ·𝑠 ‘ 𝐻 )
6 ttgelitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7 ttgelitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8 ttgbtwnid.r ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝐻 ) )
9 ttgbtwnid.2 ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ 𝑅 )
10 ttgbtwnid.1 ⊢ ( 𝜑 → 𝐻 ∈ ℂMod )
11 ttgbtwnid.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) )
12 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → 𝜑 )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) )
14 clmlmod ⊢ ( 𝐻 ∈ ℂMod → 𝐻 ∈ LMod )
15 10 14 syl ⊢ ( 𝜑 → 𝐻 ∈ LMod )
16 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
17 3 16 4 lmodsubid ⊢ ( ( 𝐻 ∈ LMod ∧ 𝑋 ∈ 𝑃 ) → ( 𝑋 − 𝑋 ) = ( 0g ‘ 𝐻 ) )
18 15 6 17 syl2anc ⊢ ( 𝜑 → ( 𝑋 − 𝑋 ) = ( 0g ‘ 𝐻 ) )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → ( 𝑋 − 𝑋 ) = ( 0g ‘ 𝐻 ) )
20 19 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → ( 𝑘 · ( 𝑋 − 𝑋 ) ) = ( 𝑘 · ( 0g ‘ 𝐻 ) ) )
21 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → 𝐻 ∈ LMod )
22 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → ( 0 [,] 1 ) ⊆ 𝑅 )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → 𝑘 ∈ ( 0 [,] 1 ) )
24 22 23 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → 𝑘 ∈ 𝑅 )
25 eqid ⊢ ( Scalar ‘ 𝐻 ) = ( Scalar ‘ 𝐻 )
26 25 5 8 16 lmodvs0 ⊢ ( ( 𝐻 ∈ LMod ∧ 𝑘 ∈ 𝑅 ) → ( 𝑘 · ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
27 21 24 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → ( 𝑘 · ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
28 13 20 27 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → ( 𝑌 − 𝑋 ) = ( 0g ‘ 𝐻 ) )
29 3 16 4 lmodsubeq0 ⊢ ( ( 𝐻 ∈ LMod ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑌 − 𝑋 ) = ( 0g ‘ 𝐻 ) ↔ 𝑌 = 𝑋 ) )
30 15 7 6 29 syl3anc ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) = ( 0g ‘ 𝐻 ) ↔ 𝑌 = 𝑋 ) )
31 30 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑌 − 𝑋 ) = ( 0g ‘ 𝐻 ) ) → 𝑌 = 𝑋 )
32 12 28 31 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → 𝑌 = 𝑋 )
33 32 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) → 𝑋 = 𝑌 )
34 1 2 3 4 5 6 6 10 7 ttgelitv ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) ) )
35 11 34 mpbid ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑌 − 𝑋 ) = ( 𝑘 · ( 𝑋 − 𝑋 ) ) )
36 33 35 r19.29a ⊢ ( 𝜑 → 𝑋 = 𝑌 )