Theorem ttgvscaOLD

Description: Obsolete proof of ttgvsca as of 29-Oct-2024. The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgvsca.1	⊢ · = ( ·𝑠 ‘ 𝐻 )
3		df-vsca	⊢ ·𝑠 = Slot 6
4		6nn	⊢ 6 ∈ ℕ
5		1nn	⊢ 1 ∈ ℕ
6		6nn0	⊢ 6 ∈ ℕ0
7		6lt10	⊢ 6 < ; 1 0
8	5 6 6 7	declti	⊢ 6 < ; 1 6
9	1 3 4 8	ttglemOLD	⊢ ( ·𝑠 ‘ 𝐻 ) = ( ·𝑠 ‘ 𝐺 )
10	2 9	eqtri	⊢ · = ( ·𝑠 ‘ 𝐺 )