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 
|- .~ = ( cgrG ` G )
iscgrgd.g 
|- ( ph -> G e. V )
iscgrgd.d 
|- ( ph -> D C_ RR )
iscgrgd.a 
|- ( ph -> A : D --> P )
iscgrgd.b 
|- ( ph -> B : D --> P )
Assertion iscgrgd 
|- ( ph -> ( A .~ 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 iscgrgd.g 
 |-  ( ph -> G e. V )
5 iscgrgd.d 
 |-  ( ph -> D C_ RR )
6 iscgrgd.a 
 |-  ( ph -> A : D --> P )
7 iscgrgd.b 
 |-  ( ph -> B : D --> P )
8 1 fvexi 
 |-  P e. _V
9 reex 
 |-  RR e. _V
10 elpm2r 
 |-  ( ( ( P e. _V /\ RR e. _V ) /\ ( A : D --> P /\ D C_ RR ) ) -> A e. ( P ^pm RR ) )
11 8 9 10 mpanl12 
 |-  ( ( A : D --> P /\ D C_ RR ) -> A e. ( P ^pm RR ) )
12 6 5 11 syl2anc 
 |-  ( ph -> A e. ( P ^pm RR ) )
13 elpm2r 
 |-  ( ( ( P e. _V /\ RR e. _V ) /\ ( B : D --> P /\ D C_ RR ) ) -> B e. ( P ^pm RR ) )
14 8 9 13 mpanl12 
 |-  ( ( B : D --> P /\ D C_ RR ) -> B e. ( P ^pm RR ) )
15 7 5 14 syl2anc 
 |-  ( ph -> B e. ( P ^pm RR ) )
16 12 15 jca 
 |-  ( ph -> ( A e. ( P ^pm RR ) /\ B e. ( P ^pm RR ) ) )
17 16 biantrurd 
 |-  ( ph -> ( ( 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 ) ) /\ ( dom A = dom B /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) ) )
18 6 fdmd 
 |-  ( ph -> dom A = D )
19 7 fdmd 
 |-  ( ph -> dom B = D )
20 18 19 eqtr4d 
 |-  ( ph -> dom A = dom B )
21 20 biantrurd 
 |-  ( ph -> ( 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 ) ) ) ) )
22 1 2 3 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 ) ) ) ) ) )
23 4 22 syl 
 |-  ( ph -> ( 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 ) ) ) ) ) )
24 17 21 23 3bitr4rd 
 |-  ( ph -> ( A .~ B <-> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )