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={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
	ttgvsca.1	$$⊢\underset{\dot{}}{·}={\cdot }_H$$
Assertion	ttgvsca	$$⊢\underset{\dot{}}{·}={\cdot }_G$$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgvsca.1	$$⊢\underset{\dot{}}{·}={\cdot }_H$$
3		vscaid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
4		slotslnbpsd	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$
5		simprl	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
6	4 5	ax-mp	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
7	6	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)$$
8		slotsinbpsd	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$
9		simprl	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
10	8 9	ax-mp	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
11	10	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$$
12	1 3 7 11	ttglem	$$⊢{\cdot }_H={\cdot }_G$$
13	2 12	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_G$$