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