iscgrgd

Description: The property for two sequences A and B of points to be congruent. (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)$
	iscgrgd.g	$⊢ φ \to G \in V$
	iscgrgd.d	$⊢ φ \to D \subseteq ℝ$
	iscgrgd.a	$⊢ φ \to A : D ⟶ P$
	iscgrgd.b	$⊢ φ \to B : D ⟶ P$
Assertion	iscgrgd	$⊢ φ \to (A \underset{˙}{\sim} B \leftrightarrow \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		iscgrgd.g	$⊢ φ \to G \in V$
5		iscgrgd.d	$⊢ φ \to D \subseteq ℝ$
6		iscgrgd.a	$⊢ φ \to A : D ⟶ P$
7		iscgrgd.b	$⊢ φ \to B : D ⟶ P$
8	1	fvexi	$⊢ P \in V$
9		reex	$⊢ ℝ \in V$
10		elpm2r	$⊢ ((P \in V \land ℝ \in V) \land (A : D ⟶ P \land D \subseteq ℝ)) \to A \in (P ↑_{𝑝𝑚} ℝ)$
11	8 9 10	mpanl12	$⊢ (A : D ⟶ P \land D \subseteq ℝ) \to A \in (P ↑_{𝑝𝑚} ℝ)$
12	6 5 11	syl2anc	$⊢ φ \to A \in (P ↑_{𝑝𝑚} ℝ)$
13		elpm2r	$⊢ ((P \in V \land ℝ \in V) \land (B : D ⟶ P \land D \subseteq ℝ)) \to B \in (P ↑_{𝑝𝑚} ℝ)$
14	8 9 13	mpanl12	$⊢ (B : D ⟶ P \land D \subseteq ℝ) \to B \in (P ↑_{𝑝𝑚} ℝ)$
15	7 5 14	syl2anc	$⊢ φ \to B \in (P ↑_{𝑝𝑚} ℝ)$
16	12 15	jca	$⊢ φ \to (A \in (P ↑_{𝑝𝑚} ℝ) \land B \in (P ↑_{𝑝𝑚} ℝ))$
17	16	biantrurd	$⊢ φ \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 ((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))))$
18	6	fdmd	$⊢ φ \to dom A = D$
19	7	fdmd	$⊢ φ \to dom B = D$
20	18 19	eqtr4d	$⊢ φ \to dom A = dom B$
21	20	biantrurd	$⊢ φ \to (\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)))$
22	1 2 3	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))))$
23	4 22	syl	$⊢ φ \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))))$
24	17 21 23	3bitr4rd	$⊢ φ \to (A \underset{˙}{\sim} B \leftrightarrow \forall i \in dom A \forall j \in dom A A (i) \underset{˙}{-} A (j) = B (i) \underset{˙}{-} B (j))$

Metamath Proof Explorer

Theorem iscgrgd

Proof