Theorem ttgplusg

Description: The addition operation 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 )
	ttgplusg.1	|- .+ = ( +g ` H )
Assertion	ttgplusg	|- .+ = ( +g ` G )

Proof

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