Metamath Proof Explorer

Theorem 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 ⊢ - ˙ = dist ⁡ G
iscgrg.e ⊢ ∼ ˙ = ∼ 𝒢 ⁡ G
iscgrgd.g ⊢ φ → G ∈ V
iscgrgd.d ⊢ φ → D ⊆ ℝ
iscgrgd.a ⊢ φ → A : D ⟶ P
iscgrgd.b ⊢ φ → B : D ⟶ P
Assertion iscgrgd ⊢ φ → A ∼ ˙ B ↔ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j

Proof

Step Hyp Ref Expression
1 iscgrg.p ⊢ P = Base G
2 iscgrg.m ⊢ - ˙ = dist ⁡ G
3 iscgrg.e ⊢ ∼ ˙ = ∼ 𝒢 ⁡ G
4 iscgrgd.g ⊢ φ → G ∈ V
5 iscgrgd.d ⊢ φ → D ⊆ ℝ
6 iscgrgd.a ⊢ φ → A : D ⟶ P
7 iscgrgd.b ⊢ φ → B : D ⟶ P
8 1 fvexi ⊢ P ∈ V
9 reex ⊢ ℝ ∈ V
10 elpm2r ⊢ P ∈ V ∧ ℝ ∈ V ∧ A : D ⟶ P ∧ D ⊆ ℝ → A ∈ P ↑ 𝑝𝑚 ℝ
11 8 9 10 mpanl12 ⊢ A : D ⟶ P ∧ D ⊆ ℝ → A ∈ P ↑ 𝑝𝑚 ℝ
12 6 5 11 syl2anc ⊢ φ → A ∈ P ↑ 𝑝𝑚 ℝ
13 elpm2r ⊢ P ∈ V ∧ ℝ ∈ V ∧ B : D ⟶ P ∧ D ⊆ ℝ → B ∈ P ↑ 𝑝𝑚 ℝ
14 8 9 13 mpanl12 ⊢ B : D ⟶ P ∧ D ⊆ ℝ → B ∈ P ↑ 𝑝𝑚 ℝ
15 7 5 14 syl2anc ⊢ φ → B ∈ P ↑ 𝑝𝑚 ℝ
16 12 15 jca ⊢ φ → A ∈ P ↑ 𝑝𝑚 ℝ ∧ B ∈ P ↑ 𝑝𝑚 ℝ
17 16 biantrurd ⊢ φ → dom ⁡ A = dom ⁡ B ∧ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j ↔ A ∈ P ↑ 𝑝𝑚 ℝ ∧ B ∈ P ↑ 𝑝𝑚 ℝ ∧ dom ⁡ A = dom ⁡ B ∧ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j
18 6 fdmd ⊢ φ → dom ⁡ A = D
19 7 fdmd ⊢ φ → dom ⁡ B = D
20 18 19 eqtr4d ⊢ φ → dom ⁡ A = dom ⁡ B
21 20 biantrurd ⊢ φ → ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j ↔ dom ⁡ A = dom ⁡ B ∧ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j
22 1 2 3 iscgrg ⊢ G ∈ V → A ∼ ˙ B ↔ A ∈ P ↑ 𝑝𝑚 ℝ ∧ B ∈ P ↑ 𝑝𝑚 ℝ ∧ dom ⁡ A = dom ⁡ B ∧ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j
23 4 22 syl ⊢ φ → A ∼ ˙ B ↔ A ∈ P ↑ 𝑝𝑚 ℝ ∧ B ∈ P ↑ 𝑝𝑚 ℝ ∧ dom ⁡ A = dom ⁡ B ∧ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j
24 17 21 23 3bitr4rd ⊢ φ → A ∼ ˙ B ↔ ∀ i ∈ dom ⁡ A ∀ j ∈ dom ⁡ A A ⁡ i - ˙ A ⁡ j = B ⁡ i - ˙ B ⁡ j