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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
iscgrg.m ⊢ − = ( dist ‘ 𝐺 )
iscgrg.e ⊢ ∼ = ( cgrG ‘ 𝐺 )
iscgrgd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
iscgrgd.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
iscgrgd.a ⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑃 )
iscgrgd.b ⊢ ( 𝜑 → 𝐵 : 𝐷 ⟶ 𝑃 )
Assertion iscgrgd ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscgrg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 iscgrg.m ⊢ − = ( dist ‘ 𝐺 )
3 iscgrg.e ⊢ ∼ = ( cgrG ‘ 𝐺 )
4 iscgrgd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5 iscgrgd.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
6 iscgrgd.a ⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑃 )
7 iscgrgd.b ⊢ ( 𝜑 → 𝐵 : 𝐷 ⟶ 𝑃 )
8 1 fvexi ⊢ 𝑃 ∈ V
9 reex ⊢ ℝ ∈ V
10 elpm2r ⊢ ( ( ( 𝑃 ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐴 : 𝐷 ⟶ 𝑃 ∧ 𝐷 ⊆ ℝ ) ) → 𝐴 ∈ ( 𝑃 ↑pm ℝ ) )
11 8 9 10 mpanl12 ⊢ ( ( 𝐴 : 𝐷 ⟶ 𝑃 ∧ 𝐷 ⊆ ℝ ) → 𝐴 ∈ ( 𝑃 ↑pm ℝ ) )
12 6 5 11 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑃 ↑pm ℝ ) )
13 elpm2r ⊢ ( ( ( 𝑃 ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐵 : 𝐷 ⟶ 𝑃 ∧ 𝐷 ⊆ ℝ ) ) → 𝐵 ∈ ( 𝑃 ↑pm ℝ ) )
14 8 9 13 mpanl12 ⊢ ( ( 𝐵 : 𝐷 ⟶ 𝑃 ∧ 𝐷 ⊆ ℝ ) → 𝐵 ∈ ( 𝑃 ↑pm ℝ ) )
15 7 5 14 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑃 ↑pm ℝ ) )
16 12 15 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) )
17 16 biantrurd ⊢ ( 𝜑 → ( ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
18 6 fdmd ⊢ ( 𝜑 → dom 𝐴 = 𝐷 )
19 7 fdmd ⊢ ( 𝜑 → dom 𝐵 = 𝐷 )
20 18 19 eqtr4d ⊢ ( 𝜑 → dom 𝐴 = dom 𝐵 )
21 20 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
22 1 2 3 iscgrg ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
23 4 22 syl ⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
24 17 21 23 3bitr4rd ⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )