Metamath Proof Explorer

Theorem tgjustc1

Description: A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023)

Ref Expression
Hypotheses tgjustc1.p 
|- P = ( Base ` G )
tgjustc1.d 
|- .- = ( dist ` G )
Assertion tgjustc1 
|- E. r ( r Er ( P X. P ) /\ A. w e. P A. x e. P A. y e. P A. z e. P ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) )

Proof

Step Hyp Ref Expression
1 tgjustc1.p 
 |-  P = ( Base ` G )
2 tgjustc1.d 
 |-  .- = ( dist ` G )
3 1 fvexi 
 |-  P e. _V
4 3 3 xpex 
 |-  ( P X. P ) e. _V
5 tgjustf 
 |-  ( ( P X. P ) e. _V -> E. r ( r Er ( P X. P ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) ) )
6 4 5 ax-mp 
 |-  E. r ( r Er ( P X. P ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) )
7 simplrl 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> w e. P )
8 simplrr 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> x e. P )
9 7 8 opelxpd 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> <. w , x >. e. ( P X. P ) )
10 simprl 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> y e. P )
11 simprr 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> z e. P )
12 10 11 opelxpd 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> <. y , z >. e. ( P X. P ) )
13 simpll 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) )
14 breq1 
 |-  ( u = <. w , x >. -> ( u r v <-> <. w , x >. r v ) )
15 fveq2 
 |-  ( u = <. w , x >. -> ( .- ` u ) = ( .- ` <. w , x >. ) )
16 df-ov 
 |-  ( w .- x ) = ( .- ` <. w , x >. )
17 15 16 eqtr4di 
 |-  ( u = <. w , x >. -> ( .- ` u ) = ( w .- x ) )
18 17 eqeq1d 
 |-  ( u = <. w , x >. -> ( ( .- ` u ) = ( .- ` v ) <-> ( w .- x ) = ( .- ` v ) ) )
19 14 18 bibi12d 
 |-  ( u = <. w , x >. -> ( ( u r v <-> ( .- ` u ) = ( .- ` v ) ) <-> ( <. w , x >. r v <-> ( w .- x ) = ( .- ` v ) ) ) )
20 breq2 
 |-  ( v = <. y , z >. -> ( <. w , x >. r v <-> <. w , x >. r <. y , z >. ) )
21 fveq2 
 |-  ( v = <. y , z >. -> ( .- ` v ) = ( .- ` <. y , z >. ) )
22 df-ov 
 |-  ( y .- z ) = ( .- ` <. y , z >. )
23 21 22 eqtr4di 
 |-  ( v = <. y , z >. -> ( .- ` v ) = ( y .- z ) )
24 23 eqeq2d 
 |-  ( v = <. y , z >. -> ( ( w .- x ) = ( .- ` v ) <-> ( w .- x ) = ( y .- z ) ) )
25 20 24 bibi12d 
 |-  ( v = <. y , z >. -> ( ( <. w , x >. r v <-> ( w .- x ) = ( .- ` v ) ) <-> ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) ) )
26 19 25 rspc2va 
 |-  ( ( ( <. w , x >. e. ( P X. P ) /\ <. y , z >. e. ( P X. P ) ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) ) -> ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) )
27 9 12 13 26 syl21anc 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) )
28 27 ralrimivva 
 |-  ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) /\ ( w e. P /\ x e. P ) ) -> A. y e. P A. z e. P ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) )
29 28 ralrimivva 
 |-  ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) -> A. w e. P A. x e. P A. y e. P A. z e. P ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) )
30 29 anim2i 
 |-  ( ( r Er ( P X. P ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u r v <-> ( .- ` u ) = ( .- ` v ) ) ) -> ( r Er ( P X. P ) /\ A. w e. P A. x e. P A. y e. P A. z e. P ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) ) )
31 6 30 eximii 
 |-  E. r ( r Er ( P X. P ) /\ A. w e. P A. x e. P A. y e. P A. z e. P ( <. w , x >. r <. y , z >. <-> ( w .- x ) = ( y .- z ) ) )