istrkge

Description: Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	istrkg.p	$⊢ P = {Base}_{G}$
	istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	istrkg.i	$⊢ I = Itv (G)$
Assertion	istrkge	$⊢ G \in 𝒢_{Tarski}^{E} \leftrightarrow (G \in V \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$⊢ P = {Base}_{G}$
2		istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg.i	$⊢ I = Itv (G)$
4		simpl	$⊢ (p = P \land i = I) \to p = P$
5		simpr	$⊢ (p = P \land i = I) \to i = I$
6	5	oveqd	$⊢ (p = P \land i = I) \to x i v = x I v$
7	6	eleq2d	$⊢ (p = P \land i = I) \to (u \in (x i v) \leftrightarrow u \in (x I v))$
8	5	oveqd	$⊢ (p = P \land i = I) \to y i z = y I z$
9	8	eleq2d	$⊢ (p = P \land i = I) \to (u \in (y i z) \leftrightarrow u \in (y I z))$
10	7 9	3anbi12d	$⊢ (p = P \land i = I) \to ((u \in (x i v) \land u \in (y i z) \land x \neq u) \leftrightarrow (u \in (x I v) \land u \in (y I z) \land x \neq u))$
11	5	oveqd	$⊢ (p = P \land i = I) \to x i a = x I a$
12	11	eleq2d	$⊢ (p = P \land i = I) \to (y \in (x i a) \leftrightarrow y \in (x I a))$
13	5	oveqd	$⊢ (p = P \land i = I) \to x i b = x I b$
14	13	eleq2d	$⊢ (p = P \land i = I) \to (z \in (x i b) \leftrightarrow z \in (x I b))$
15	5	oveqd	$⊢ (p = P \land i = I) \to a i b = a I b$
16	15	eleq2d	$⊢ (p = P \land i = I) \to (v \in (a i b) \leftrightarrow v \in (a I b))$
17	12 14 16	3anbi123d	$⊢ (p = P \land i = I) \to ((y \in (x i a) \land z \in (x i b) \land v \in (a i b)) \leftrightarrow (y \in (x I a) \land z \in (x I b) \land v \in (a I b)))$
18	4 17	rexeqbidv	$⊢ (p = P \land i = I) \to (\exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)) \leftrightarrow \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b)))$
19	4 18	rexeqbidv	$⊢ (p = P \land i = I) \to (\exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)) \leftrightarrow \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b)))$
20	10 19	imbi12d	$⊢ (p = P \land i = I) \to (((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
21	4 20	raleqbidv	$⊢ (p = P \land i = I) \to (\forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
22	4 21	raleqbidv	$⊢ (p = P \land i = I) \to (\forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
23	4 22	raleqbidv	$⊢ (p = P \land i = I) \to (\forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
24	4 23	raleqbidv	$⊢ (p = P \land i = I) \to (\forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
25	4 24	raleqbidv	$⊢ (p = P \land i = I) \to (\forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
26	1 3 25	sbcie2s	$⊢ f = G \to (\underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))) \leftrightarrow \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
27		df-trkge	$⊢ 𝒢_{Tarski}^{E} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))\}$
28	26 27	elab4g	$⊢ G \in 𝒢_{Tarski}^{E} \leftrightarrow (G \in V \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$

Metamath Proof Explorer

Theorem istrkge

Proof