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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgjustc1.d	⊢ − = ( dist ‘ 𝐺 )
Assertion	tgjustc1	⊢ ∃ 𝑟 ( 𝑟 Er ( 𝑃 × 𝑃 ) ∧ ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgjustc1.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgjustc1.d	⊢ − = ( dist ‘ 𝐺 )
3	1	fvexi	⊢ 𝑃 ∈ V
4	3 3	xpex	⊢ ( 𝑃 × 𝑃 ) ∈ V
5		tgjustf	⊢ ( ( 𝑃 × 𝑃 ) ∈ V → ∃ 𝑟 ( 𝑟 Er ( 𝑃 × 𝑃 ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ) )
6	4 5	ax-mp	⊢ ∃ 𝑟 ( 𝑟 Er ( 𝑃 × 𝑃 ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) )
7		simplrl	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑤 ∈ 𝑃 )
8		simplrr	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑥 ∈ 𝑃 )
9	7 8	opelxpd	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ⟨ 𝑤 , 𝑥 ⟩ ∈ ( 𝑃 × 𝑃 ) )
10		simprl	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑦 ∈ 𝑃 )
11		simprr	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑧 ∈ 𝑃 )
12	10 11	opelxpd	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑃 × 𝑃 ) )
13		simpll	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) )
14		breq1	⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( 𝑢 𝑟 𝑣 ↔ ⟨ 𝑤 , 𝑥 ⟩ 𝑟 𝑣 ) )
15		fveq2	⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( − ‘ 𝑢 ) = ( − ‘ ⟨ 𝑤 , 𝑥 ⟩ ) )
16		df-ov	⊢ ( 𝑤 − 𝑥 ) = ( − ‘ ⟨ 𝑤 , 𝑥 ⟩ )
17	15 16	eqtr4di	⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( − ‘ 𝑢 ) = ( 𝑤 − 𝑥 ) )
18	17	eqeq1d	⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ↔ ( 𝑤 − 𝑥 ) = ( − ‘ 𝑣 ) ) )
19	14 18	bibi12d	⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ↔ ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 𝑣 ↔ ( 𝑤 − 𝑥 ) = ( − ‘ 𝑣 ) ) ) )
20		breq2	⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 𝑣 ↔ ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ) )
21		fveq2	⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( − ‘ 𝑣 ) = ( − ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
22		df-ov	⊢ ( 𝑦 − 𝑧 ) = ( − ‘ ⟨ 𝑦 , 𝑧 ⟩ )
23	21 22	eqtr4di	⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( − ‘ 𝑣 ) = ( 𝑦 − 𝑧 ) )
24	23	eqeq2d	⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑤 − 𝑥 ) = ( − ‘ 𝑣 ) ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )
25	20 24	bibi12d	⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 𝑣 ↔ ( 𝑤 − 𝑥 ) = ( − ‘ 𝑣 ) ) ↔ ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) ) )
26	19 25	rspc2va	⊢ ( ( ( ⟨ 𝑤 , 𝑥 ⟩ ∈ ( 𝑃 × 𝑃 ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑃 × 𝑃 ) ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ) → ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )
27	9 12 13 26	syl21anc	⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )
28	27	ralrimivva	⊢ ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) → ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )
29	28	ralrimivva	⊢ ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) → ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )
30	29	anim2i	⊢ ( ( 𝑟 Er ( 𝑃 × 𝑃 ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑟 𝑣 ↔ ( − ‘ 𝑢 ) = ( − ‘ 𝑣 ) ) ) → ( 𝑟 Er ( 𝑃 × 𝑃 ) ∧ ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) ) )
31	6 30	eximii	⊢ ∃ 𝑟 ( 𝑟 Er ( 𝑃 × 𝑃 ) ∧ ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑟 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 − 𝑥 ) = ( 𝑦 − 𝑧 ) ) )