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=BaseG
tgjustc2.d ⊢RErP×P
Assertion tgjustc2 ⊢∃ddFnP×P∧∀w∈P∀x∈P∀y∈P∀z∈PwxRyz↔wdx=ydz

Proof

Step Hyp Ref Expression
1 tgjustc2.p ⊢P=BaseG
2 tgjustc2.d ⊢RErP×P
3 1 fvexi ⊢P∈V
4 3 3 xpex ⊢P×P∈V
5 tgjustr ⊢P×P∈V∧RErP×P→∃ddFnP×P∧∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v
6 4 2 5 mp2an ⊢∃ddFnP×P∧∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v
7 simplrl ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→w∈P
8 simplrr ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→x∈P
9 7 8 opelxpd ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→wx∈P×P
10 simprl ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→y∈P
11 simprr ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→z∈P
12 10 11 opelxpd ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→yz∈P×P
13 simpll ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v
14 breq1 ⊢u=wx→uRv↔wxRv
15 fveq2 ⊢u=wx→d⁡u=d⁡wx
16 df-ov ⊢wdx=d⁡wx
17 15 16 eqtr4di ⊢u=wx→d⁡u=wdx
18 17 eqeq1d ⊢u=wx→d⁡u=d⁡v↔wdx=d⁡v
19 14 18 bibi12d ⊢u=wx→uRv↔d⁡u=d⁡v↔wxRv↔wdx=d⁡v
20 breq2 ⊢v=yz→wxRv↔wxRyz
21 fveq2 ⊢v=yz→d⁡v=d⁡yz
22 df-ov ⊢ydz=d⁡yz
23 21 22 eqtr4di ⊢v=yz→d⁡v=ydz
24 23 eqeq2d ⊢v=yz→wdx=d⁡v↔wdx=ydz
25 20 24 bibi12d ⊢v=yz→wxRv↔wdx=d⁡v↔wxRyz↔wdx=ydz
26 19 25 rspc2va ⊢wx∈P×P∧yz∈P×P∧∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v→wxRyz↔wdx=ydz
27 9 12 13 26 syl21anc ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P∧y∈P∧z∈P→wxRyz↔wdx=ydz
28 27 ralrimivva ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v∧w∈P∧x∈P→∀y∈P∀z∈PwxRyz↔wdx=ydz
29 28 ralrimivva ⊢∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v→∀w∈P∀x∈P∀y∈P∀z∈PwxRyz↔wdx=ydz
30 29 anim2i ⊢dFnP×P∧∀u∈P×P∀v∈P×PuRv↔d⁡u=d⁡v→dFnP×P∧∀w∈P∀x∈P∀y∈P∀z∈PwxRyz↔wdx=ydz
31 6 30 eximii ⊢∃ddFnP×P∧∀w∈P∀x∈P∀y∈P∀z∈PwxRyz↔wdx=ydz