ecgrtg

Description: The congruence relation used in the Tarski structure for the Euclidean geometry is the same as Cgr . (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Hypotheses	ecgrtg.1	$⊢ φ \to N \in ℕ$
	ecgrtg.2	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
	ecgrtg.3	$⊢ \underset{˙}{-} = dist (𝔼_{𝒢} (N))$
	ecgrtg.a	$⊢ φ \to A \in P$
	ecgrtg.b	$⊢ φ \to B \in P$
	ecgrtg.c	$⊢ φ \to C \in P$
	ecgrtg.d	$⊢ φ \to D \in P$
Assertion	ecgrtg	$⊢ φ \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow A \underset{˙}{-} B = C \underset{˙}{-} D)$

Proof

Step	Hyp	Ref	Expression
1		ecgrtg.1	$⊢ φ \to N \in ℕ$
2		ecgrtg.2	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
3		ecgrtg.3	$⊢ \underset{˙}{-} = dist (𝔼_{𝒢} (N))$
4		ecgrtg.a	$⊢ φ \to A \in P$
5		ecgrtg.b	$⊢ φ \to B \in P$
6		ecgrtg.c	$⊢ φ \to C \in P$
7		ecgrtg.d	$⊢ φ \to D \in P$
8		eengbas	$⊢ N \in ℕ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
9	1 8	syl	$⊢ φ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
10	9 2	eqtr4di	$⊢ φ \to 𝔼 (N) = P$
11	4 10	eleqtrrd	$⊢ φ \to A \in 𝔼 (N)$
12	5 10	eleqtrrd	$⊢ φ \to B \in 𝔼 (N)$
13	6 10	eleqtrrd	$⊢ φ \to C \in 𝔼 (N)$
14	7 10	eleqtrrd	$⊢ φ \to D \in 𝔼 (N)$
15		brcgr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
16	11 12 13 14 15	syl22anc	$⊢ φ \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
17		dsid	$⊢ dist = Slot dist (ndx)$
18		fvexd	$⊢ φ \to 𝔼_{𝒢} (N) \in V$
19		eengstr	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) Struct ⟨1, 17⟩$
20	1 19	syl	$⊢ φ \to 𝔼_{𝒢} (N) Struct ⟨1, 17⟩$
21		structn0fun	$⊢ 𝔼_{𝒢} (N) Struct ⟨1, 17⟩ \to Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\})$
22	20 21	syl	$⊢ φ \to Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\})$
23		structcnvcnv	$⊢ 𝔼_{𝒢} (N) Struct ⟨1, 17⟩ \to {𝔼_{𝒢} (N)}^{-1}^{-1} = 𝔼_{𝒢} (N) ∖ \{\emptyset\}$
24	20 23	syl	$⊢ φ \to {𝔼_{𝒢} (N)}^{-1}^{-1} = 𝔼_{𝒢} (N) ∖ \{\emptyset\}$
25	24	funeqd	$⊢ φ \to (Fun {𝔼_{𝒢} (N)}^{-1}^{-1} \leftrightarrow Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\}))$
26	22 25	mpbird	$⊢ φ \to Fun {𝔼_{𝒢} (N)}^{-1}^{-1}$
27		opex	$⊢ ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩ \in V$
28	27	prid2	$⊢ ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩ \in \{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\}$
29		elun1	$⊢ ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩ \in \{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \to ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩ \in (\{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\})$
30	28 29	ax-mp	$⊢ ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩ \in (\{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\})$
31		eengv	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) = \{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\}$
32	1 31	syl	$⊢ φ \to 𝔼_{𝒢} (N) = \{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\}$
33	30 32	eleqtrrid	$⊢ φ \to ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩ \in 𝔼_{𝒢} (N)$
34		fvex	$⊢ 𝔼 (N) \in V$
35	34 34	mpoex	$⊢ (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2}) \in V$
36	35	a1i	$⊢ φ \to (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2}) \in V$
37	17 18 26 33 36	strfv2d	$⊢ φ \to (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2}) = dist (𝔼_{𝒢} (N))$
38	3 37	eqtr4id	$⊢ φ \to \underset{˙}{-} = (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})$
39		simplrl	$⊢ ((φ \land (x = A \land y = B)) \land i \in (1 \dots N)) \to x = A$
40	39	fveq1d	$⊢ ((φ \land (x = A \land y = B)) \land i \in (1 \dots N)) \to x (i) = A (i)$
41		simplrr	$⊢ ((φ \land (x = A \land y = B)) \land i \in (1 \dots N)) \to y = B$
42	41	fveq1d	$⊢ ((φ \land (x = A \land y = B)) \land i \in (1 \dots N)) \to y (i) = B (i)$
43	40 42	oveq12d	$⊢ ((φ \land (x = A \land y = B)) \land i \in (1 \dots N)) \to x (i) - y (i) = A (i) - B (i)$
44	43	oveq1d	$⊢ ((φ \land (x = A \land y = B)) \land i \in (1 \dots N)) \to {(x (i) - y (i))}^{2} = {(A (i) - B (i))}^{2}$
45	44	sumeq2dv	$⊢ (φ \land (x = A \land y = B)) \to \sum_{i = 1}^{N} {(x (i) - y (i))}^{2} = \sum_{i = 1}^{N} {(A (i) - B (i))}^{2}$
46		sumex	$⊢ \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} \in V$
47	46	a1i	$⊢ φ \to \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} \in V$
48	38 45 11 12 47	ovmpod	$⊢ φ \to A \underset{˙}{-} B = \sum_{i = 1}^{N} {(A (i) - B (i))}^{2}$
49	48	eqcomd	$⊢ φ \to \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = A \underset{˙}{-} B$
50		simplrl	$⊢ ((φ \land (x = C \land y = D)) \land i \in (1 \dots N)) \to x = C$
51	50	fveq1d	$⊢ ((φ \land (x = C \land y = D)) \land i \in (1 \dots N)) \to x (i) = C (i)$
52		simplrr	$⊢ ((φ \land (x = C \land y = D)) \land i \in (1 \dots N)) \to y = D$
53	52	fveq1d	$⊢ ((φ \land (x = C \land y = D)) \land i \in (1 \dots N)) \to y (i) = D (i)$
54	51 53	oveq12d	$⊢ ((φ \land (x = C \land y = D)) \land i \in (1 \dots N)) \to x (i) - y (i) = C (i) - D (i)$
55	54	oveq1d	$⊢ ((φ \land (x = C \land y = D)) \land i \in (1 \dots N)) \to {(x (i) - y (i))}^{2} = {(C (i) - D (i))}^{2}$
56	55	sumeq2dv	$⊢ (φ \land (x = C \land y = D)) \to \sum_{i = 1}^{N} {(x (i) - y (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}$
57		sumex	$⊢ \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \in V$
58	57	a1i	$⊢ φ \to \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \in V$
59	38 56 13 14 58	ovmpod	$⊢ φ \to C \underset{˙}{-} D = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}$
60	59	eqcomd	$⊢ φ \to \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} = C \underset{˙}{-} D$
61	49 60	eqeq12d	$⊢ φ \to (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \leftrightarrow A \underset{˙}{-} B = C \underset{˙}{-} D)$
62	16 61	bitrd	$⊢ φ \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow A \underset{˙}{-} B = C \underset{˙}{-} D)$

Metamath Proof Explorer

Theorem ecgrtg

Proof