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	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgplusg.1	⊢ + = ( +g ‘ 𝐻 )
Assertion	ttgplusg	⊢ + = ( +g ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgplusg.1	⊢ + = ( +g ‘ 𝐻 )
3		plusgid	⊢ +g = Slot ( +g ‘ ndx )
4		slotslnbpsd	⊢ ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
5		simplr	⊢ ( ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ 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 ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
9		simplr	⊢ ( ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ 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 ‘ 𝐻 ) = ( +g ‘ 𝐺 )
13	2 12	eqtri	⊢ + = ( +g ‘ 𝐺 )