Theorem trkgstr

Description: Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017)

	Ref	Expression
Hypothesis	trkgstr.w	|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
Assertion	trkgstr	|- W Struct <. 1 , ; 1 6 >.

Proof

Step	Hyp	Ref	Expression
1		trkgstr.w	|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
2		1nn	|- 1 e. NN
3		basendx	|- ( Base ` ndx ) = 1
4		2nn0	|- 2 e. NN0
5		1nn0	|- 1 e. NN0
6		1lt10	|- 1 < ; 1 0
7	2 4 5 6	declti	|- 1 < ; 1 2
8		2nn	|- 2 e. NN
9	5 8	decnncl	|- ; 1 2 e. NN
10		dsndx	|- ( dist ` ndx ) = ; 1 2
11		6nn	|- 6 e. NN
12		2lt6	|- 2 < 6
13	5 4 11 12	declt	|- ; 1 2 < ; 1 6
14	5 11	decnncl	|- ; 1 6 e. NN
15		itvndx	|- ( Itv ` ndx ) = ; 1 6
16	2 3 7 9 10 13 14 15	strle3	|- { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. } Struct <. 1 , ; 1 6 >.
17	1 16	eqbrtri	|- W Struct <. 1 , ; 1 6 >.