ltgseg

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

	Ref	Expression
Hypotheses	legval.p	$⊢ P = {Base}_{G}$
	legval.d	$⊢ \underset{˙}{-} = dist (G)$
	legval.i	$⊢ I = Itv (G)$
	legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
	legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	legso.a	$⊢ E = \underset{˙}{-} [P \times P]$
	legso.f	$⊢ φ \to Fun \underset{˙}{-}$
	ltgseg.p	$⊢ φ \to A \in E$
Assertion	ltgseg	$⊢ φ \to \exists x \in P \exists y \in P A = x \underset{˙}{-} y$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$⊢ P = {Base}_{G}$
2		legval.d	$⊢ \underset{˙}{-} = dist (G)$
3		legval.i	$⊢ I = Itv (G)$
4		legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
5		legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		legso.a	$⊢ E = \underset{˙}{-} [P \times P]$
7		legso.f	$⊢ φ \to Fun \underset{˙}{-}$
8		ltgseg.p	$⊢ φ \to A \in E$
9		simp-4r	$⊢ (((((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \land x \in P) \land y \in P) \land a = ⟨x, y⟩) \to \underset{˙}{-} (a) = A$
10		simpr	$⊢ (((((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \land x \in P) \land y \in P) \land a = ⟨x, y⟩) \to a = ⟨x, y⟩$
11	10	fveq2d	$⊢ (((((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \land x \in P) \land y \in P) \land a = ⟨x, y⟩) \to \underset{˙}{-} (a) = \underset{˙}{-} (⟨x, y⟩)$
12	9 11	eqtr3d	$⊢ (((((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \land x \in P) \land y \in P) \land a = ⟨x, y⟩) \to A = \underset{˙}{-} (⟨x, y⟩)$
13		df-ov	$⊢ x \underset{˙}{-} y = \underset{˙}{-} (⟨x, y⟩)$
14	12 13	eqtr4di	$⊢ (((((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \land x \in P) \land y \in P) \land a = ⟨x, y⟩) \to A = x \underset{˙}{-} y$
15		simplr	$⊢ ((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \to a \in (P \times P)$
16		elxp2	$⊢ a \in (P \times P) \leftrightarrow \exists x \in P \exists y \in P a = ⟨x, y⟩$
17	15 16	sylib	$⊢ ((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \to \exists x \in P \exists y \in P a = ⟨x, y⟩$
18	14 17	reximddv2	$⊢ ((φ \land a \in (P \times P)) \land \underset{˙}{-} (a) = A) \to \exists x \in P \exists y \in P A = x \underset{˙}{-} y$
19	8 6	eleqtrdi	$⊢ φ \to A \in \underset{˙}{-} [P \times P]$
20		fvelima	$⊢ (Fun \underset{˙}{-} \land A \in \underset{˙}{-} [P \times P]) \to \exists a \in (P \times P) \underset{˙}{-} (a) = A$
21	7 19 20	syl2anc	$⊢ φ \to \exists a \in (P \times P) \underset{˙}{-} (a) = A$
22	18 21	r19.29a	$⊢ φ \to \exists x \in P \exists y \in P A = x \underset{˙}{-} y$

Metamath Proof Explorer

Theorem ltgseg

Proof