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	|- G = ( toTG ` H )
	ttgvsca.1	|- .x. = ( .s ` H )
Assertion	ttgvsca	|- .x. = ( .s ` G )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	|- G = ( toTG ` H )
2		ttgvsca.1	|- .x. = ( .s ` H )
3		vscaid	|- .s = Slot ( .s ` ndx )
4		slotslnbpsd	|- ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) )
5		simprl	|- ( ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) ) -> ( LineG ` ndx ) =/= ( .s ` ndx ) )
6	4 5	ax-mp	|- ( LineG ` ndx ) =/= ( .s ` ndx )
7	6	necomi	|- ( .s ` ndx ) =/= ( LineG ` ndx )
8		slotsinbpsd	|- ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) )
9		simprl	|- ( ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) ) -> ( Itv ` ndx ) =/= ( .s ` ndx ) )
10	8 9	ax-mp	|- ( Itv ` ndx ) =/= ( .s ` ndx )
11	10	necomi	|- ( .s ` ndx ) =/= ( Itv ` ndx )
12	1 3 7 11	ttglem	|- ( .s ` H ) = ( .s ` G )
13	2 12	eqtri	|- .x. = ( .s ` G )