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 r r Er P × P w P x P y P z 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 V
4 3 3 xpex P × P V
5 tgjustf P × P V r r Er P × P u P × P v P × P u r v - ˙ u = - ˙ v
6 4 5 ax-mp r r Er P × P u P × P v P × P u r v - ˙ u = - ˙ v
7 simplrl u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P w P
8 simplrr u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P x P
9 7 8 opelxpd u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P w x P × P
10 simprl u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P y P
11 simprr u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P z P
12 10 11 opelxpd u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P y z P × P
13 simpll u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P u P × P v P × 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 P × P y z P × P u P × P v P × P u r v - ˙ u = - ˙ v w x r y z w - ˙ x = y - ˙ z
27 9 12 13 26 syl21anc u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P w x r y z w - ˙ x = y - ˙ z
28 27 ralrimivva u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P w x r y z w - ˙ x = y - ˙ z
29 28 ralrimivva u P × P v P × P u r v - ˙ u = - ˙ v w P x P y P z P w x r y z w - ˙ x = y - ˙ z
30 29 anim2i r Er P × P u P × P v P × P u r v - ˙ u = - ˙ v r Er P × P w P x P y P z P w x r y z w - ˙ x = y - ˙ z
31 6 30 eximii r r Er P × P w P x P y P z P w x r y z w - ˙ x = y - ˙ z