Metamath Proof Explorer

Theorem tgjustc2

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 tgjustc2.p 
|- P = ( Base ` G )
tgjustc2.d 
|- R Er ( P X. P )
Assertion tgjustc2 
|- E. d ( d Fn ( 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 d x ) = ( y d z ) ) )

Proof

Step Hyp Ref Expression
1 tgjustc2.p 
 |-  P = ( Base ` G )
2 tgjustc2.d 
 |-  R Er ( P X. P )
3 1 fvexi 
 |-  P e. _V
4 3 3 xpex 
 |-  ( P X. P ) e. _V
5 tgjustr 
 |-  ( ( ( P X. P ) e. _V /\ R Er ( P X. P ) ) -> E. d ( d Fn ( P X. P ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` v ) ) ) )
6 4 2 5 mp2an 
 |-  E. d ( d Fn ( P X. P ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` v ) ) )
7 simplrl 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` 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 <-> ( d ` u ) = ( d ` v ) ) )
14 breq1 
 |-  ( u = <. w , x >. -> ( u R v <-> <. w , x >. R v ) )
15 fveq2 
 |-  ( u = <. w , x >. -> ( d ` u ) = ( d ` <. w , x >. ) )
16 df-ov 
 |-  ( w d x ) = ( d ` <. w , x >. )
17 15 16 eqtr4di 
 |-  ( u = <. w , x >. -> ( d ` u ) = ( w d x ) )
18 17 eqeq1d 
 |-  ( u = <. w , x >. -> ( ( d ` u ) = ( d ` v ) <-> ( w d x ) = ( d ` v ) ) )
19 14 18 bibi12d 
 |-  ( u = <. w , x >. -> ( ( u R v <-> ( d ` u ) = ( d ` v ) ) <-> ( <. w , x >. R v <-> ( w d x ) = ( d ` v ) ) ) )
20 breq2 
 |-  ( v = <. y , z >. -> ( <. w , x >. R v <-> <. w , x >. R <. y , z >. ) )
21 fveq2 
 |-  ( v = <. y , z >. -> ( d ` v ) = ( d ` <. y , z >. ) )
22 df-ov 
 |-  ( y d z ) = ( d ` <. y , z >. )
23 21 22 eqtr4di 
 |-  ( v = <. y , z >. -> ( d ` v ) = ( y d z ) )
24 23 eqeq2d 
 |-  ( v = <. y , z >. -> ( ( w d x ) = ( d ` v ) <-> ( w d x ) = ( y d z ) ) )
25 20 24 bibi12d 
 |-  ( v = <. y , z >. -> ( ( <. w , x >. R v <-> ( w d x ) = ( d ` v ) ) <-> ( <. w , x >. R <. y , z >. <-> ( w d x ) = ( y d 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 <-> ( d ` u ) = ( d ` v ) ) ) -> ( <. w , x >. R <. y , z >. <-> ( w d x ) = ( y d z ) ) )
27 9 12 13 26 syl21anc 
 |-  ( ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` v ) ) /\ ( w e. P /\ x e. P ) ) /\ ( y e. P /\ z e. P ) ) -> ( <. w , x >. R <. y , z >. <-> ( w d x ) = ( y d z ) ) )
28 27 ralrimivva 
 |-  ( ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` v ) ) /\ ( w e. P /\ x e. P ) ) -> A. y e. P A. z e. P ( <. w , x >. R <. y , z >. <-> ( w d x ) = ( y d z ) ) )
29 28 ralrimivva 
 |-  ( A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` v ) ) -> A. w e. P A. x e. P A. y e. P A. z e. P ( <. w , x >. R <. y , z >. <-> ( w d x ) = ( y d z ) ) )
30 29 anim2i 
 |-  ( ( d Fn ( P X. P ) /\ A. u e. ( P X. P ) A. v e. ( P X. P ) ( u R v <-> ( d ` u ) = ( d ` v ) ) ) -> ( d Fn ( 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 d x ) = ( y d z ) ) ) )
31 6 30 eximii 
 |-  E. d ( d Fn ( 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 d x ) = ( y d z ) ) )