ercgrg

Description: The shape congruence relation is an equivalence relation. Statement 4.4 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019)

		Ref	Expression
	Hypothesis	ercgrg.p	$⊢ P = {Base}_{G}$
	Assertion	ercgrg	$⊢ G \in 𝒢_{Tarski} \to \sim_{𝒢} (G) Er (P ↑_{𝑝𝑚} ℝ)$

Proof

Step	Hyp	Ref	Expression
1		ercgrg.p	$⊢ P = {Base}_{G}$
2		df-cgrg	$⊢ \sim_{𝒢} = (g \in V ⟼ \{⟨a, b⟩ \| ((a \in ({Base}_{g} ↑_{𝑝𝑚} ℝ) \land b \in ({Base}_{g} ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) dist (g) a (j) = b (i) dist (g) b (j)))\})$
3	2	relmptopab	$⊢ Rel \sim_{𝒢} (G)$
4	3	a1i	$⊢ G \in 𝒢_{Tarski} \to Rel \sim_{𝒢} (G)$
5		eqid	$⊢ dist (G) = dist (G)$
6		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
7	1 5 6	iscgrg	$⊢ G \in 𝒢_{Tarski} \to (x \sim_{𝒢} (G) y \leftrightarrow ((x \in (P ↑_{𝑝𝑚} ℝ) \land y \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom y \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j))))$
8	7	biimpa	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to ((x \in (P ↑_{𝑝𝑚} ℝ) \land y \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom y \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j)))$
9	8	simpld	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to (x \in (P ↑_{𝑝𝑚} ℝ) \land y \in (P ↑_{𝑝𝑚} ℝ))$
10	9	ancomd	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to (y \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ))$
11	8	simprd	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to (dom x = dom y \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j))$
12	11	simpld	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to dom x = dom y$
13	12	eqcomd	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to dom y = dom x$
14		simpl	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y)$
15		simprl	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to i \in dom y$
16	12	adantr	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to dom x = dom y$
17	15 16	eleqtrrd	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to i \in dom x$
18		simprr	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to j \in dom y$
19	18 16	eleqtrrd	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to j \in dom x$
20	11	simprd	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j)$
21	20	r19.21bi	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land i \in dom x) \to \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j)$
22	21	r19.21bi	$⊢ (((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land i \in dom x) \land j \in dom x) \to x (i) dist (G) x (j) = y (i) dist (G) y (j)$
23	14 17 19 22	syl21anc	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to x (i) dist (G) x (j) = y (i) dist (G) y (j)$
24	23	eqcomd	$⊢ ((G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \land (i \in dom y \land j \in dom y)) \to y (i) dist (G) y (j) = x (i) dist (G) x (j)$
25	24	ralrimivva	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = x (i) dist (G) x (j)$
26	13 25	jca	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to (dom y = dom x \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = x (i) dist (G) x (j))$
27	1 5 6	iscgrg	$⊢ G \in 𝒢_{Tarski} \to (y \sim_{𝒢} (G) x \leftrightarrow ((y \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ)) \land (dom y = dom x \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = x (i) dist (G) x (j))))$
28	27	adantr	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to (y \sim_{𝒢} (G) x \leftrightarrow ((y \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ)) \land (dom y = dom x \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = x (i) dist (G) x (j))))$
29	10 26 28	mpbir2and	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to y \sim_{𝒢} (G) x$
30	9	simpld	$⊢ (G \in 𝒢_{Tarski} \land x \sim_{𝒢} (G) y) \to x \in (P ↑_{𝑝𝑚} ℝ)$
31	30	adantrr	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to x \in (P ↑_{𝑝𝑚} ℝ)$
32	1 5 6	iscgrg	$⊢ G \in 𝒢_{Tarski} \to (y \sim_{𝒢} (G) z \leftrightarrow ((y \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ)) \land (dom y = dom z \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = z (i) dist (G) z (j))))$
33	32	biimpa	$⊢ (G \in 𝒢_{Tarski} \land y \sim_{𝒢} (G) z) \to ((y \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ)) \land (dom y = dom z \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = z (i) dist (G) z (j)))$
34	33	adantrl	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to ((y \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ)) \land (dom y = dom z \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = z (i) dist (G) z (j)))$
35	34	simpld	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to (y \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ))$
36	35	simprd	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to z \in (P ↑_{𝑝𝑚} ℝ)$
37	31 36	jca	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to (x \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ))$
38	8	adantrr	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to ((x \in (P ↑_{𝑝𝑚} ℝ) \land y \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom y \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j)))$
39	38	simprd	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to (dom x = dom y \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j))$
40	39	simpld	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to dom x = dom y$
41	34	simprd	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to (dom y = dom z \land \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = z (i) dist (G) z (j))$
42	41	simpld	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to dom y = dom z$
43	40 42	eqtrd	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to dom x = dom z$
44	39	simprd	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j)$
45	44	r19.21bi	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land i \in dom x) \to \forall j \in dom x x (i) dist (G) x (j) = y (i) dist (G) y (j)$
46	45	r19.21bi	$⊢ (((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land i \in dom x) \land j \in dom x) \to x (i) dist (G) x (j) = y (i) dist (G) y (j)$
47	46	anasss	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to x (i) dist (G) x (j) = y (i) dist (G) y (j)$
48		simpl	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z))$
49		simprl	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to i \in dom x$
50	40	adantr	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to dom x = dom y$
51	49 50	eleqtrd	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to i \in dom y$
52		simprr	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to j \in dom x$
53	52 50	eleqtrd	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to j \in dom y$
54	41	simprd	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to \forall i \in dom y \forall j \in dom y y (i) dist (G) y (j) = z (i) dist (G) z (j)$
55	54	r19.21bi	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land i \in dom y) \to \forall j \in dom y y (i) dist (G) y (j) = z (i) dist (G) z (j)$
56	55	r19.21bi	$⊢ (((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land i \in dom y) \land j \in dom y) \to y (i) dist (G) y (j) = z (i) dist (G) z (j)$
57	48 51 53 56	syl21anc	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to y (i) dist (G) y (j) = z (i) dist (G) z (j)$
58	47 57	eqtrd	$⊢ ((G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \land (i \in dom x \land j \in dom x)) \to x (i) dist (G) x (j) = z (i) dist (G) z (j)$
59	58	ralrimivva	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = z (i) dist (G) z (j)$
60	43 59	jca	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to (dom x = dom z \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = z (i) dist (G) z (j))$
61	1 5 6	iscgrg	$⊢ G \in 𝒢_{Tarski} \to (x \sim_{𝒢} (G) z \leftrightarrow ((x \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom z \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = z (i) dist (G) z (j))))$
62	61	adantr	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to (x \sim_{𝒢} (G) z \leftrightarrow ((x \in (P ↑_{𝑝𝑚} ℝ) \land z \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom z \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = z (i) dist (G) z (j))))$
63	37 60 62	mpbir2and	$⊢ (G \in 𝒢_{Tarski} \land (x \sim_{𝒢} (G) y \land y \sim_{𝒢} (G) z)) \to x \sim_{𝒢} (G) z$
64		pm4.24	$⊢ x \in (P ↑_{𝑝𝑚} ℝ) \leftrightarrow (x \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ))$
65		eqid	$⊢ dom x = dom x$
66		eqidd	$⊢ (i \in dom x \land j \in dom x) \to x (i) dist (G) x (j) = x (i) dist (G) x (j)$
67	66	rgen2	$⊢ \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = x (i) dist (G) x (j)$
68	65 67	pm3.2i	$⊢ (dom x = dom x \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = x (i) dist (G) x (j))$
69	68	biantru	$⊢ (x \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ)) \leftrightarrow ((x \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom x \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = x (i) dist (G) x (j)))$
70	64 69	bitri	$⊢ x \in (P ↑_{𝑝𝑚} ℝ) \leftrightarrow ((x \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom x \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = x (i) dist (G) x (j)))$
71	1 5 6	iscgrg	$⊢ G \in 𝒢_{Tarski} \to (x \sim_{𝒢} (G) x \leftrightarrow ((x \in (P ↑_{𝑝𝑚} ℝ) \land x \in (P ↑_{𝑝𝑚} ℝ)) \land (dom x = dom x \land \forall i \in dom x \forall j \in dom x x (i) dist (G) x (j) = x (i) dist (G) x (j))))$
72	70 71	bitr4id	$⊢ G \in 𝒢_{Tarski} \to (x \in (P ↑_{𝑝𝑚} ℝ) \leftrightarrow x \sim_{𝒢} (G) x)$
73	4 29 63 72	iserd	$⊢ G \in 𝒢_{Tarski} \to \sim_{𝒢} (G) Er (P ↑_{𝑝𝑚} ℝ)$

Metamath Proof Explorer

Theorem ercgrg

Proof