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 
|- P = ( Base ` G )
iscgrg.m 
|- .- = ( dist ` G )
iscgrg.e 
|- .~ = ( cgrG ` G )
Assertion iscgrg 
|- ( G e. V -> ( A .~ B <-> ( ( A e. ( P ^pm RR ) /\ B e. ( P ^pm RR ) ) /\ ( dom A = dom B /\ A. i e. dom A A. j e. 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 
 |-  .~ = ( cgrG ` G )
4 elex 
 |-  ( G e. V -> G e. _V )
5 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
6 5 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
7 6 oveq1d 
 |-  ( g = G -> ( ( Base ` g ) ^pm RR ) = ( P ^pm RR ) )
8 7 eleq2d 
 |-  ( g = G -> ( a e. ( ( Base ` g ) ^pm RR ) <-> a e. ( P ^pm RR ) ) )
9 7 eleq2d 
 |-  ( g = G -> ( b e. ( ( Base ` g ) ^pm RR ) <-> b e. ( P ^pm RR ) ) )
10 8 9 anbi12d 
 |-  ( g = G -> ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) <-> ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) ) )
11 fveq2 
 |-  ( g = G -> ( dist ` g ) = ( dist ` G ) )
12 11 2 eqtr4di 
 |-  ( g = G -> ( dist ` g ) = .- )
13 12 oveqd 
 |-  ( g = G -> ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( a ` i ) .- ( a ` j ) ) )
14 12 oveqd 
 |-  ( g = G -> ( ( b ` i ) ( dist ` g ) ( b ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) )
15 13 14 eqeq12d 
 |-  ( g = G -> ( ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) <-> ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) )
16 15 2ralbidv 
 |-  ( g = G -> ( A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) <-> A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) )
17 16 anbi2d 
 |-  ( g = G -> ( ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) <-> ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) )
18 10 17 anbi12d 
 |-  ( g = G -> ( ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) <-> ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) ) )
19 18 opabbidv 
 |-  ( g = G -> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) } = { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } )
20 df-cgrg 
 |-  cgrG = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) } )
21 df-xp 
 |-  ( ( P ^pm RR ) X. ( P ^pm RR ) ) = { <. a , b >. | ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) }
22 ovex 
 |-  ( P ^pm RR ) e. _V
23 22 22 xpex 
 |-  ( ( P ^pm RR ) X. ( P ^pm RR ) ) e. _V
24 21 23 eqeltrri 
 |-  { <. a , b >. | ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) } e. _V
25 simpl 
 |-  ( ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) -> ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) )
26 25 ssopab2i 
 |-  { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } C_ { <. a , b >. | ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) }
27 24 26 ssexi 
 |-  { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } e. _V
28 19 20 27 fvmpt 
 |-  ( G e. _V -> ( cgrG ` G ) = { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } )
29 4 28 syl 
 |-  ( G e. V -> ( cgrG ` G ) = { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } )
30 3 29 syl5eq 
 |-  ( G e. V -> .~ = { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } )
31 30 breqd 
 |-  ( G e. V -> ( A .~ B <-> A { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } B ) )
32 dmeq 
 |-  ( a = A -> dom a = dom A )
33 32 eqeq1d 
 |-  ( a = A -> ( dom a = dom b <-> dom A = dom b ) )
34 32 adantr 
 |-  ( ( a = A /\ i e. dom a ) -> dom a = dom A )
35 simpll 
 |-  ( ( ( a = A /\ i e. dom a ) /\ j e. dom a ) -> a = A )
36 35 fveq1d 
 |-  ( ( ( a = A /\ i e. dom a ) /\ j e. dom a ) -> ( a ` i ) = ( A ` i ) )
37 35 fveq1d 
 |-  ( ( ( a = A /\ i e. dom a ) /\ j e. dom a ) -> ( a ` j ) = ( A ` j ) )
38 36 37 oveq12d 
 |-  ( ( ( a = A /\ i e. dom a ) /\ j e. dom a ) -> ( ( a ` i ) .- ( a ` j ) ) = ( ( A ` i ) .- ( A ` j ) ) )
39 38 eqeq1d 
 |-  ( ( ( a = A /\ i e. dom a ) /\ j e. dom a ) -> ( ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) <-> ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) )
40 34 39 raleqbidva 
 |-  ( ( a = A /\ i e. dom a ) -> ( A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) <-> A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) )
41 32 40 raleqbidva 
 |-  ( a = A -> ( A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) <-> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) )
42 33 41 anbi12d 
 |-  ( a = A -> ( ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) <-> ( dom A = dom b /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) )
43 dmeq 
 |-  ( b = B -> dom b = dom B )
44 43 eqeq2d 
 |-  ( b = B -> ( dom A = dom b <-> dom A = dom B ) )
45 fveq1 
 |-  ( b = B -> ( b ` i ) = ( B ` i ) )
46 fveq1 
 |-  ( b = B -> ( b ` j ) = ( B ` j ) )
47 45 46 oveq12d 
 |-  ( b = B -> ( ( b ` i ) .- ( b ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
48 47 eqeq2d 
 |-  ( b = B -> ( ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) <-> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
49 48 2ralbidv 
 |-  ( b = B -> ( A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) <-> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
50 44 49 anbi12d 
 |-  ( b = B -> ( ( dom A = dom b /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) <-> ( dom A = dom B /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
51 42 50 sylan9bb 
 |-  ( ( a = A /\ b = B ) -> ( ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) <-> ( dom A = dom B /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
52 eqid 
 |-  { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } = { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) }
53 51 52 brab2a 
 |-  ( A { <. a , b >. | ( ( a e. ( P ^pm RR ) /\ b e. ( P ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) .- ( a ` j ) ) = ( ( b ` i ) .- ( b ` j ) ) ) ) } B <-> ( ( A e. ( P ^pm RR ) /\ B e. ( P ^pm RR ) ) /\ ( dom A = dom B /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
54 31 53 bitrdi 
 |-  ( G e. V -> ( A .~ B <-> ( ( A e. ( P ^pm RR ) /\ B e. ( P ^pm RR ) ) /\ ( dom A = dom B /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) ) )