Theorem ltgseg

Description: The set E denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	legval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	legval.d	⊢ − = ( dist ‘ 𝐺 )
	legval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	legval.l	⊢ ≤ = ( ≤G ‘ 𝐺 )
	legval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	legso.a	⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) )
	legso.f	⊢ ( 𝜑 → Fun − )
	ltgseg.p	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
Assertion	ltgseg	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝐴 = ( 𝑥 − 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		legval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		legval.d	⊢ − = ( dist ‘ 𝐺 )
3		legval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		legval.l	⊢ ≤ = ( ≤G ‘ 𝐺 )
5		legval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		legso.a	⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) )
7		legso.f	⊢ ( 𝜑 → Fun − )
8		ltgseg.p	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
9		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( − ‘ 𝑎 ) = 𝐴 )
10		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
11	10	fveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( − ‘ 𝑎 ) = ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
12	9 11	eqtr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐴 = ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
13		df-ov	⊢ ( 𝑥 − 𝑦 ) = ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ )
14	12 13	eqtr4di	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐴 = ( 𝑥 − 𝑦 ) )
15		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) → 𝑎 ∈ ( 𝑃 × 𝑃 ) )
16		elxp2	⊢ ( 𝑎 ∈ ( 𝑃 × 𝑃 ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
17	15 16	sylib	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
18	14 17	reximddv2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( − ‘ 𝑎 ) = 𝐴 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝐴 = ( 𝑥 − 𝑦 ) )
19	8 6	eleqtrdi	⊢ ( 𝜑 → 𝐴 ∈ ( − “ ( 𝑃 × 𝑃 ) ) )
20		fvelima	⊢ ( ( Fun − ∧ 𝐴 ∈ ( − “ ( 𝑃 × 𝑃 ) ) ) → ∃ 𝑎 ∈ ( 𝑃 × 𝑃 ) ( − ‘ 𝑎 ) = 𝐴 )
21	7 19 20	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝑃 × 𝑃 ) ( − ‘ 𝑎 ) = 𝐴 )
22	18 21	r19.29a	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝐴 = ( 𝑥 − 𝑦 ) )