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 × P
Assertion tgjustc2 ⊢ ∃ d d Fn P × P ∧ ∀ w ∈ P ∀ x ∈ P ∀ y ∈ P ∀ z ∈ 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 × P
3 1 fvexi ⊢ P ∈ V
4 3 3 xpex ⊢ P × P ∈ V
5 tgjustr ⊢ P × P ∈ V ∧ R Er P × P → ∃ d d Fn P × P ∧ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v
6 4 2 5 mp2an ⊢ ∃ d d Fn P × P ∧ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v
7 simplrl ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → w ∈ P
8 simplrr ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → x ∈ P
9 7 8 opelxpd ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → w x ∈ P × P
10 simprl ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → y ∈ P
11 simprr ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → z ∈ P
12 10 11 opelxpd ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → y z ∈ P × P
13 simpll ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → ∀ u ∈ P × P ∀ v ∈ P × 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 ∈ P × P ∧ y z ∈ P × P ∧ ∀ u ∈ P × P ∀ v ∈ P × 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 ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P ∧ y ∈ P ∧ z ∈ P → w x R y z ↔ w d x = y d z
28 27 ralrimivva ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v ∧ w ∈ P ∧ x ∈ P → ∀ y ∈ P ∀ z ∈ P w x R y z ↔ w d x = y d z
29 28 ralrimivva ⊢ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v → ∀ w ∈ P ∀ x ∈ P ∀ y ∈ P ∀ z ∈ P w x R y z ↔ w d x = y d z
30 29 anim2i ⊢ d Fn P × P ∧ ∀ u ∈ P × P ∀ v ∈ P × P u R v ↔ d ⁡ u = d ⁡ v → d Fn P × P ∧ ∀ w ∈ P ∀ x ∈ P ∀ y ∈ P ∀ z ∈ P w x R y z ↔ w d x = y d z
31 6 30 eximii ⊢ ∃ d d Fn P × P ∧ ∀ w ∈ P ∀ x ∈ P ∀ y ∈ P ∀ z ∈ P w x R y z ↔ w d x = y d z