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 syl5eq ( 𝐺𝑉 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃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 𝐴 ( ( 𝐴𝑖 ) ( 𝐴𝑗 ) ) = ( ( 𝐵𝑖 ) ( 𝐵𝑗 ) ) ) ) ) )