Metamath Proof Explorer

Theorem iscgrg

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

Ref Expression
Hypotheses iscgrg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
iscgrg.m ⊢ − = ( dist ‘ 𝐺 )
iscgrg.e ⊢ ∼ = ( cgrG ‘ 𝐺 )
Assertion iscgrg ( 𝐺 ∈ 𝑉 → ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iscgrg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 iscgrg.m ⊢ − = ( dist ‘ 𝐺 )
3 iscgrg.e ⊢ ∼ = ( cgrG ‘ 𝐺 )
4 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
7 6 oveq1d ⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ↑pm ℝ ) = ( 𝑃 ↑pm ℝ ) )
8 7 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ↔ 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ) )
9 7 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ↔ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) )
10 8 9 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ↔ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ) )
11 fveq2 ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
12 11 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = − )
13 12 oveqd ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) )
14 12 oveqd ⊢ ( 𝑔 = 𝐺 → ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) )
15 13 14 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ↔ ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) )
16 15 2ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) )
17 16 anbi2d ⊢ ( 𝑔 = 𝐺 → ( ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) )
18 10 17 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) ) )
19 18 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } )
20 df-cgrg ⊢ cgrG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } )
21 df-xp ⊢ ( ( 𝑃 ↑pm ℝ ) × ( 𝑃 ↑pm ℝ ) ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) }
22 ovex ⊢ ( 𝑃 ↑pm ℝ ) ∈ V
23 22 22 xpex ⊢ ( ( 𝑃 ↑pm ℝ ) × ( 𝑃 ↑pm ℝ ) ) ∈ V
24 21 23 eqeltrri ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) } ∈ V
25 simpl ⊢ ( ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) → ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) )
26 25 ssopab2i ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ⊆ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) }
27 24 26 ssexi ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ∈ V
28 19 20 27 fvmpt ⊢ ( 𝐺 ∈ V → ( cgrG ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } )
29 4 28 syl ⊢ ( 𝐺 ∈ 𝑉 → ( cgrG ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } )
30 3 29 eqtrid ⊢ ( 𝐺 ∈ 𝑉 → ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } )
31 30 breqd ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐴 ∼ 𝐵 ↔ 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } 𝐵 ) )
32 dmeq ⊢ ( 𝑎 = 𝐴 → dom 𝑎 = dom 𝐴 )
33 32 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏 ) )
34 32 adantr ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) → dom 𝑎 = dom 𝐴 )
35 simpll ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → 𝑎 = 𝐴 )
36 35 fveq1d ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( 𝑎 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
37 35 fveq1d ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( 𝑎 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
38 36 37 oveq12d ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) )
39 38 eqeq1d ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) )
40 34 39 raleqbidva ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) → ( ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) )
41 32 40 raleqbidva ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) )
42 33 41 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝐴 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) )
43 dmeq ⊢ ( 𝑏 = 𝐵 → dom 𝑏 = dom 𝐵 )
44 43 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵 ) )
45 fveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) )
46 fveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑗 ) )
47 45 46 oveq12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) )
48 47 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
49 48 2ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) )
50 44 49 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( dom 𝐴 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
51 42 50 sylan9bb ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
52 eqid ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) }
53 51 52 brab2a ⊢ ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) )
54 31 53 bitrdi ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) )