Theorem eengstr

Description: The Euclidean geometry as a structure. (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Assertion	eengstr	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		eengv	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
2		1nn	⊢ 1 ∈ ℕ
3		basendx	⊢ ( Base ‘ ndx ) = 1
4		2nn0	⊢ 2 ∈ ℕ0
5		1nn0	⊢ 1 ∈ ℕ0
6		1lt10	⊢ 1 < ; 1 0
7	2 4 5 6	declti	⊢ 1 < ; 1 2
8		2nn	⊢ 2 ∈ ℕ
9	5 8	decnncl	⊢ ; 1 2 ∈ ℕ
10		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
11	2 3 7 9 10	strle2	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } Struct ⟨ 1 , ; 1 2 ⟩
12		6nn	⊢ 6 ∈ ℕ
13	5 12	decnncl	⊢ ; 1 6 ∈ ℕ
14		itvndx	⊢ ( Itv ‘ ndx ) = ; 1 6
15		6nn0	⊢ 6 ∈ ℕ0
16		7nn	⊢ 7 ∈ ℕ
17		6lt7	⊢ 6 < 7
18	5 15 16 17	declt	⊢ ; 1 6 < ; 1 7
19	5 16	decnncl	⊢ ; 1 7 ∈ ℕ
20		lngndx	⊢ ( LineG ‘ ndx ) = ; 1 7
21	13 14 18 19 20	strle2	⊢ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } Struct ⟨ ; 1 6 , ; 1 7 ⟩
22		2lt6	⊢ 2 < 6
23	5 4 12 22	declt	⊢ ; 1 2 < ; 1 6
24	11 21 23	strleun	⊢ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) Struct ⟨ 1 , ; 1 7 ⟩
25	1 24	eqbrtrdi	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ )