iscgrg

Description: The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019)

	Ref	Expression
Hypotheses	iscgrg.p	$⊢ P = {Base}_{G}$
	iscgrg.m	$⊢ \underset{˙}{-} = dist (G)$
	iscgrg.e	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
Assertion	iscgrg	$⊢ G \in V \to (A \underset{˙}{\sim} B \leftrightarrow ((A \in (P ↑_{𝑝𝑚} ℝ) \land B \in (P ↑_{𝑝𝑚} ℝ)) \land (dom A = dom B \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j))))$

Proof

Step	Hyp	Ref	Expression
1		iscgrg.p	$⊢ P = {Base}_{G}$
2		iscgrg.m	$⊢ \underset{˙}{-} = dist (G)$
3		iscgrg.e	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
4		elex	$⊢ G \in V \to G \in V$
5		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
6	5 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
7	6	oveq1d	$⊢ g = G \to {Base}_{g} ↑_{𝑝𝑚} ℝ = P ↑_{𝑝𝑚} ℝ$
8	7	eleq2d	$⊢ g = G \to (a \in ({Base}_{g} ↑_{𝑝𝑚} ℝ) \leftrightarrow a \in (P ↑_{𝑝𝑚} ℝ))$
9	7	eleq2d	$⊢ g = G \to (b \in ({Base}_{g} ↑_{𝑝𝑚} ℝ) \leftrightarrow b \in (P ↑_{𝑝𝑚} ℝ))$
10	8 9	anbi12d	$⊢ g = G \to ((a \in ({Base}_{g} ↑_{𝑝𝑚} ℝ) \land b \in ({Base}_{g} ↑_{𝑝𝑚} ℝ)) \leftrightarrow (a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)))$
11		fveq2	$⊢ g = G \to dist (g) = dist (G)$
12	11 2	eqtr4di	$⊢ g = G \to dist (g) = \underset{˙}{-}$
13	12	oveqd	$⊢ g = G \to a (i) dist (g) a (j) = a (i) \underset{˙}{-} a (j)$
14	12	oveqd	$⊢ g = G \to b (i) dist (g) b (j) = b (i) \underset{˙}{-} b (j)$
15	13 14	eqeq12d	$⊢ g = G \to (a (i) dist (g) a (j) = b (i) dist (g) b (j) \leftrightarrow a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j))$
16	15	2ralbidv	$⊢ g = G \to (\forall i \in dom a \forall j \in dom a a (i) dist (g) a (j) = b (i) dist (g) b (j) \leftrightarrow \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j))$
17	16	anbi2d	$⊢ g = G \to ((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)) \leftrightarrow (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))$
18	10 17	anbi12d	$⊢ g = G \to (((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))) \leftrightarrow ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j))))$
19	18	opabbidv	$⊢ g = G \to \{⟨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)))\} = \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\}$
20		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)))\})$
21		df-xp	$⊢ (P ↑_{𝑝𝑚} ℝ) \times (P ↑_{𝑝𝑚} ℝ) = \{⟨a, b⟩ \| (a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ))\}$
22		ovex	$⊢ P ↑_{𝑝𝑚} ℝ \in V$
23	22 22	xpex	$⊢ (P ↑_{𝑝𝑚} ℝ) \times (P ↑_{𝑝𝑚} ℝ) \in V$
24	21 23	eqeltrri	$⊢ \{⟨a, b⟩ \| (a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ))\} \in V$
25		simpl	$⊢ ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j))) \to (a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ))$
26	25	ssopab2i	$⊢ \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\} \subseteq \{⟨a, b⟩ \| (a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ))\}$
27	24 26	ssexi	$⊢ \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\} \in V$
28	19 20 27	fvmpt	$⊢ G \in V \to \sim_{𝒢} (G) = \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\}$
29	4 28	syl	$⊢ G \in V \to \sim_{𝒢} (G) = \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\}$
30	3 29	syl5eq	$⊢ G \in V \to \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\}$
31	30	breqd	$⊢ G \in V \to (A \underset{˙}{\sim} B \leftrightarrow A \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\} B)$
32		dmeq	$⊢ a = A \to dom a = dom A$
33	32	eqeq1d	$⊢ a = A \to (dom a = dom b \leftrightarrow dom A = dom b)$
34	32	adantr	$⊢ (a = A \land i \in dom a) \to dom a = dom A$
35		simpll	$⊢ ((a = A \land i \in dom a) \land j \in dom a) \to a = A$
36	35	fveq1d	$⊢ ((a = A \land i \in dom a) \land j \in dom a) \to a (i) = A (i)$
37	35	fveq1d	$⊢ ((a = A \land i \in dom a) \land j \in dom a) \to a (j) = A (j)$
38	36 37	oveq12d	$⊢ ((a = A \land i \in dom a) \land j \in dom a) \to a (i) \underset{˙}{-} a (j) = A (i) \underset{˙}{-} A (j)$
39	38	eqeq1d	$⊢ ((a = A \land i \in dom a) \land j \in dom a) \to (a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j) \leftrightarrow A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j))$
40	34 39	raleqbidva	$⊢ (a = A \land i \in dom a) \to (\forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j) \leftrightarrow \forall j \in dom A A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j))$
41	32 40	raleqbidva	$⊢ a = A \to (\forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j) \leftrightarrow \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j))$
42	33 41	anbi12d	$⊢ a = A \to ((dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)) \leftrightarrow (dom A = dom b \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j)))$
43		dmeq	$⊢ b = B \to dom b = dom B$
44	43	eqeq2d	$⊢ b = B \to (dom A = dom b \leftrightarrow dom A = dom B)$
45		fveq1	$⊢ b = B \to b (i) = B (i)$
46		fveq1	$⊢ b = B \to b (j) = B (j)$
47	45 46	oveq12d	$⊢ b = B \to b (i) \underset{˙}{-} b (j) = B (i) \underset{˙}{-} B (j)$
48	47	eqeq2d	$⊢ b = B \to (A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j) \leftrightarrow A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j))$
49	48	2ralbidv	$⊢ b = B \to (\forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j) \leftrightarrow \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j))$
50	44 49	anbi12d	$⊢ b = B \to ((dom A = dom b \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = b (i) \underset{˙}{-} b (j)) \leftrightarrow (dom A = dom B \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j)))$
51	42 50	sylan9bb	$⊢ (a = A \land b = B) \to ((dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)) \leftrightarrow (dom A = dom B \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j)))$
52		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\} = \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\}$
53	51 52	brab2a	$⊢ A \{⟨a, b⟩ \| ((a \in (P ↑_{𝑝𝑚} ℝ) \land b \in (P ↑_{𝑝𝑚} ℝ)) \land (dom a = dom b \land \forall i \in dom a \forall j \in dom a a (i) \underset{˙}{-} a (j) = b (i) \underset{˙}{-} b (j)))\} B \leftrightarrow ((A \in (P ↑_{𝑝𝑚} ℝ) \land B \in (P ↑_{𝑝𝑚} ℝ)) \land (dom A = dom B \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j)))$
54	31 53	bitrdi	$⊢ G \in V \to (A \underset{˙}{\sim} B \leftrightarrow ((A \in (P ↑_{𝑝𝑚} ℝ) \land B \in (P ↑_{𝑝𝑚} ℝ)) \land (dom A = dom B \land \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j))))$

Metamath Proof Explorer

Theorem iscgrg

Proof