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	4	eqcomd	$⊢ (p = P \land i = I) \to P = p$
6	5	adantr	$⊢ ((p = P \land i = I) \land x \in P) \to P = p$
7	6	adantr	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to P = p$
8	7	adantr	$⊢ ((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \to P = p$
9	8	adantr	$⊢ (((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \to P = p$
10		simp-6r	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to i = I$
11	10	eqcomd	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to I = i$
12	11	oveqd	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to x I v = x i v$
13	12	eleq2d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to (u \in (x I v) \leftrightarrow u \in (x i v))$
14	11	oveqd	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to y I z = y i z$
15	14	eleq2d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to (u \in (y I z) \leftrightarrow u \in (y i z))$
16	13 15	3anbi12d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \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))$
17	9	adantr	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to P = p$
18	17	adantr	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \to P = p$
19	10	ad2antrr	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to i = I$
20	19	eqcomd	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to I = i$
21	20	oveqd	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to x I a = x i a$
22	21	eleq2d	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to (y \in (x I a) \leftrightarrow y \in (x i a))$
23	20	oveqd	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to x I b = x i b$
24	23	eleq2d	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to (z \in (x I b) \leftrightarrow z \in (x i b))$
25	20	oveqd	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to a I b = a i b$
26	25	eleq2d	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \to (v \in (a I b) \leftrightarrow v \in (a i b))$
27	22 24 26	3anbi123d	$⊢ ((((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \land b \in P) \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)))$
28	18 27	rexeqbidva	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \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)))$
29	17 28	rexeqbidva	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \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)))$
30	16 29	imbi12d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \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))))$
31	9 30	raleqbidva	$⊢ (((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \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))))$
32	8 31	raleqbidva	$⊢ ((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \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))))$
33	7 32	raleqbidva	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \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))))$
34	6 33	raleqbidva	$⊢ ((p = P \land i = I) \land x \in P) \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))))$
35	5 34	raleqbidva	$⊢ (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))))$
36	1 3 35	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))))$
37		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)))\}$
38	36 37	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