Theorem ttgvsca

Description: The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019) (Revised by AV, 29-Oct-2024)

	Ref	Expression
Hypotheses	ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgvsca.1	⊢ · = ( ·𝑠 ‘ 𝐻 )
Assertion	ttgvsca	⊢ · = ( ·𝑠 ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgvsca.1	⊢ · = ( ·𝑠 ‘ 𝐻 )
3		vscaid	⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
4		slotslnbpsd	⊢ ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
5		simprl	⊢ ( ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( dist ‘ ndx ) ) ) → ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) )
6	4 5	ax-mp	⊢ ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
7	6	necomi	⊢ ( ·𝑠 ‘ ndx ) ≠ ( LineG ‘ ndx )
8		slotsinbpsd	⊢ ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
9		simprl	⊢ ( ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) ) → ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) )
10	8 9	ax-mp	⊢ ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
11	10	necomi	⊢ ( ·𝑠 ‘ ndx ) ≠ ( Itv ‘ ndx )
12	1 3 7 11	ttglem	⊢ ( ·𝑠 ‘ 𝐻 ) = ( ·𝑠 ‘ 𝐺 )
13	2 12	eqtri	⊢ · = ( ·𝑠 ‘ 𝐺 )